T. Altenkirch, Extensional equality in intensional type theory, 14th Symposium on Logic in Computer Science, pp.412-420, 1999.

T. Altenkirch and A. Kaposi, Type theory in type theory using quotient inductive types, Proceedings of POPL 2016, pp.18-29, 2016.

,

T. Altenkirch and A. Kaposi, Towards a Cubical Type Theory without an Interval, TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs), vol.69, pp.1-3, 2018.

T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now! In: PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification, pp.57-58, 2007.

A. Anand, S. Boulier, C. Cohen, M. Sozeau, and N. Tabareau, Towards certified meta-programming with typed template-coq, ITP 2018-9th Conference on Interactive Theorem Proving, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01809681

R. Atkey, N. Ghani, and P. Johann, A relationally parametric model of dependent type theory, Proceedings of POPL '14, pp.503-516, 2014.

J. P. Bernardy, P. Jansson, and R. Paterson, Proofs for free -parametricity for dependent types, Journal of Functional Programming, vol.22, issue.02, pp.107-152, 2012.

M. Bezem, T. Coquand, and S. Huber, A model of type theory in cubical sets, 19th International Conference on Types for Proofs and Programs (TYPES 2013), vol.26, pp.107-128, 2014.

S. Boulier, Extending Type Theory with Syntactic Models, 2018.
URL : https://hal.archives-ouvertes.fr/tel-02007839

S. Boulier, P. M. 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, pp.182-194, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01445835

,

J. Cartmell, Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic, vol.32, pp.209-243, 1986.

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom, TYPES 2015. Leibniz International Proceedings in Informatics (LIPIcs), vol.69, pp.1-5, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01378906

P. Dybjer, Internal type theory, Lecture Notes in Computer Science. pp, pp.120-134, 1996.

G. Gilbert, J. Cockx, M. Sozeau, and N. Tabareau, Definitional Proof-Irrelevance without K, Proceedings of POPL 2019, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01859964

H. Herbelin, Syntactic investigations into cubical type theory, TYPES 2018. University of Minho, 2018.

M. Hofmann, Conservativity of equality reflection over intensional type theory, TYPES 95, pp.153-164, 1995.

M. Hofmann, Extensional concepts in intensional type theory. Thesis, 1995.

M. Hofmann, Syntax and semantics of dependent types, Semantics and Logics of Computation, pp.79-130, 1997.

M. Hofmann and T. Streicher, The groupoid interpretation of type theory. In: In Venice Festschrift, pp.83-111, 1996.

G. Jaber, G. Lewertowski, P. Pédrot, M. Sozeau, and N. Tabareau, The definitional side of the forcing, Proceedings of LICS '16, pp.367-376, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01319066

A. Kaposi, The setoid model formalized in Agda, 2019.

A. Kaposi, A. Kovács, and T. Altenkirch, Constructing quotient inductiveinductive types, Proc. ACM Program. Lang. 3(POPL), vol.2, 2019.

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

M. Sozeau and N. T. , , 2013.

C. Mcbride, Elimination with a motive, Selected Papers from the International Workshop on Types for Proofs and Programs, pp.197-216, 2002.

N. Oury, Extensionality in the calculus of constructions, pp.278-293, 2005.

T. U. Program, Homotopy type theory: Univalent foundations of mathematics, Tech. rep., Institute for Advanced Study, 2013.

J. Sterling, C. Angiuli, and D. Gratzer, Cubical syntax for reflection-free extensional equality, Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), vol.131, 2019.

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

N. Tabareau, É. Tanter, and M. Sozeau, Equivalences for Free, ICFP 2018 -International Conference on Functional Programming, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01559073

P. Van-der-walt and W. Swierstra, Engineering proof by reflection in agda, Symposium on Implementation and Application of Functional Languages, pp.157-173, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00987610

T. Winterhalter, M. Sozeau, and N. Tabareau, Using reflection to eliminate reflection, 24th International Conference on Types for Proofs and Programs, TYPES 2018. University of Minho, 2018.