Midpoints.agda: proof of equivalence for a HIT (for Cale)

2013-06-26-midpoints.agda

{-# 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.