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.
The circle is a model for the classifying space for the abelian group $\mathbb{Z}$, the integers. Equivalently, the circle is the Eilenberg-Mac Lane space $K({\mathbb{Z}},1)$. Explicitly, the first homotopy group $\pi_1(S^1)$ is the integers $\mathbb{Z}$. But the higher homotopy groups $\pi_n(S^1) \simeq *$, $n \gt 1$ all vanish (and so is a homotopy 1-type). This can be deduced from the result that the loop space $\Omega S^1$ of the circle is the group ${\mathbb{Z}}$ of integers and that $S^1$ is path-connected. A proof of this in homotopy type theory is in Shulman P1S1.
The result that $S^1\simeq K({\mathbb{Z}},1)$ holds in a general Grothendieck (∞,1)-topos. In fact, more generally, for $X$ a pointed object of a Grothendieck (∞,1)-topos ${\mathcal{H}}$, there is a natural equivalence between the suspension object $\Sigma X$ and the classifying space $B{\mathbb{Z}}\wedge X$. In particular, when $X$ is specifically the 0-truncated two-point space $S^0$, we get $S^1\simeq K({\mathbb{Z}},1)$.
The product of the circle with itself is the ($2$)-torus
Generally, the $n$-torus $T^n$ is $(S^1)^n$.
A formalization in homotopy type theory, along with a proof that $\Omega S^1\simeq {\mathbb{Z}}$ (and hence $\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