Skip to content

Instantly share code, notes, and snippets.

@twanvl
Last active December 19, 2015 00:59
Show Gist options
  • Save twanvl/5873090 to your computer and use it in GitHub Desktop.
Save twanvl/5873090 to your computer and use it in GitHub Desktop.
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