------------------------------------------------------------------------ -- The Agda standard library -- -- Results concerning uniqueness of identity proofs ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Axiom.UniquenessOfIdentityProofs where open import Data.Bool.Base using (true; false) open import Data.Empty open import Relation.Nullary.Reflects using (invert) open import Relation.Nullary hiding (Irrelevant) open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality.Core open import Relation.Binary.PropositionalEquality.Properties ------------------------------------------------------------------------ -- Definition -- -- Uniqueness of Identity Proofs (UIP) states that all proofs of -- equality are themselves equal. In other words, the equality relation -- is irrelevant. Here we define UIP relative to a given type. UIP : ∀ {a} (A : Set a) → Set a UIP A = Irrelevant {A = A} _≡_ ------------------------------------------------------------------------ -- Properties -- UIP always holds when using axiom K -- (see `Axiom.UniquenessOfIdentityProofs.WithK`). -- The existence of a constant function over proofs of equality for -- elements in A is enough to prove UIP for A. Indeed, we can relate any -- proof to its image via this function which we then know is equal to -- the image of any other proof. module Constant⇒UIP {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_) (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q) where ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p ≡-canonical refl = trans-symˡ (f refl) ≡-irrelevant : UIP A ≡-irrelevant p q = begin p ≡⟨ sym (≡-canonical p) ⟩ trans (sym (f refl)) (f p) ≡⟨ cong (trans _) (f-constant p q) ⟩ trans (sym (f refl)) (f q) ≡⟨ ≡-canonical q ⟩ q ∎ where open ≡-Reasoning -- If equality is decidable for a given type, then we can prove UIP for -- that type. Indeed, the decision procedure allows us to define a -- function over proofs of equality which is constant: it returns the -- proof produced by the decision procedure. module Decidable⇒UIP {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_) where ≡-normalise : _≡_ {A = A} ⇒ _≡_ ≡-normalise {a} {b} a≡b with a ≟ b ... | true because [p] = invert [p] ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b) ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q ≡-normalise-constant {a} {b} p q with a ≟ b ... | true because _ = refl ... | false because [¬p] = ⊥-elim (invert [¬p] p) ≡-irrelevant : UIP A ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant