-- 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)

  ≡-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 
    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} _≡_)

  ≡-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