Last active
December 19, 2015 00:59
-
-
Save twanvl/5873090 to your computer and use it in GitHub Desktop.
Midpoints.agda: proof of equivalence for a HIT (for Cale)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# 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