Fixed set of type constructors to simulate all intensional inductive families? 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 -&gt; Type) -&gt; Type where
  Fold : (f : Type -&gt; Type) -&gt; f (Fix f) -&gt; Fix f

which is fine as long as f is 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.
I am not 100% sure this is what you want, but assuming you are looking for a  type theory with a closed set of type constructors, which can model inductive families, then what you want are indexed containers or dependent polynomial functors. What you should look at first is:


Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride and Peter Morris's 2014 draft Indexed Containers. 

This paper is an expanded version of Altenkirch and Morris's 2009 LICS paper. It is all formalized in Agda, and gives a set of codes for defining all the strictly positive families. If you need it, it also gives an interpretation of them into W-types (and M-types for coinductive families). This is probably what you want to look at first. 

It may also be worth looking at Containers: Constructing Strictly Positive Types by Michael Abbott, Thorsten Altenkirch and Neil Ghani for the non-dependent case.


Category theorists also invented this concept, which they dubbed dependent polynomial functors. The original paper, and some I found helpful for reading it are:


Wellfounded trees and dependent polynomial functors by Nicola Gambino and Martin Hyland. TYPES 2003.
Generalized Polynomial Functors Marcelo Fiore, ICALP 2012. There is a bit more logical intuition in this paper. 
A foundation for GADTs and inductive families: dependent polynomial functor approach. Makoto Hamana and Marcelo Fiore, WGP 2011. This paper shows how to interpret indexed families as polynomial functors. 


Now, you might also ask whether or not inductive families are "the morally correct" syntax for indexed containers. The answer is: probably not, but this is because containers/polynomials are too rich to have an obvious syntax.


Tamara von Glehn's PhD thesis, Polynomials and Models of Dependent Type Theory, builds models of dependent type theory out of polynomial functors. This implies that the correct syntax for datatypes in type theory is type theory itself, and I just don't know how to connect that to language design. Someone should give it a try, though!
Pierre Hyvernat has an LMCS 2014 paper, A Linear Category of Polynomial Functors, which uses a different notion of morphism to give polynomials a monoidal closed structure. So perhaps datatype declarations should be written in a linear type theory?