CW-complex, Hausdorff space, second-countable space, sober space
connected space, locally connected space, contractible space, locally contractible space
The circle is a fantastic thing with lots and lots of properties and extra structures. It is a:
and it is one of the basic building blocks for lots of areas of mathematics, including:
We consider the circle first as a topological space, then as the homotopy type represented by that space.
The two most common definitions of the circle are:
It is the subspace of $\mathbb{C}$ consisting of those numbers of length $1$:
(of course, $\mathbb{C}$ can be identified with $\mathbb{R}^2$ and an equivalent formulation of this definition given; also, to emphasise the reason for the notation $U(1)$, $\mathbb{C}$ can be replaced by $\mathbb{C}^* = GL_1(\mathbb{C})$)
It is the quotient of $\mathbb{R}$ by the integers:
The standard equivalence of the two definitions is given by the map $\mathbb{R} \to \mathbb{C}$, $t \mapsto e^{2 \pi i t}$.
As a homotopy type the circle is for instance the homotopy pushout
In homotopy type theory, this can be formalized as a higher inductive type generated by a point base
and a path from base
to itself; see the references.
The topological circle is a compact, connected topological space. It is a $1$-dimensional smooth manifold (indeed, it is the only $1$-dimensional compact, connected smooth manifold). It is not simply connected. Its first homotopy group is the integers
(A proof of this in homotopy type theory is in Shulman P1S1.)
But the higher homotopy groups $\pi_n(S^1) \simeq *$, $n \gt 1$ all vanish (and so is a homotopy 1-type). The circle is a model for the classifying space for the abelian group $\mathbb{Z}$, the integers.
The product of the circle with itself is the torus
Generally, the $n$-torus is $(S^1)^n$.
A formalization in homotopy type theory, along with a proof that $\pi_1(S^1) \simeq \mathbb{Z}$, can be found in
The proof is formalized therein using the Agda proof assistant. See also
The HoTT Book, section 8.1
The HoTT Coq library: theories/hit/Circle.v
The HoTT Agda library: homotopy/LoopSpaceCircle.agda