------------------------------------------------------------------------
-- 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
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4