I am defining the type
Nat of natural numbers a recursive sum type:
$$ Nat = \mu X. Unit \oplus X$$
Now, I have defined
zero as the term:
zero : Nat zero = fold Nat (Inl tmUnit tyNat tyUnit)
and successor as
succ : Nat -> Nat succ n = fold Nat (tmInr n tyNat tyUnit)
Please note, that I am not completely sure of these two implementations; they might be wrong - I accept comments on them too.
Now, my question: I want to implement a predecessor function. I have both an
isZero function and an
if-then-else construct. How could I to this?