Double negation stable h-propositions in cubical sets

TL;DR

This paper constructs classifiers for double negation stable h-propositions in cubical set models, demonstrating their existence aligns with the metatheory and enabling models with extended Church's thesis.

Contribution

It introduces a method to build classifiers for double negation stable propositions in cubical sets, linking their existence to the metatheory and enabling new models of homotopy type theory.

Findings

Classifiers for double negation stable propositions exist in cubical sets if they do in the metatheory.

The Dedekind real numbers can be added without affecting consistency.

A model with extended Church's thesis, where all partial functions with stable domains are computable, is constructed.

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.