Unique.agda

{-# OPTIONS --without-K #-}
module Unique where

open import Level
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module Unique {a} {A : Set a} (_≟_ : (x y : A) → Dec (x ≡ y)) where
  squish : {x y : A} → x ≡ y → x ≡ y
  squish {x} {y} eq with x ≟ y
  squish _  | yes p = p
  squish eq | no ¬p = ⊥-elim (¬p eq)

  squish-constant : {x y : A} (p q : x ≡ y) → squish p ≡ squish q
  squish-constant {x} {y} p q with x ≟ y
  squish-constant p q | yes eq = refl
  squish-constant p q | no ¬eq = ⊥-elim (¬eq q)

  comp : {x y z : A} (p : x ≡ y) (q : x ≡ z) → y ≡ z
  comp p q = trans (sym p) q

  comp-refl : {x y : A} (p : x ≡ y) → comp p p ≡ refl
  comp-refl refl = refl

  unsquish : {x y : A} → x ≡ y → x ≡ y
  unsquish eq = comp (squish refl) eq

  inv : {x y : A} (p : x ≡ y) → unsquish (squish p) ≡ p
  inv {x} refl with x ≟ x
  inv refl | yes p = comp-refl p
  inv refl | no ¬p = ⊥-elim (¬p refl)

  proof : {x y : A} (p q : x ≡ y) → p ≡ q
  proof p q = trans (sym (inv p)) (trans (cong (trans (sym (squish refl))) (squish-constant p q)) (inv q))

open Unique

I vaguely remember translating this argument from elsewhere, but I can't remember where now.