F. Stuart, R. L. Allen, R. Constable, C. Eaton, L. Kreitz et al., The Nuprl Open Logical Environment, Automated Deduction-CADE-17, 17th International Conference on Automated Deduction, vol.1831, pp.170-176, 2000.

T. Altenkirch, Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158, pp.412-420, 1999.
DOI : 10.1109/lics.1999.782636

URL : http://www.cs.nott.ac.uk/~txa/publ/lics99.pdf

T. Altenkirch, P. Capriotti, and N. Kraus, Extending Homotopy Type Theory with Strict Equality, 2016.

T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification, pp.57-68, 2007.
DOI : 10.1145/1292597.1292608

URL : http://strictlypositive.org/obseqnow.pdf

A. Anand, S. Boulier, C. Cohen, M. Sozeau, and N. Tabareau, Towards Certified Meta-Programming with Typed Template-Coq, Interactive Theorem Proving-9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC, vol.10895, pp.20-39, 2018.
DOI : 10.1007/978-3-319-94821-8_2

URL : https://hal.archives-ouvertes.fr/hal-01809681

D. Annenkov, P. Capriotti, and N. Kraus, Two-Level Type Theory and Applications, 2017.

A. Bauer, G. Gilbert, P. G. Haselwarter, M. Pretnar, and C. Stone, The 'Andromeda' prover, 2016.

J. Bernardy, P. Jansson, and R. Paterson, Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, pp.107-152, 2012.
DOI : 10.1145/1863543.1863592

URL : http://www.soi.city.ac.uk/~ross/papers/pts.pdf

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

M. Bezem, T. Coquand, and S. Huber, A Model of Type Theory in Cubical Sets, 2013.

S. Boulier, P. Pédrot, and N. Tabareau, The Next 700 Syntactical Models of Type Theory, Certified Programs and Proofs-CPP 2017, pp.182-194, 2017.
DOI : 10.1145/3018610.3018620

URL : https://hal.archives-ouvertes.fr/hal-01445835

, The Coq proof assistant reference manual, 2017.

M. Hofmann, Conservativity of equality reflection over intensional type theory, International Workshop on Types for Proofs and Programs, pp.153-164, 1995.

M. Hofmann, Extensional constructs in intensional type theory, 1997.

M. Hofmann and T. Streicher, The Groupoid Interpretation of Type Theory, Twenty-five years of constructive type theory, vol.36, pp.83-111, 1995.

J. and P. Strub, Coq without Type Casts: A Complete Proof of Coq Modulo Theory, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.46, pp.474-489, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01664457

C. Kapulkin and P. Lefanu-lumsdaine, The simplicial model of univalent foundations, 2012.

C. Mcbride, Dependently typed functional programs and their proofs, 2000.

C. Mcbride, Epigram: Practical programming with dependent types, International School on Advanced Functional Programming, pp.130-170, 2004.

U. Norell, Towards a practical programming language based on dependent type theory, vol.32, 2007.

N. Oury, Extensionality in the calculus of constructions, International Conference on Theorem Proving in Higher Order Logics, pp.278-293, 2005.

N. Oury, Egalité et filtrage avec types dépendants dans le calcul des constructions inductives, Ph.D. Dissertation, 2006.

M. Sozeau, Program-ing Finger Trees in Coq, ICFP'07, pp.13-24, 2007.

M. Sozeau, Equations: A Dependent Pattern-Matching Compiler, Interactive Theorem Proving, First International Conference, ITP 2010, vol.6172, pp.419-434, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00628862

T. Streicher, Investigations into intensional type theory, 1993.

, The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.

F. Van-doorn, H. Geuvers, and F. Wiedijk, Explicit convertibility proofs in pure type systems, Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & metalanguages: theory & practice. ACM, pp.25-36, 2013.

V. Voevodsky, A simple type system with two identity types, 2013.