B. Ahrens, K. Kapulkin, and M. Shulman, Univalent categories and the Rezk completion, Mathematical Structures in Computer Science, vol.20, issue.05, pp.1010-103910, 2015.
DOI : 10.1016/j.indag.2013.09.002

T. Altenkirch, J. Chapman, and T. Uustalu, Monads need not be endofunctors, Logical Methods in Computer Science, vol.11, issue.11, pp.2015-2025
DOI : 10.1007/978-3-642-12032-9_21
URL : http://arxiv.org/abs/1412.7148

S. Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, vol.177, pp.1-4610, 2016.
DOI : 10.1017/S0305004112000394

J. Cartmell, Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic, vol.32, 1978.
DOI : 10.1016/0168-0072(86)90053-9
URL : http://doi.org/10.1016/0168-0072(86)90053-9

J. Cartmell, Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic, vol.32, issue.86, pp.209-24310, 1986.
DOI : 10.1016/0168-0072(86)90053-9
URL : http://doi.org/10.1016/0168-0072(86)90053-9

P. Dybjer, Internal type theory, Types for Proofs and Programs, International Workshop TYPES'95, pp.120-134, 1995.
DOI : 10.1007/3-540-61780-9_66

M. Fiore, Discrete generalised polynomial functors, 2012. Slides from talk given at ICALP 2012
DOI : 10.1007/978-3-642-31585-5_22

M. Hofmann, Syntax and semantics of dependent types, Semantics and Logics of Computation, pp.79-130, 1997.

A. William and . Howard, The formulae-as-types notion of construction

. Hindley and H. B. To, Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.479-490, 1980.

A. M. Pitts, Categorical logic Handbook of Logic in Computer Science Algebraic and Logical Structures, pp.39-128, 2000.

. Benno-van-den, R. Berg, and . Garner, Topological and simplicial models of identity types, ACM Trans. Comput. Logic, vol.133, issue.1, pp.1-3, 2012.

V. Voevodsky, A C-system defined by a universe category, Theory Appl. Categ, vol.303037, issue.37, pp.1181-121530, 2015.

V. Voevodsky, An experimental library of formalized Mathematics based on the univalent foundations, Mathematical Structures in Computer Science, vol.25, issue.05, pp.1278-1294
DOI : 10.1016/0890-5401(88)90005-3

V. Voevodsky, Subsystems and regular quotients of C-systems, Conference on Mathematics and its Applications number 658 in Contemporary Mathematics, pp.127-137, 2016.
DOI : 10.1090/conm/658/13124

V. Voevodsky, B. Ahrens, and D. Grayson, URL: https://github