A pointless circle in HoTT In the beginning of chapter two in The HoTT Book there is a discussion about synthetic vs. analytic geometry:

An important difference between homotopy type theory and classical homotopy theory is that homotopy type theory provides a synthetic description of spaces, in the following sense. Synthetic geometry is geometry in the style of Euclid [EucBC]: one starts from some basic notions (points and lines), constructions (a line connecting any two points), and axioms (all right angles are equal), and deduces consequences logically. This is in contrast with analytic geometry, where notions such as points and lines are represented concretely using cartesian coordinates in $\mathbb{R}^n$ — lines are sets of points — and the basic constructions and axioms are derived from this representation. While classical homotopy theory is analytic (spaces and paths are made of points), homotopy type theory is synthetic: points, paths, and paths between paths are basic, indivisible, primitive notions.

If a circle is a cohesive closed curve independent of points, is the circle necessarily inhabited by points? Or can we have a "pointless circle", i.e. a type $C$ representing a circle without any objects? Is there a circle without any subspaces such as points and paths? If so, is a circle inhabited by a point or a path something else than a plain circle? Or do we automatically have an infinite set of points as inhabitants when we consider a cohesive geometric object in HoTT, as in Euclidean geometry?
 A: Francois' answer is good; let me add a bit more.  Homotopy type theory is synthetic homotopy theory, which means that the "spaces" in question are not the same sort of "spaces" that you find in point-set topology: it's better to think of them as "homotopy types" or "$\infty$-groupoids".  They are not "geometric" in the sense of circles as "closed curves" in a plane; you should think instead of the "circle" as the fundamental $\infty$-groupoid of a topological circle.
(There are refinements of homotopy type theory in which there also exist "cohesive" or "geometric" objects in addition to "homotopy types", but that's an extra layer of confusion that's best ignored when learning the basic subject.)
Another point to emphasize is that in homotopy type theory, a type does not have a "set of points" at all.  The analogy to Euclidean geometry may seem a bit misleading because in the latter one can talk about "the set of points that lie on some line" whether or not that line is identified with its set of points, but in homotopy type theory there is no such thing.  A type does have points, but we don't have a "set of" such points, at least not for the meaning of "set" internal to the theory.  (So actually, the analogy to Euclidean geometry is okay, because internal to Euclidean geometry we don't even have a meaning of "set"; thus "the set of points on a line" must also there be external to the theory.  But it's confusing because in homotopy type theory we do have an internal meaning of "set".)
Finally, there was also a recent discussion on the homotopy type theory mailing list about "circles without points".
A: The (homotopy-theoretic) circle is discussed in Chapter 6 of the book and it does have points. In fact, it is defined as a higher inductive type with an explicit point $\mathsf{base}:S^1$ and one nontrivial identification $\mathsf{loop}:\mathsf{base} =_{S^1} \mathsf{base}$.
This paragraph is about something else. One shouldn't think of a type as "the sum of its points" since types can have a lot of intrinsic structure. In set theory, the circle is a collection of points with extrinsic topological structure — one cannot distinguish the circle from any other set of size continuum without the additional topological data. In homotopy type theory, the topological structure of the circle type $S^1$ above is intrinsic. Any type equivalent to $S^1$ has the same structure, in fact it is $S^1$ by univalence.
Interestingly, the equivalence $$A \simeq {\textstyle\sum_{x:A} 1},$$ which literally says that $A$ is equivalent to the sum of its points, is true in homotopy type theory. While this may be confounding at first, it actually illustrates the strength of the intrinsic structure of types: the intrinsic structure is automatically reconstructed when reassembling individual parts of a type into a whole. That said, one can forget the intrinsic structure of a type by means of set truncation ($0$-truncation) but the resulting type, which is now just a plain set of points with no additional structure, is no longer equivalent to the original type.
