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))