The syntax is a bit peculiar, but they defined the union type Nat, defined the function + which takes two Nats and returns a Nat (which they defined in a thorou

The syntax is a bit peculiar, but they defined the union type Nat, defined the function + which takes two Nats and returns a Nat (which they defined in a thoroughly confusing point-free way because the language is concatenative), and demonstrated the associativity of +. If you read any introduction to dependent types, they will do this.