One point and one loop make a circle: higher inductive types build spaces from generators
Euclid began with points and lines as primitives — things you do not construct but simply declare, along with the rules for what you may do with them. Homotopy type theory does the same, except its primitives are points, paths, and paths between paths. And the moment you are allowed to declare a path, you are allowed to declare a space.
Ordinary inductive types are generated by point constructors. The natural numbers come from zero and successor; every natural number is something those two can build. Higher inductive types add one ingredient: constructors whose output is a path. The flagship example is the circle. One point, called base. One path from base to itself, called loop. That is the whole definition — and it really is the circle, in the sense that everything topology says about circles can be proved from those two lines.
The word freely is doing heavy lifting. Listing one loop hands you far more than one loop, because the ambient path operations immediately produce loop followed by loop, loop reversed, loop three times — and these are provably different from one another. One generator, and out falls a copy of the integers, exactly as the free group on a single element does.
A sandbox with three tools: place a point, drag a path between points (self-loops allowed), and fill a pair of parallel paths with a 2-cell. The panel alongside lists what your generators have freely produced — with one point and one self-loop you get every winding number for free. Presets snap to the booleans, the circle, and the torus.
You wrote down one loop, but composition and inversion come with the ambient path structure, so every winding number exists for free — and they are all distinct. The loops form the free group on one generator, a copy of the integers. One point plus one loop: this type is the circle.
The picture is a diagram, not a metric space: a “loop” drawn 34 pixels wide is the same constructor however it is drawn. All that exists is what the generators, and the path operations acting on them, force to exist.
An inductive definition is a promise in two directions. It says what you may put into the type — the constructors — and, through its induction principle, it says that nothing else is in there. For the circle, the induction principle reads: to define a function out of the circle, supply a point in the target and a loop at that point. Nothing more is needed, and nothing less will do. That is the entire universal property, and it is worth stating in the sharper form: the type of functions out of the circle is equivalent to the type of pairs consisting of a point and a loop at it.
There is a companion example that looks trivial and is not. The interval — two points and a path between them — is contractible, homotopically the most boring space there is. Yet its existence proves function extensionality, because a homotopy between two functions is exactly a map out of the interval into the function space. A space with no shape at all can still carry real deductive power.
Suspension is the machine that turns points into paths. Add a north pole and a south pole, then run one meridian from north to south for every point of the space you started with. Step the pipeline and watch the empty type become two points, two points become a circle, and a circle’s worth of meridians sweep out a sphere. Scrub the slider to extrude the meridians by hand.
On the equator plane: nothing at all — the current type is empty. Press Suspend anyway.
Writing the higher spheres out by hand gets ugly fast. The 2-sphere is a point plus a 2-dimensional path from the constant loop to itself; the 3-sphere needs a 3-path; and the bookkeeping for dependent paths at each new level grows faster than anyone wants to manage. Suspension replaces all of it with a single recursive clause. Each sphere is the suspension of the one below, so the whole infinite family follows from the empty type and one operation applied over and over.
The pattern generalizes. Suspension is a special case of a pushout — gluing two types along a third — and pushouts cover an enormous range of standard constructions at once: cones, joins, wedges, smash products, mapping cylinders. Declare the span, and the glued space exists.
The picture from every topology course, made literal. Take a square, choose how to identify its edges, and fold. The torus glues both pairs with matching orientation; flip one pair and you get the Klein bottle; identify opposite boundary points and you get the projective plane. Watch the four corners converge to a single point as the fold completes.
Both pairs of edges glue with matching orientation. All four corners become one point, the two edge pairs become the loops p and q, and the square’s interior is the 2-cell witnessing that they commute.
The torus is the cleanest illustration of what a higher inductive definition is. Its generators are one point, two loops, and a single 2-cell asserting that the two loops commute — and that 2-cell is precisely the interior of the folded square. The classical construction and the type-theoretic definition are not analogous. They are the same object, written twice.
Two surprises are worth flagging. First, gluing creates structure that was not there before: take two points, glue them to two other points along two separate paths, and the result is a circle. Colimits manufacture loops, which means sets are not closed under gluing — the reason truncation exists as an operation. Second, and stranger: the dimension of your generators does not bound the homotopy you get. The 2-sphere is built from a point and one 2-dimensional cell, and yet it contains genuinely nontrivial 3-dimensional structure. Nothing in the definition hints at it.
See also: The Sphere Table in this module, where that surprise is pinned down as the Hopf fibration, and the dedicated Hopf Fibration module for the geometry on its own terms.