Double negation stable h-propositions in cubical sets
arXiv:2209.15035
The paper constructs classifiers for double‑negation‑stable h‑propositions in various cubical set models of homotopy type theory, and uses them to obtain relative consistency results such as adding Dedekind reals without increasing consistency strength and modeling extended Church’s thesis.
Abstract
We give a construction of classifiers for double negation stable h-propositions in a variety of cubical set models of homotopy type theory and cubical type theory. This is used to give some relative consistency results: classifiers for double negation stable propositions exist in cubical sets whenever they exist in the metatheory; the Dedekind real numbers can be added to homotopy type theory without changing the consistency strength; we construct a model of homotopy type theory with extended Church's thesis, which states that all partial functions with double negation stable domain are computable.