A continuum is in general something opposite to a discrete. There are several notions of continuum in mathematics:
Often the continuum is taken to refer to the real line; consequently the cardinality of the continuum referse to the cardinality of the set of real numbers. There is a related continuum hypothesis in set theory.
In physics one may also mean by a continuum a medium which spreads the physical quantities spatially with some finite density, unlike the physics of a system of particles, where an infinite (delta-distribution-like) density is attached to a discrete system of points. See at geometry of physics for more on the relation of the continuum in form of the real line to physics.
One can axiomatize aspects of the notion of line continuum in cohesive homotopy type theory. There the idea of an object all whose points are, while different, connectable by continuous paths (and uniquely so, up to suitable homotopy) is encoded in asking that after applying the fundamental ∞-groupoid functor to it, the result is something contractible
In the model of cohesive homotopy type theory called Smooth∞Grpd we have a full and faithful embedding of smooth manifolds. Therefore we can embed the integers , the rational numbers as well as the real numbers , all equipped with their canonical smooth manifold structure. This is discrete for the first two, but not for the last one, and homotopy cohesion can detect this:
This reflects the fact that the points of form a continuum, but those of and do not.
Also the complex numbers with their canonical manifold structure of course form a continuum in this sense
This is not true in smooth cohesion for replaced by and in this sense is “the real continuum” here (in both sense of the word “real”).
Hence in words: “If in the ring the elements 0 and 1 are path-connected, then is already contractible, hence is a line continuum.”
Under the given assumptions we obtain a commuting diagram of the form
Since preserves products, it sends this to a diagram of the form
which exhibits a contracting homotopy of .
The of prop. 1 is in general not an interval type, but only its image is. See the discussion Geometric spaces and their cohesive homotopy types at cohesive homotopy type theory for more on this.