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.
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
Type. Inductives in
Prop may behave slightly differently.