Double negation stable h-propositions in cubical sets
Logic
2022-10-03 v1 Logic in Computer Science
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.
Cite
@article{arxiv.2209.15035,
title = {Double negation stable h-propositions in cubical sets},
author = {Andrew W. Swan},
journal= {arXiv preprint arXiv:2209.15035},
year = {2022}
}