, Sigma types ( x:A)B, (a,b), (Ex,y)(c,d

. ·-·-·,

. W-types, Wx?A)B, sup(a,b)

U. Universes,

J. Adámek, Free algebras and automata realizations in the language of categories, Comment. Math. Univ. Carol, vol.015, issue.4, pp.589-602, 1974.

B. Ahrens, P. Capriotti, and R. Spadotti, Non-wellfounded trees in homotopy type theory, 13th International Conference on Typed Lambda Calculi and Applications, vol.38, pp.17-30, 2015.

B. Ahrens, K. Kapulkin, and M. Shulman, Univalent categories and the Rezk completion, Math. Struct. Comput. Sci, vol.25, pp.1010-1039, 2015.

B. Ahrens and R. Matthes, Heterogeneous substitution systems revisited, Uustalu, T. (ed.) 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), 2018.

B. Ahrens and J. Zsidó, Initial semantics for higher-order typed syntax in Coq, J. Formal. Reason, vol.4, issue.1, pp.25-69, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01329572

T. Altenkirch and B. Reus, Monadic presentations of lambda terms using generalized inductive types, Computer Science Logic: 13th International Workshop. CSL'99, 8th Annual Conference of the EACSL, pp.453-468, 1999.

S. Awodey, N. Gambino, and K. Sojakova, Inductive types in homotopy type theory, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.95-104, 2012.

F. Bellegarde and J. Hook, Substitution: a formal methods case study using monads and transformations, Sci. Comput. Program, vol.23, pp.287-311, 1994.

R. Bird and L. Meertens, Nested datatypes, Mathematics of Program Construction: 4th International Conference. MPC'98, vol.1422, pp.52-67, 1998.

R. Bird and R. Paterson, De Bruijn notation as a nested datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999.

R. Bird and R. Paterson, Generalised folds for nested datatypes, Formal Aspects Comput, vol.11, issue.2, pp.200-222, 1999.

J. Cartmell, Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic, vol.32, pp.209-243, 1986.

L. Chicli, L. Pottier, and C. Simpson, Mathematical quotients and quotient types in Coq, Types for Proofs and Programs, Second International Workshop, vol.2646, pp.95-107, 2002.

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical type theory: a constructive interpretation of the univalence axiom, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01378906

G. Gonthier, A. Mahboubi, and E. Tassi, A small scale reflection extension for the Coq system, 2016.
URL : https://hal.archives-ouvertes.fr/inria-00258384

A. Hirschowitz and M. Maggesi, Modules over monads and linearity. In: Logic, Language, Information and Computation, 14th International Workshop, Lecture Notes in Computer Science, vol.4576, pp.218-237, 2007.

A. Hirschowitz and M. Maggesi, Modules over monads and initial semantics, Inf. Comput, vol.208, issue.5, pp.545-564, 2010.

K. Kapulkin and P. L. Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), 2016.

M. Lane and S. , Categories for the Working Mathematician, Graduate Texts in Mathematics, vol.5, 1998.

P. Martin-löf, Intuitionistic Type Theory, Studies in Proof Theory. Bibliopolis, vol.1, 1984.

P. Martin-löf, Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, vol.104, pp.153-175, 1982.

R. Matthes and T. Uustalu, Substitution in non-wellfounded syntax with variable binding, Theor. Comput. Sci, vol.327, issue.1-2, pp.155-174, 2004.

N. P. Mendler, Inductive types and type constraints in the second-order lambda calculus, Ann. Pure Appl. Logic, vol.51, issue.1-2, pp.159-172, 1991.

F. Métayer, Fixed points of functors, 2003.

F. Rech, Strictly Positive Types in Homotopy Type Theory, 2017.

, The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.

V. Voevodsky, Resizing rules. Talk at TYPES workshop, 2011.

V. Voevodsky, C-system of a module over a monad on sets, 2014.

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

V. Voevodsky, An experimental library of formalized mathematics based on the univalent foundations, Math. Struct. Comput. Sci, vol.25, pp.1278-1294, 2015.