module maybe_nat where
-- by @esmolanka
-- here is simple one tweet equality sample with transport
-- Nat ~ Fix Maybe
-- Z ~ Nothing
-- S ~ Fix . Just
import nat
import maybe
import control
import recursion
import proto
import path
import set
import iso
three: fix maybe = Fix (just (Fix (just (Fix (just (Fix nothing))))))
natToMaybe: nat -> fix maybe = split
zero -> Fix nothing
succ n -> Fix (just (natToMaybe n))
maybeToNat: fix maybe -> nat = split
Fix m -> go m where go: maybe (fix maybe) -> nat = split
nothing -> zero
just f -> succ (maybeToNat f)
natMaybeIso: (a: nat) -> Path nat (maybeToNat (natToMaybe a)) a = split
zero -> * zero
succ n -> ** succ (natMaybeIso n @ i)
maybeNatIso : (a : fix maybe) -> Path (fix maybe) (natToMaybe (maybeToNat a)) a = split
Fix m -> go m where go: (a: maybe (fix maybe)) -> Path (fix maybe) (natToMaybe (maybeToNat (Fix a))) (Fix a) = split
nothing -> ** Fix nothing
just f -> ** Fix (just (maybeNatIso f @ i))
maybenat: Path U (fix maybe) nat = isoPath (fix maybe) nat maybeToNat natToMaybe natMaybeIso maybeNatIso
HeteroEqu (A B:U)(a:A)(b:B)(P:Path U A B):U = PathP P a b
-- > HeteroEqu (fix maybe) nat (Fix nothing) zero maybenat
-- > transNeg (fix maybe) (nat) maybenat (succ (succ zero))
-- EVAL: Fix (just (Fix (just (Fix nothing))))
-- > trans (fix maybe) (nat) maybenat (Fix nothing)
-- EVAL: zero
-- import univalence
-- natEquiv : isEquiv nat (fix maybe) natToMaybe =
-- isoToEquiv
-- nat (fix maybe)
-- natToMaybe maybeToNat
-- maybeNatIso natMaybeIso
-- natEq : Path U nat (fix maybe) =
-- ua nat (fix maybe) (natToMaybe, natEquiv)
-- > transport natEq (succ (succ zero))
-- EVAL: Fix (just (Fix (just (Fix nothing))))
-- > transport (** natEq @ -i) (Fix (just (Fix (just (Fix (just (Fix nothing)))))))
-- EVAL: succ (succ (succ zero))
*