[ re #184 ] Axiom.UIP (#630)

CHANGELOG.md

@@ -342,6 +342,9 @@ List of new modules
 
   Algebra.FunctionProperties.Consequences.Propositional
 
+  Axiom.UIP
+  Axiom.UIP.WithK
+
   Codata.Cowriter
 
   Codata.M.Properties
@@ -1157,8 +1160,6 @@ Other minor additions
   trans-injectiveˡ : trans p₁ q ≡ trans p₂ q → p₁ ≡ p₂
   trans-injectiveʳ : trans p q₁ ≡ trans p q₂ → q₁ ≡ q₂
   subst-injective  : subst P x≡y p ≡ subst P x≡y q → p ≡ q
-  module Constant⇒UIP
-  module Decidable⇒UIP
   ```
 
 * Added new proofs to `Relation.Binary.Consequences`:

README.agda

@@ -46,6 +46,10 @@ module README where
 --     properties needed to specify these structures (associativity,
 --     commutativity, etc.), and operations on and proofs about the
 --     structures.
+-- • Axiom
+--     The consequences of assuming various additional axioms
+--     e.g. uniqueness of identity of proofs, function extensionality,
+--     excluded middle.
 -- • Category
 --     Category theory-inspired idioms used to structure functional
 --     programs (functors and monads, for instance).
@@ -120,7 +124,7 @@ import Category.Monad        -- Monads.
 import Relation.Binary.PropositionalEquality
 
 -- Convenient syntax for "equational reasoning" using a preorder:
-import Relation.Binary.PreorderReasoning
+import Relation.Binary.Reasoning.Preorder
 
 -- Solver for commutative ring or semiring equalities:
 import Algebra.Solver.Ring

src/Axiom/UIP.agda

@@ -0,0 +1,70 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Results concerning uniqueness of identity proofs
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Axiom.UIP where
+
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality.Core
+
+------------------------------------------------------------------------
+-- 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} _≡_
+
+------------------------------------------------------------------------
+-- UIP always holds when using axiom K (see `Axiom.UIP.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
+  ... | yes p = p
+  ... | no ¬p = ⊥-elim (¬p a≡b)
+
+  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
+  ≡-normalise-constant {a} {b} p q with a ≟ b
+  ... | yes _ = refl
+  ... | no ¬p = ⊥-elim (¬p p)
+
+  ≡-irrelevant : UIP A
+  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant

src/Axiom/UIP/WithK.agda

@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Results concerning uniqueness of identity proofs, with K axiom
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K --safe #-}
+
+module Axiom.UIP.WithK where
+
+open import Axiom.UIP
+open import Relation.Binary.PropositionalEquality.Core
+
+-- K implies UIP.
+
+uip : ∀ {a A} → UIP {a} A
+uip refl refl = refl

src/Data/Nat/Properties.agda

@@ -11,6 +11,7 @@
 
 module Data.Nat.Properties where
 
+open import Axiom.UIP
 open import Algebra
 open import Algebra.Morphism
 open import Function

src/Relation/Binary/PropositionalEquality.agda

@@ -15,6 +15,7 @@ open import Data.Empty
 open import Data.Product
 open import Relation.Nullary using (yes ; no)
 open import Relation.Unary using (Pred)
+open import Axiom.UIP
 open import Relation.Binary
 open import Relation.Binary.Indexed.Heterogeneous
   using (IndexedSetoid)
@@ -33,10 +34,6 @@ subst₂ : ∀ {a b p} {A : Set a} {B : Set b} (P : A → B → Set p)
          {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂
 subst₂ P refl refl p = p
 
-cong : ∀ {a b} {A : Set a} {B : Set b}
-       (f : A → B) {x y} → x ≡ y → f x ≡ f y
-cong f refl = refl
-
 cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
            f ≡ g → (x : A) → f x ≡ g x
 cong-app refl x = refl
@@ -121,32 +118,6 @@ inspect f x = [ refl ]
 -- f x y with g x | inspect g x
 -- f x y | c z | [ eq ] = ...
 
-------------------------------------------------------------------------
--- Convenient syntax for equational reasoning
-
--- This is special instance of Relation.Binary.EqReasoning.
--- Rather than instantiating the latter with (setoid A),
--- we reimplement equation chains from scratch
--- since then goals are printed much more readably.
-
-module ≡-Reasoning {a} {A : Set a} where
-
-  infix  3 _∎
-  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
-  infix  1 begin_
-
-  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
-  begin_ x≡y = x≡y
-
-  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
-  _ ≡⟨⟩ x≡y = x≡y
-
-  _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
-  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
-
-  _∎ : ∀ (x : A) → x ≡ x
-  _∎ _ = refl
-
 ------------------------------------------------------------------------
 -- Functional extensionality
 
@@ -191,19 +162,6 @@ module _ {a} {A : Set a} {x y : A} where
 ------------------------------------------------------------------------
 -- Various equality rearrangement lemmas
 
-  trans-reflʳ : (p : x ≡ y) → trans p refl ≡ p
-  trans-reflʳ refl = refl
-
-  trans-assoc : ∀ {z u : A} (p : x ≡ y) {q : y ≡ z} {r : z ≡ u} →
-                trans (trans p q) r ≡ trans p (trans q r)
-  trans-assoc refl = refl
-
-  trans-symˡ : (p : x ≡ y) → trans (sym p) p ≡ refl
-  trans-symˡ refl = refl
-
-  trans-symʳ : (p : x ≡ y) → trans p (sym p) ≡ refl
-  trans-symʳ refl = refl
-
   trans-injectiveˡ : ∀ {z} {p₁ p₂ : x ≡ y} (q : y ≡ z) →
                      trans p₁ q ≡ trans p₂ q → p₁ ≡ p₂
   trans-injectiveˡ refl = subst₂ _≡_ (trans-reflʳ _) (trans-reflʳ _)
@@ -288,38 +246,6 @@ cong-≡id {f = f} {x} f≡id =
   where
   open ≡-Reasoning
 
-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 : Irrelevant {A = 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
-
-module Decidable⇒UIP
-       {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A}))
-       where
-
-  ≡-normalise : _≡_ {A = A} ⇒ _≡_
-  ≡-normalise {a} {b} a≡b with a ≟ b
-  ... | yes p = p
-  ... | no ¬p = ⊥-elim (¬p a≡b)
-
-  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
-  ≡-normalise-constant {a} {b} p q with a ≟ b
-  ... | yes _ = refl
-  ... | no ¬p = ⊥-elim (¬p p)
-
-  ≡-irrelevant : Irrelevant {A = A} _≡_
-  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant
-
 module _ {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) {a : A} where
 
   ≡-≟-identity : ∀ {b} (eq : a ≡ b) → a ≟ b ≡ yes eq

src/Relation/Binary/PropositionalEquality/Core.agda

@@ -39,6 +39,9 @@ module _ {a} {A : Set a} where
   subst : ∀ {p} → Substitutive {A = A} _≡_ p
   subst P refl p = p
 
+  cong : ∀ {b} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
+  cong f refl = refl
+
   respˡ : ∀ {ℓ} (∼ : Rel A ℓ) → ∼ Respectsˡ _≡_
   respˡ _∼_ refl x∼y = x∼y
 
@@ -54,3 +57,47 @@ module _ {a} {A : Set a} where
     ; sym   = sym
     ; trans = trans
     }
