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