Quotient inductive-inductive types, FoSSaCS, vol.10803, pp.293-310, 2018. ,
Extending homotopy type theory with strict equality, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.62, pp.1-21, 2016. ,
Cartesian cubical type theory, 2019. ,
Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Computer Science Logic, 2018. ,
A model of type theory in cubical sets, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.26, pp.107-128, 2013. ,
The univalence axiom in cubical sets, The Journal of Automated Reasoning, vol.63, issue.2, pp.159-171, 2019. ,
Non-constructivity in Kan simplicial sets, 13th International Conference on Typed Lambda Calculi and Applications, vol.38, pp.92-106, 2015. ,
Models of Type Theory with Strict Equality, 2017. ,
Higher inductive types in cubical computational type theory, PACMPL 3 (POPL) 1:1-1:27, 2019. ,
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
On higher inductive types in cubical type theory, LICS, ACM, pp.255-264, 2018. ,
The identity type weak factorisation system, Theoretical Computer Science, vol.409, issue.1, pp.94-109, 2008. ,
, Uniform fibrations and the frobenius condition, 2015.
Model Categories and Their Localizations, Mathematical Surveys and Monographs, vol.99, 2003. ,
Syntax and semantics of dependent types, Extensional Constructs in Intensional Type Theory, pp.13-54, 1997. ,
, Homotopy Type Theory wiki, 2014.
Model Categories, vol.63, 2007. ,
The simplicial model of univalent foundations (after voevodsky), 2012. ,
Internal universes in models of homotopy type theory, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.108, pp.1-22, 2018. ,
Model structures from higher inductive types, 2011. ,
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.
Code supporting Axioms for Modelling Cubical Type Theory in a Topos, 2018. ,
, The Equivalence Extension Property and Model Structures, 2017.
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.
Let us remark that our formalization does not use connected (ax 1 ), cof_? (ax 8 ), and strictness (ax 9 ) axioms ,
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