T. Altenkirch, P. Capriotti, G. Dijkstra, N. Kraus, and F. N. Forsberg, Quotient inductive-inductive types, FoSSaCS, vol.10803, pp.293-310, 2018.

T. Altenkirch, P. Capriotti, and N. Kraus, Extending homotopy type theory with strict equality, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.62, pp.1-21, 2016.

C. Angiuli, G. Brunerie, T. Coquand, K. Hou, R. Harper et al., Cartesian cubical type theory, 2019.

C. Angiuli, K. F. Hou, and R. Harper, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Computer Science Logic, 2018.

M. Bezem, T. Coquand, and S. Huber, A model of type theory in cubical sets, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.26, pp.107-128, 2013.

M. Bezem, T. Coquand, and S. Huber, The univalence axiom in cubical sets, The Journal of Automated Reasoning, vol.63, issue.2, pp.159-171, 2019.

M. Bezem, T. Coquand, and E. Parmann, Non-constructivity in Kan simplicial sets, 13th International Conference on Typed Lambda Calculi and Applications, vol.38, pp.92-106, 2015.

P. Capriotti, Models of Type Theory with Strict Equality, 2017.

E. Cavallo and R. Harper, Higher inductive types in cubical computational type theory, PACMPL 3 (POPL) 1:1-1:27, 2019.

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical type theory: A constructive interpretation of the univalence axiom, FLAP, vol.4, issue.10, pp.3127-3170, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01378906

T. Coquand, S. Huber, and A. Mörtberg, On higher inductive types in cubical type theory, LICS, ACM, pp.255-264, 2018.

N. Gambino and R. Garner, The identity type weak factorisation system, Theoretical Computer Science, vol.409, issue.1, pp.94-109, 2008.

N. Gambino and C. Sattler, Uniform fibrations and the frobenius condition, 2015.

P. S. Hirschhorn, Model Categories and Their Localizations, Mathematical Surveys and Monographs, vol.99, 2003.

M. Hofmann, Syntax and semantics of dependent types, Extensional Constructs in Intensional Type Theory, pp.13-54, 1997.

, Homotopy Type Theory wiki, 2014.

M. Hovey, Model Categories, vol.63, 2007.

C. Kapulkin and P. L. Lumsdaine, The simplicial model of univalent foundations (after voevodsky), 2012.

D. R. Licata, I. Orton, A. M. Pitts, and B. Spitters, Internal universes in models of homotopy type theory, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.108, pp.1-22, 2018.

P. L. Lumsdaine, Model structures from higher inductive types, 2011.

A. Nuyts, Robust notions of contextual fibrancy, Presentation at HoTT/UF'18 Workshop, 2018.

,

, at 09:52:14, subject to the Cambridge Core terms of use, Logical Methods in Computer Science, vol.14, issue.4, 2018.

I. Orton and A. M. Pitts, Code supporting Axioms for Modelling Cubical Type Theory in a Topos, 2018.

C. Sattler, The Equivalence Extension Property and Model Structures, 2017.

A. W. Swan, An algebraic weak factorisation system on 01-substitution sets: A constructive proof, Journal of Logic & Analysis, vol.8, 2016.

, A simple type system with two identity types, The Coq Development Team, 2013.

. Remark, Let us remark that our formalization does not use connected (ax 1 ), cof_? (ax 8 ), and strictness (ax 9 ) axioms

S. Boulier and N. Tabareau, Model structure on the universe of all types in interval type theory, Mathematical Structures in Computer Science, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02966633