The goal of this line of work is to find an essentially algebraic formulation of dependent type theory. This automatically provides free models and quotients. The syntax will then be the initial model.

Rijke’s E-systems are a generalization of Voevodsky’s B-systems.