Notes on W Types and Inductive Types

Table of Contents Well-Founded Trees Example: Ordinals with a twist Indexed Well-Founded Trees Example: Mutual inductives - even and odd naturals Example: Nonuniformly parametrized inductive - accessibility predicate Example: Nonuniformly parametrized inductive - perfect trees Indexed Inductives and Fording Example: Function images Example: The finite sets Nested Inductives Example: Finitely branching trees Non-example: Truly nested inductive - bushes Inductive–Inductives Example: ...