+
+------------------------------------------------------------------------
+-- Various equality rearrangement lemmas
+
+module _ {a} {A : Set a} {x y : A} where
+
+  trans-reflʳ : (p : x ≡ y) → trans p refl ≡ p
+  trans-reflʳ refl = refl
+
+  trans-assoc : ∀ {z u} (p : x ≡ y) {q : y ≡ z} {r : z ≡ u} →
+    trans (trans p q) r ≡ trans p (trans q r)
+  trans-assoc refl = refl
+
+  trans-symˡ : (p : x ≡ y) → trans (sym p) p ≡ refl
+  trans-symˡ refl = refl
+
+  trans-symʳ : (p : x ≡ y) → trans p (sym p) ≡ refl
+  trans-symʳ refl = refl
+
+------------------------------------------------------------------------
+-- Convenient syntax for equational reasoning
+
+-- This is special instance of Relation.Binary.EqReasoning.
+-- Rather than instantiating the latter with (setoid A),
+-- we reimplement equation chains from scratch
+-- since then goals are printed much more readably.
+
+module ≡-Reasoning {a} {A : Set a} where
+
+  infix  3 _∎
+  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
+  infix  1 begin_
+
+  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
+  begin_ x≡y = x≡y
+
+  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
+  _ ≡⟨⟩ x≡y = x≡y
+
+  _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
+  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
+
+  _∎ : ∀ (x : A) → x ≡ x
+  _∎ _ = refl

src/Relation/Binary/PropositionalEquality/WithK.agda

@@ -9,14 +9,15 @@
 
 module Relation.Binary.PropositionalEquality.WithK where
 
+open import Axiom.UIP.WithK
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
 
 ------------------------------------------------------------------------
 -- Proof irrelevance
 
-≡-irrelevant : ∀ {a} {A : Set a} → Irrelevant (_≡_ {A = A})
-≡-irrelevant refl refl = refl
+≡-irrelevant : ∀ {a} {A : Set a} → Irrelevant {A = A} _≡_
+≡-irrelevant = uip
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES