------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to transitive closures that relies on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Relation.Binary.Construct.Closure.Transitive.WithK where

open import Function.Base using (_∋_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where

 ∼⁺⟨⟩-injectiveˡ : ∀ {x y z} {p r : x [ _∼_ ]⁺ y} {q s} →
                   (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → p ≡ r
 ∼⁺⟨⟩-injectiveˡ refl = refl

 ∼⁺⟨⟩-injectiveʳ : ∀ {x y z} {p r : x [ _∼_ ]⁺ y} {q s} →
                   (x [ _∼_ ]⁺ z ∋ x ∼⁺⟨ p ⟩ q) ≡ (x ∼⁺⟨ r ⟩ s) → q ≡ s
 ∼⁺⟨⟩-injectiveʳ refl = refl