In homotopy type theory, propositional excluded middle and the axiom of choice sets are both consistent with univalence, both of which yields type theoretic models for classical mathematics. However, there are other axioms, such as the axiom of global choice and uniqueness of identity proofs, that are known to be inconsistent with univalence. Is the generalised continuum hypothesis consistent with univalence?
$\begingroup$ $\endgroup$
1 - 9$\begingroup$ The construction of the simplicial sets model does not depend on CH or its negation, so I imagine if you do that construction starting from a model of GCH then you will get a model of HoTT in which GCH holds. $\endgroup$Zhen Lin– Zhen Lin2022-03-02 11:47:36 +00:00Commented Mar 2, 2022 at 11:47
Add a comment |
1 Answer
$\begingroup$ $\endgroup$
1 Dominik Kirst and Felix Rech managed to formalize the Generalized Continuum Hypothesis for sets in the HoTT library in Coq with univalence, which already shows the consistency of the GCH with univalence, and proved that it implies the Axiom of Choice for sets:
- 5$\begingroup$ Just formulating GCH in HoTT doesn't imply it's consistency. But as Zhen Lin commented, we have the simplicial sets model and that gives an equivalence of the category of sets in the model with the ambient category of sets, so if GCH holds in the ambient set theory, it holds in the simplicial sets model of HoTT. $\endgroup$Ulrik Buchholtz– Ulrik Buchholtz2022-06-05 08:55:16 +00:00Commented Jun 5, 2022 at 8:55