nLab real-cohesive (infinity,1)-topos



Cohesive \infty-Toposes

Discrete and concrete objects



The categorical semantics of real-cohesive homotopy type theory.


A cohesive (infinity,1)-topos HH is a real cohesive (infinity,1)-topos if HH has a Dedekind real numbers object \mathbb{R} and it satisfies axiom R-flat: for each infinity-groupoid AHA \in H, AA is discrete if and only if the morphism c:Hom(A,A )c \colon Hom(A,A^\mathbb{R}) is an equivalence.

A consequence of axiom R-flat is that the fundamental infinity-groupoid of the Dedekind real numbers is contractible.

See also


Last revised on June 14, 2022 at 13:31:36. See the history of this page for a list of all contributions to it.