I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction principles).
For example, I'm thinking:
- You can use propositional equality to turn an inductive family into an inductive type with equality constraints on the indices
- You can use Sigma types to encode sums-of-products
You can get inductive types with a fixed-point type:
data Fix : (Type -> Type) -> Type where
Fold : (f : Type -> Type) -> f (Fix f) -> Fix f
which is fine as long as
fis strictly positive.
But I'm not certain that these give you the full power of inductive families, particularly whether
Fix gives you the full power of eliminators/structural recursion for inductive families.
Are there any references on what is sufficient to model inductive families?
I'm aware of:
- W-types, which don't work well in an intensional setting.
- Church-encodings, which aren't powerful enough to prove that (0 != 1), and also don't work well in a predicative setting
- Levitation/datatype-generic-programming, which seems to give you all of inductive families, but at the expense of having to keep a runtime representation of every type, with a lot of complexity related to this representation. This seems like a chainsaw where I need a knife.