A. Abel, J. Öhman, and A. Vezzosi, Decidability of conversion for type theory in type theory, Proc. ACM Program. Lang. 2, POPL, Article 23, p.3158111, 2018.
DOI : 10.1109/LICS.2008.44

A. Abel and G. Scherer, On Irrelevance and Algorithmic Equality in Predicative Type Theory, Logical Methods in Computer Science, vol.15, issue.5/6, pp.29-2012, 2012.
DOI : 10.2168/LMCS-4(3:13)2008

. 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

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

S. Awodey and A. Bauer, Propositions as [Types], Journal of Logic and Computation, vol.14, issue.4, pp.447-471, 2004.
DOI : 10.1093/logcom/14.4.447

S. Boulier, P. Pédrot, and N. Tabareau, The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp.182-194, 2017.
DOI : 10.1109/LICS.1989.39193

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

E. Brady, C. Mcbride, and J. Mckinna, Inductive Families Need Not Store Their Indices, Types for Proofs and Programs, pp.115-129, 2004.
DOI : 10.1007/978-3-540-24849-1_8

P. Capriotti, Models of type theory with strict equality, 2017.

J. Cockx and A. Abel, Elaborating dependent (co)pattern matching, Proceedings of the 23th ACM SIGPLAN Conference on Functional Programming, 2018.
DOI : 10.1145/1328438.1328482

J. Cockx and D. Devriese, Abstract, Journal of Functional Programming, vol.28, 2018.
DOI : 10.1016/0890-5401(91)90066-B

J. Cockx, D. Devriese, and F. Piessens, Pattern matching without K, ACM SIGPLAN Notices, vol.49, issue.9, pp.257-268, 2014.
DOI : 10.1007/978-3-642-38946-7_14

. Thierry-coquand, Universe of Bishop sets, 2016.

P. Dybjer, Internal type theory, Types for Proofs and Programs, pp.120-134, 1996.
DOI : 10.1007/3-540-61780-9_66

M. Hofmann, Conservativity of equality reflection over intensional type theory, International Workshop on Types for Proofs and Programs, pp.153-164, 1995.
DOI : 10.1007/3-540-61780-9_68

P. Letouzey, Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004.

C. Mangin and M. Sozeau, Equations Reloaded, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01671777

P. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium '73, pp.73-118, 1975.
DOI : 10.1016/S0049-237X(08)71945-1

F. Pfenning, Intensionality, extensionality, and proof irrelevance in modal type theory, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, p.221, 2001.
DOI : 10.1109/LICS.2001.932499

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

V. Voevodsky, Resising Rules -their use and semantic justification. www.math.ias, 2011.

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

B. Werner, On the Strength of Proof-Irrelevant Type Theories, pp.1-20, 2008.

A. Lean, Type axiom r : A ? A ? Prop