Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Midpoints.agda: proof of equivalence for a HIT (for Cale)
{-# OPTIONS --without-K #-}
module 2013-06-26-midpoints where
{-
This is a proof that the HIT
data S A where
[_] : A -> S A;
mid : {x y : A} -> Id x y -> Id [ x ] [ y ]
sheet: {x y : x} -> (p : Id x y) -> Id (mid p) (cong [ _ ] p)
is equivalent to A. Using lots of postulates :)
-}
open import Level
open import Function
open import Relation.Binary.PropositionalEquality
postulate
-- stuff about paths
Id : {b} {B : Set b} B B Set
refl' : {la} {A : Set la} {x : A} Id x x
cong' : {la lb} {A : Set la} {B : Set lb} (f : A B) {x y}
Id x y Id (f x) (f y)
subst' : {la lb} {A : Set la} (B : A Set lb) {x y}
Id x y B x B y
hcong' : {la lb} {A : Set la} {B : A Set lb} (f : (x : A) B x) {x y}
(x=y : Id x y) Id (subst' B x=y (f x)) (f y)
-- computation rule for cong
cong'-id : {A : Set} {x y : A} {x=y} x=y ≡ cong' (\x x) {x} {y} x=y
-- our type
S : Set Set
fw : {A : Set} A S A
-- induction
ind-S : {lb : Level} {A : Set} {B : Set lb}
(f : A B)
(m : {x y : A} Id x y Id (f x) (f y))
(s : {x y : A} (x=y : Id x y) Id (m x=y) (cong' f x=y))
S A B
-- dependent induction
ind-S' : {lb : Level} {A : Set} {B : S A Set lb}
(f : (x : A) B (fw x))
(m : {x y : A} (x=y : Id x y) Id (subst' (B ∘ fw) x=y (f x)) (f y))
(s : {x y : A} (x=y : Id x y) Id (m x=y) (hcong' f x=y))
(u : S A) B u
-- computation of induction
comp-ind-S : {lb : Level} {A : Set} {B : Set lb}
{f : A B}
{m : {x y : A} Id x y Id (f x) (f y)}
{s : {x y : A} (x=y : Id x y) Id (m x=y) (cong' f x=y)}
{u : A} ind-S f m s (fw u) ≡ f u
mcong' : {la lb} {A : Set la} {B : Set lb} (f : A B) {x y} x ≡ y Id (f x) (f y)
mcong' f refl = refl'
bw : {A : Set} S A A
bw {A} = ind-S {B = A} (\x x) (\x=y x=y) (\x=y subst (Id _) cong'-id refl')
bw-fw-T : {A : Set} S A Set
bw-fw-T {A} = ind-S {A = A} {B = Set} f (\x=y cong' f x=y) (\x=y refl')
where f = (\(x : A) Id (bw (fw x)) x)
bw-fw : {A : Set} -> (x : A) -> Id (bw (fw x)) x
bw-fw {A} x = subst id comp-ind-S $
ind-S' {A = A} {B = bw-fw-T}
-- manually apply some computation rules:
(\x subst id (sym $ comp-ind-S {f = \(x : A) Id (bw (fw x)) x} {u = x}) $
subst (flip Id x) (sym $ comp-ind-S {f = id} {u = x}) refl')
_
(\x=y refl')
(fw x)
fw-bw : {A : Set} -> (sx : S A) -> Id (fw (bw sx)) sx
fw-bw {A} = ind-S' {A = A} {B = \x Id (fw (bw x)) x}
(\x mcong' fw comp-ind-S)
_
(\x=y refl')
-- now we have an isomorphism (fw,bw,bw-fw,fw-bw), so also an equivalence.
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.