I’m glad you’re interested in this topic; it is one of my favorite areas of study.

Since the type of binary trees is *countable*, they are in bijection with the natural numbers, and can be defined as such. Letting `pair (x y : nat) : nat := 1/2 (x + y) (x + y + 1) + y`

be the Cantor pairing function, we can define `Leaf := 0`

and `Node x y := 1 + pair x y`

.

Since `pair`

is invertible, the induction principle will be provable, though it will only satisfy the expected computation rules/equations up to propositional equality, not definitional equality.

I believe tricks like this work for all finitary types (if they carry data, you can define the skeleton, and then use large eliminations and dependent pairs to stick the data on afterwards), but once you have infinitary inductive arguments (ex. a constructor of type `(nat -> bin) -> bin`

you need at least W-types.

W-types with large eliminations plus dependent pairs (with definitional eta) and equality (with `J`

that computes on `refl`

) are enough to construct most all inductive types with induction principles with definitional computation rules, though the encoding is rather complex.

This includes uniform parameters of any size, mutual inductives in the same predicative sort (`Prop`

messes things up here), small non-uniform parameters, and small induction-recursion.

Inductive types which I don’t believe any encoding just using W-types can have definitional computation rules include constructors like `list bin -> bin`

, or types with a large, non-uniform parameter. These types can however be constructed with propositional computation rules.

Inductive-inductive types probably require function extensionality or UIP to get even propositional computation rules.

Large induction recursion and higher inductive types definitely require strict extensions of the theory.

Everything I’ve said here is mostly about inductives in `Set`

or `Type`

. Inductives in `Prop`

may behave slightly differently.