Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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 that look like continua.
One simple way to axiomatize this would be to say:
is a ring object;
it is geometrically contractible, .
The last condition reflects the “continuumness”. For instance in the standard model Smooth∞Grpd for smooth homotopy cohesion, this distibuishes from .
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.
I just saw this page. A remark that you might like is that if is a path-connected internal ring in (say) , then it is automatically contractible. Actually, all we really need is that there is a path that connects the additive identity to the multiplicative identity , since then
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.
Thanks, good point. I have added a remark on this.
I have tried to state it in generality: if there is a subobject which is itself geometrically contractible and contains the elements 0 and 1, then this implies already that the ring object is geometrically conctractible.
(This needs of the axioms of cohesion the statement that preserves products! )
Of course, doesn’t have to be a subobject. All we need is an interval (a cospan such that is geometrically contractible) together with a cospan map from the interval cospan to the cospan .
If you don’t object, I’ll add this in.
Sure, very good.
Okay, I added something in. Not knowing the best terminology, I referred to a map from an interval type to the bipointed type . 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.
Thanks. I had entirely forgotten that we have interval type.
Wait, we have to be careful here. The unit interval is not (the interpretation of) an interval type. Instead is:
the difference is that an interval type is required to have its endpoints be equivalent by morphism. But in there are no non-trivial morphisms at all.
I’ll edit at continuum a bit more to reflect this.
This is nice!
Added this pointer:
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).
1 to 12 of 12