------------------------------------------------------------------------ -- The Agda standard library -- -- Results concerning uniqueness of identity proofs ------------------------------------------------------------------------ {-# OPTIONS --without-K --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