Skip to content

Instantly share code, notes, and snippets.

@copumpkin copumpkin/Unique.agda
Last active Oct 27, 2018

Embed
What would you like to do?
{-# 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 (xy)) 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

This comment has been minimized.

Copy link
Owner Author

copumpkin commented Feb 12, 2016

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
You can’t perform that action at this time.