But anyhow, the impact of this observation about W-types (infinitely many implementations of zero, all provably equal but definitionally distinct), is just that we need a slightly larger base set of types from which to work. Whatever the base set, we apply the same technique to compute the meaning of equations.

In Epigram 2, we don’t take W-types as the primitive source of inductive structure. Instead, we supply a universe of inductive types, giving first-order data a first-order representation. We’ve just written a paper about it: The Gentle Art of Levitation.

]]>