J. Avigad, K. Kapulkin, and P. L. Lumsdaine, Homotopy limits in type theory, Mathematical Structures in Computer Science, vol.13, issue.05, 2015.
DOI : 10.1007/978-3-642-02273-9_14

B. Ahrens, K. Kapulkin, and M. Shulman, Univalent Categories and the Rezk completion, Mathematical Structures in Computer Science, 2015.

S. Berardi, M. Bezem, and T. Coquand, Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998.
DOI : 10.1007/BF02007566

A. Bauer, J. Gross, P. Lefanu-lumsdaine, M. Shulman, M. Sozeau et al., 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

P. Cohen, Set theory and the continuum hypothesis, 1966.

K. Gödel, 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

K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory, 1940.

H. Herbelin, 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

G. Jaber, P. Lewertowski, M. Pédrot, N. Sozeau, and . Tabareau, 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

G. Jaber, N. Tabareau, and M. Sozeau, 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.

J. Krivine, 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

P. Lefanu, L. , and M. Shulman, Higher inductive types. preparation, 2013.

J. Lurie, Higher topos theory Annals of mathematics studies, 2009.

S. Maclane and I. Moerdijk, 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.

M. Parigot, Classical proofs as programs. In Computational logic and proof theory, pp.263-276, 1993.
DOI : 10.1007/bfb0022575

E. Rijke, B. Spittersshu, and M. Shulman, 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

M. Shulman and M. Shulman, 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.

M. Tierney, Sheaf theory and the continuum hypothesis, 1972.
DOI : 10.1007/BFb0073963

M. Tierney, Sheaf theory and the continuum hypothesis, LNM, vol.274, pp.13-42, 1972.
DOI : 10.1007/BFb0073963