He didn’t mention the higher inductive-inductive Cauchy reals! (-: Although I suppose he also didn’t mention the problem with the Cauchy reals that they solve (lack of Cauchy-completeness), while they don’t solve the problem with the Cauchy reals that he did mention (undesirable behavior in models).

]]>Added this pointer:

- Peter Johnstone,
*Topos-theoretic models of the continuum*(slides, lecture video)

This is nice!

]]>Wait, we have to be careful here. The unit interval $[0,1] \in TopMfd \hookrightarrow ETop\inftyGrpd$ is not (the interpretation of) an interval type. Instead $\Pi([0,1]) \in \infty Grpd$ is:

the difference is that an interval type is required to have its endpoints be equivalent by morphism. But in $[0,1]$ there are no non-trivial morphisms at all.

I’ll edit at continuum a bit more to reflect this.

]]>Thanks. I had entirely forgotten that we have *interval type*.

Okay, I added something in. Not knowing the best terminology, I referred to a map from an interval type $(left, right, I)$ to the bipointed type $(0, 1, \mathbb{A}^1)$. By the way, I changed in this section “continuum” to “line continuum”, to avoid conflict with the way that “continuum” was being used in the previous section. Hope that’s okay with you.

]]>Sure, very good.

]]>Of course, $i: I \to \mathbb{A}$ doesn’t have to be a *subobject*. All we need is an interval (a cospan $\ast \to I \leftarrow \ast$ such that $I$ is geometrically contractible) together with a cospan map from the interval cospan to the cospan $\ast \stackrel{0}{\to} \mathbb{A} \stackrel{1}{\leftarrow} \ast$.

If you don’t object, I’ll add this in.

]]>Thanks, good point. I have added a remark on this.

I have tried to state it in generality: if there is a subobject $I \hookrightarrow \mathbb{A}^1$ which is itself geometrically contractible and contains the elements 0 and 1, then this implies already that the ring object $\mathbb{A}^1$ is geometrically conctractible.

(This needs of the axioms of cohesion the statement that $\Pi$ preserves products! )

]]>I just saw this page. A remark that you might like is that if $\mathbb{A}$ is a path-connected internal ring in (say) $Top$, then it is automatically contractible. Actually, all we really need is that there is a path $\alpha: I \to \mathbb{A}$ that connects the additive identity $0$ to the multiplicative identity $1$, since then

$I \times \mathbb{A} \stackrel{\alpha \times 1}{\to} \mathbb{A} \times \mathbb{A} \stackrel{mult}{\to} \mathbb{A}$defines a contracting homotopy.

The reason I’m bringing this up is that the first section of continuum mentions connectedness but not at all contractibility. The two are brought together when we have a ring object.

]]>I have added to continuum a paragraph titled In cohesive homotopy type theory.

This is a simple observation and idea that I have been carrying around for a while. Several people are currently thinking about ways to axiomatize the reals in (homotopy) type theory.

With *cohesive* homotopy type theory there is what looks like an interesting option for an approach different to the other ones: one can ask more generally about line objects $\mathbb{A}^1$ that look like continua.

One simple way to axiomatize this would be to say:

$\mathbb{A}$ is a ring object;

it is geometrically contractible, $\mathbf{\Pi} \mathbb{A} \simeq *$.

The last condition reflects the “continuumness”. For instance in the standard model Smooth∞Grpd for smooth homotopy cohesion, this distibuishes $\mathbb{A} = \mathbb{Z}, \mathbb{Q}$ from $\mathbb{A} = \mathbb{R}, \mathbb{C}$.

So while this axiomatization clearly captures one aspect of “continuum” very elegantly, I don’t know yet how far one can carry this in order to actually derive statements that one would want to make, say, about the real numbers.

]]>