nat = fix maybe

natMaybeEq.ctt

import prelude
import equiv

data nat
  = zero
  | suc (n : nat)

data fix (f : U -> U) = mk (x : f (fix f))

data maybe (A : U)
  = nothing
  | just (a : A)

three : fix maybe = mk (just (mk (just (mk (just (mk nothing))))))

natToMaybe : nat -> fix maybe = split
  zero -> mk nothing
  suc n -> mk (just (natToMaybe n))

maybeToNat : fix maybe -> nat = split
  mk m -> go m
   where
    go : maybe (fix maybe) -> nat = split
       nothing -> zero
       just f -> suc (maybeToNat f)

natMaybeIso : (a : nat) -> Path nat (maybeToNat (natToMaybe a)) a = split
  zero -> <i> zero
  suc n -> <i> suc (natMaybeIso n @ i)

maybeNatIso : (a : fix maybe) -> Path (fix maybe) (natToMaybe (maybeToNat a)) a = split
  mk m -> go m
   where
    go : (a : maybe (fix maybe)) -> Path (fix maybe) (natToMaybe (maybeToNat (mk a))) (mk a) = split
      nothing -> <i> mk nothing
      just f -> <i> mk (just (maybeNatIso f @ i))

natEquiv : isEquiv nat (fix maybe) natToMaybe =
  isoToEquiv
    nat (fix maybe)
    natToMaybe maybeToNat
    maybeNatIso natMaybeIso

ua (A B : U) (e : equiv A B) : Path U A B =
  <i> Glue B [ (i = 0) -> (A,e), (i = 1) -> (B,idEquiv B) ]

natEq : Path U nat (fix maybe) =
   ua nat (fix maybe) (natToMaybe, natEquiv)

-- > transport natEq (suc (suc zero))
-- EVAL: mk (just (mk (just (mk nothing))))
-- > transport (<i> natEq @ -i) (mk (just (mk (just (mk (just (mk nothing)))))))
-- EVAL: suc (suc (suc zero))