Homotopy limits in type theory, Mathematical Structures in Computer Science, vol.13, issue.05, 2015. ,
DOI : 10.1007/978-3-642-02273-9_14
Univalent Categories and the Rezk completion, Mathematical Structures in Computer Science, 2015. ,
Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998. ,
DOI : 10.1007/BF02007566
The HoTT library: a formalization of homotopy type theory in Coq, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , CPP 2017, pp.131-142, 2002. ,
DOI : 10.1145/3018610.3018615
URL : https://hal.archives-ouvertes.fr/hal-01421212
Set theory and the continuum hypothesis, 1966. ,
The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis, Proceedings of the National Academy of Sciences, pp.556-557, 1938. ,
DOI : 10.1073/pnas.24.12.556
The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory, 1940. ,
A Constructive Proof of Dependent Choice, Compatible with Classical Logic, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.365-374, 2012. ,
DOI : 10.1109/LICS.2012.47
URL : https://hal.archives-ouvertes.fr/hal-00697240
The Definitional Side of the Forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, 2016. ,
DOI : 10.1145/2933575.2935320
URL : https://hal.archives-ouvertes.fr/hal-01319066
Extending type theory with forcing The simplicial model of univalent foundations. arXiv preprint, Logic in Computer Science (LICS), 27th Annual IEEE Symposium on, pp.395-404, 2012. ,
Dependent choice, ???quote??? and the clock, Theoretical Computer Science, vol.308, issue.1-3, pp.259-276, 2003. ,
DOI : 10.1016/S0304-3975(02)00776-4
URL : https://hal.archives-ouvertes.fr/hal-00154478
Higher inductive types. preparation, 2013. ,
Higher topos theory Annals of mathematics studies, 2009. ,
Sheaves in Geometry and Logic [MV99] Fabien Morel and Vladimir Voevodsky. A 1 -homotopy theory of schemes, Publications Mathématiques de l'IHÉS, pp.45-143, 1992. ,
Classical proofs as programs. In Computational logic and proof theory, pp.263-276, 1993. ,
DOI : 10.1007/bfb0022575
Sets in homotopy type theory, Mathematical Structures in Computer Science, vol.27, issue.05, pp.1172-1202, 2015. ,
DOI : 10.1093/logcom/14.4.447
Univalence for inverse diagrams and homotopy canonicity . arXiv preprint arXiv:1203.3253 Quantum gauge field theory in cohesive homotopy type theory, Proceedings 9th Workshop on Quantum Physics and Logic of Electronic Proceedings in Theoretical Computer ScienceST14] Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq. In Interactive Theorem Proving, pp.10-12, 2012. ,
Sheaf theory and the continuum hypothesis, 1972. ,
DOI : 10.1007/BFb0073963
Sheaf theory and the continuum hypothesis, LNM, vol.274, pp.13-42, 1972. ,
DOI : 10.1007/BFb0073963