nLab real-cohesive (infinity,1)-topos

Redirected from "cohesive model topos".
Note: cohesive (infinity,1)-topos and real-cohesive (infinity,1)-topos both redirect for "cohesive model topos".

Contents

Idea

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

Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)

Last revised on November 15, 2022 at 13:52:54. See the history of this page for a list of all contributions to it.