{-# 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
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.PropositionalEquality.Properties
private
variable
a : Level
A : Set a
x y : A
UIP : (A : Set a) → Set a
UIP A = Irrelevant {A = A} _≡_
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
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