 # Recursive types what is possible?

#1

I am trying to understand what is possible with recursive types and what not. I read the docs and I think I do understand how to define a recursive type and how to manually construct instances:

``````let Nat = ∀(Nat_ : Type) → ∀(Zero_ : Nat_) → ∀(Succ_ : Nat_ → Nat_) → Nat_

let Zero
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) → Zero_

let One
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) →  Succ_ Zero_

let Two
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) →  Succ_ (Succ_ Zero_)

in Two
``````

However what I do not know, is it possible to define a function

``````let Succ : Nat -> Nat = ...
``````

such that e.g.

``````assert Two === Succ One
``````

holds?

The real use case I am interested in is to define trees and graft trees together that might be defined in different files.

#2

I found it out:

``````let Nat = ∀(Nat_ : Type) → ∀(Zero_ : Nat_) → ∀(Succ_ : Nat_ → Nat_) → Nat_

let Zero
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) → Zero_

let One
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) →  Succ_ Zero_

let Succ =
\(n : Nat) -> \(Nat_ : Type) -> \(Zero_ : Nat_) -> \(Succ_ : Nat_ -> Nat_) ->
Succ_ (n Nat_ Zero_ Succ_)

let Two
: Nat
= λ(Nat_ : Type) → λ(Zero_ : Nat_) → λ(Succ_ : Nat_ → Nat_) →  Succ_ (Succ_ Zero_)

in assert : Two === Succ (Succ Zero)

``````