Skip to content

Instantly share code, notes, and snippets.

@copumpkin
Last active October 27, 2018 11:19
Show Gist options
  • Save copumpkin/2702816 to your computer and use it in GitHub Desktop.
Save copumpkin/2702816 to your computer and use it in GitHub Desktop.
{-# 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
@copumpkin
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment