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?