------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning uniqueness of identity proofs
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Axiom.UniquenessOfIdentityProofs where

open import Level using (Level)
open import Relation.Nullary.Decidable.Core
  using (recompute; recompute-constant)
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Definitions
  using (Sym; Irrelevant; DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; trans; sym; cong)
open import Relation.Binary.PropositionalEquality.Properties

private
  variable
    a : Level
    A : Set a
    x y : A

------------------------------------------------------------------------
-- 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 : 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
  (f : _≡_ {A = A} ⇒ _≡_)
  (f-constant : ∀ {x y} (p q : x ≡ y) → f p ≡ f q)
  where

  ≡-canonical : (p : x ≡ y) → 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 (_≟_ : DecidableEquality A)
  where

  ≡-normalise : _≡_ {A = A} ⇒ _≡_
  ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y

  ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q
  ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≟ y)

  ≡-irrelevant : UIP A
  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant