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