Algebraic Presentations of Type Dependency

Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North +1

C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formul…