, Sigma types ( x:A)B, (a,b), (Ex,y)(c,d
,
Wx?A)B, sup(a,b) ,
,
Free algebras and automata realizations in the language of categories, Comment. Math. Univ. Carol, vol.015, issue.4, pp.589-602, 1974. ,
Non-wellfounded trees in homotopy type theory, 13th International Conference on Typed Lambda Calculi and Applications, vol.38, pp.17-30, 2015. ,
Univalent categories and the Rezk completion, Math. Struct. Comput. Sci, vol.25, pp.1010-1039, 2015. ,
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. ,
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
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. ,
Inductive types in homotopy type theory, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.95-104, 2012. ,
Substitution: a formal methods case study using monads and transformations, Sci. Comput. Program, vol.23, pp.287-311, 1994. ,
Nested datatypes, Mathematics of Program Construction: 4th International Conference. MPC'98, vol.1422, pp.52-67, 1998. ,
De Bruijn notation as a nested datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999. ,
Generalised folds for nested datatypes, Formal Aspects Comput, vol.11, issue.2, pp.200-222, 1999. ,
Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic, vol.32, pp.209-243, 1986. ,
Mathematical quotients and quotient types in Coq, Types for Proofs and Programs, Second International Workshop, vol.2646, pp.95-107, 2002. ,
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
A small scale reflection extension for the Coq system, 2016. ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
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. ,
Modules over monads and initial semantics, Inf. Comput, vol.208, issue.5, pp.545-564, 2010. ,
The simplicial model of univalent foundations (after Voevodsky), 2016. ,
Categories for the Working Mathematician, Graduate Texts in Mathematics, vol.5, 1998. ,
Intuitionistic Type Theory, Studies in Proof Theory. Bibliopolis, vol.1, 1984. ,
Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, vol.104, pp.153-175, 1982. ,
Substitution in non-wellfounded syntax with variable binding, Theor. Comput. Sci, vol.327, issue.1-2, pp.155-174, 2004. ,
Inductive types and type constraints in the second-order lambda calculus, Ann. Pure Appl. Logic, vol.51, issue.1-2, pp.159-172, 1991. ,
Fixed points of functors, 2003. ,
Strictly Positive Types in Homotopy Type Theory, 2017. ,
, The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.
Resizing rules. Talk at TYPES workshop, 2011. ,
C-system of a module over a monad on sets, 2014. ,
A C-system defined by a universe category, Theory Appl. Categ, vol.30, issue.37, pp.1181-1214, 2015. ,
An experimental library of formalized mathematics based on the univalent foundations, Math. Struct. Comput. Sci, vol.25, pp.1278-1294, 2015. ,