# Predecessor function with recursive types

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?

• I'll assume you're trying to study type encodings. Could you please show a more complete source of what you have so far? For example, your definitions of Nat, and isZero. – paulotorrens Dec 19 '19 at 21:39
• I am not well versed with Agda, but will copying church encoding for predecessor help in your case? en.wikipedia.org/wiki/… – Apoorv Jan 9 '20 at 17:13