A. Abel, J. Öhman, and A. Vezzosi, Decidability of Conversion for Type Theory in Type Theory, Proc. ACM Program, vol.23, 2018.

A. Abel and G. Scherer, On Irrelevance and Algorithmic Equality in Predicative Type Theory, Logical Methods in Computer Science, vol.8, p.1, 2012.

T. Altenkirch, Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158, 1999.

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

S. Awodey and A. Bauer, , 2004.

, J. Log. and Comput, vol.14, pp.447-471, 2004.

S. Boulier, P. Pédrot, and N. Tabareau, The Next 700 Syntactical Models of Type Theory, Proceedings of Certified Programs and Proofs, pp.182-194, 2017.
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.

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.

J. Cockx and D. Devriese, Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory, Journal of Functional Programming, vol.28, 2018.

J. Cockx, D. Devriese, and F. Piessens, Pattern matching without K, In ACM SIGPLAN Notices, vol.49, pp.257-268, 2014.

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

P. Dybjer, Internal type theory, Types for Proofs and Programs, pp.120-134, 1996.

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

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

C. Mangin and M. Sozeau, An Intuitionistic Theory of Types: Predicative Part, Studies in Logic and the Foundations of Mathematics, vol.80, pp.71945-71946, 2018.

F. Pfenning, Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), p.221, 2001.

A. Stump, From realizability to induction via dependent intersection, Ann. Pure Appl. Logic, vol.169, pp.637-655, 2018.

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

V. Voevodsky, Resising Rules-their use and semantic justification, 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.