import Cats.Simp1
import hlevel

record SimpType where
    spine : Nat -> Type
    simp-map : (k n : Nat) -> k ~> n -> spine n -> spine k
  with
    simp-map _ _ (id p) x = transport spine (inv p) x
    simp-map k n (comp m f g) x = simp-map k m f (simp-map m n g x)

Prod : Type -> Type -> Type
Prod A B = Sigma A (\_ -> B)

-- X (suc n) = * X 1 - X n

face0 : (n : Nat) -> zero ~> n
face0 zero = id idp
face0 (suc n) = comp n (face0 n) (face (suc n) (wrap id-le) idp)

face1 : (n : Nat) -> suc zero ~> suc n
face1 zero = id idp
face1 (suc n) = comp (suc n) (face1 n) (face (suc (suc n)) (wrap (wrap id-le)) idp)

face1-left : (n : Nat) -> face0 (suc n) = comp (suc zero) (face (suc zero) (wrap true) idp) (face1 n)
face1-left zero =
    face0 (suc zero)
  ==< idp >==
    comp zero (id idp) (face (suc zero) (wrap id-le) idp)
  ==< path (id-comp (face (suc zero) (wrap true) idp)) >==
    face (suc zero) (wrap id-le) idp
  ==< inv (path (comp-id (face (suc zero) (wrap true) idp))) >==
    comp (suc zero) (face (suc zero) (wrap true) idp) (id idp)
  ==< idp >==
    comp (suc zero) (face (suc zero) (wrap true) idp) (face1 zero)
  !qed
face1-left (suc n) =
    comp (suc n) (face0 (suc n)) (face (suc (suc n)) (wrap (wrap id-le)) idp)
  ==< map (\t -> comp (suc n) t (face (suc (suc n)) (wrap (wrap id-le)) idp)) (face1-left n) >==
    comp (suc n) (comp (suc zero) (face (suc zero) (wrap true) idp) (face1 n)) (face (suc (suc n)) (wrap (wrap id-le)) idp)
  ==< path (comp-comp (suc zero) (suc n) (face (suc zero) (wrap true) idp) (face1 n) (face (suc (suc n)) (wrap (wrap id-le)) idp)) >==
    comp (suc zero) (face (suc zero) (wrap true) idp) (comp (suc n) (face1 n) (face (suc (suc n)) (wrap (wrap id-le)) idp))
  !qed

face1-right : (n : Nat) -> Path (\_ -> zero ~> suc n) (comp (suc zero) (face zero true idp) (face1 n)) (comp n (face0 n) (face zero true idp))
face1-right zero =
    comp (suc zero) (face zero true idp) (face1 zero)
  ==< idp >==
    comp (suc zero) (face zero true idp) (id idp)
  ==< path (comp-id (face zero true idp)) >==
    face zero true idp
  ==< inv (path (id-comp (face zero true idp))) >==
    comp zero (id idp) (face zero true idp)
  ==< idp >==
    comp zero (face0 zero) (face zero true idp)
  !qed
face1-right (suc n) =
    
    comp (suc zero) (face zero true idp) (face1 (suc n))
    
  ==< idp >==
    
    comp (suc zero) (face zero true idp) (comp (suc n) (face1 n) (face (suc (suc n)) (wrap (wrap id-le)) idp))
    
  ==< inv (path (comp-comp (suc zero) (suc n) (face zero true idp) (face1 n) (face (suc (suc n)) (wrap (wrap id-le)) idp))) >==
    
    comp (suc n) (comp (suc zero) (face zero true idp) (face1 n)) (face (suc (suc n)) (wrap (wrap id-le)) idp)
    
  ==< map (\t -> comp (suc n) t (face (suc (suc n)) (wrap (wrap id-le)) idp)) (face1-right n) >==
    
    comp (suc n) (comp n (face0 n) (face zero true idp)) (face (suc (suc n)) (wrap (wrap id-le)) idp)
    
  ==< path (comp-comp n (suc n) (face0 n) (face zero true idp) (face (suc (suc n)) (wrap (wrap id-le)) idp)) >==
    
    comp n (face0 n) (comp (suc n) (face zero true idp) (face (suc (suc n)) (wrap (wrap id-le)) idp))
    
  ==< map (comp n (face0 n)) (path (face-face zero (suc n) true (wrap id-le) idp)) >==
    
    comp n (face0 n) (comp (suc n) (face (suc n) (wrap id-le) idp) (face zero true idp))
    
  ==< inv (path (comp-comp n (suc n) (face0 n) (face (suc n) (wrap id-le) idp) (face zero true idp))) >==
    
    comp (suc n) (comp n (face0 n) (face (suc n) (wrap id-le) idp)) (face zero true idp)
    
  ==< idp >==
    
    comp (suc n) (face0 (suc n)) (face zero true idp)
    
  !qed

Spine : (X : SimpType) -> Nat -> X.spine zero -> Type
Spine _ zero _ = True
Spine X (suc n) r = Sigma (X.spine (suc zero)) (\e ->
    Prod (r = X.simp-map zero (suc zero) (face (suc zero) (wrap true) idp) e)
         (Spine X n (X.simp-map zero (suc zero) (face zero true idp) e)))

getSpine0 : (X : SimpType) (n : Nat) (x : X.spine n) -> Spine X n (X.simp-map zero n (face0 n) x)
getSpine0 X zero x = true
getSpine0 X (suc n) x
    = X.simp-map (suc zero) (suc n) (face1 n) x
    , map (\t -> X.simp-map zero (suc n) t x) (face1-left n)
    , transport (\t -> Spine X n (X.simp-map zero (suc n) t x))
                (inv (face1-right n))
                (getSpine0 X n (X.simp-map n (suc n) (face zero true idp) x))

getSpine : (X : SimpType) (n : Nat) -> X.spine n -> Sigma (X.spine zero) (Spine X n)
getSpine X n x = X.simp-map zero n (face0 n) x, getSpine0 X n x

isEquiv : {X Y : Type} -> (X -> Y) -> Type
isEquiv X Y f = (y : Y) -> isContr (Sigma X (\x -> f x = y))

SegalType = Sigma SimpType (\X -> (n : Nat) -> isEquiv (getSpine X n))