Homotopy Type Theory

There are many ways to represent the natural number three:

• the decimal numeral 3,
• $\operatorname{succ}(\operatorname{succ}(\operatorname{succ}(0)))$,
• the Roman numeral III,
• three tally marks
• The hebrew numeral $ג$

These representations are visibly different, yet we expect them to support the same arithmetic. Mathematics should care about their structure, not whether we wrote a number with digits, successors, or tally marks.

Let $\mathsf{Numeral}$ be a type of canonical decimal numerals and let $\mathbb N$ be the inductive natural numbers generated by

$$0:\mathbb N,\qquad \operatorname{succ}:\mathbb N\to\mathbb N.$$

“Canonical” matters. If 3, 03, and 003 are distinct inhabitants, printing after parsing will not return the original string. We must either forbid leading zeroes or identify numerals that denote the same value.

Define a parser and a printer:

$$f:\mathsf{Numeral}\to\mathbb N,\qquad g:\mathbb N\to\mathsf{Numeral}.$$

To show that the representations match, prove that going there and back changes nothing:

$$\alpha:\prod_{n:\mathbb N}f(g(n))=n,\qquad \beta:\prod_{d:\mathsf{Numeral}}g(f(d))=d.$$

This establishes an equivalence $\mathsf{Numeral}\simeq\mathbb N$. But ordinary intensional type theory does not thereby give us an equality $\mathsf{Numeral}=\mathbb N$.
HoTT asks whether equivalence can imply equality, and what follows if they can.

For functions $f,g:A\to B$, a homotopy from $f$ to $g$ is a pointwise equality:

$$f\sim g\;:\equiv\;\prod_{x:A}f(x)=g(x).$$

An equivalence between $A$ and $B$ is a translation that loses no information. Begin with the forward function

$$f:A\to B.$$

We check that it loses no information in two directions.

Every value of $B$ can be recovered

Choose a function

$$g:B\to A$$

and prove

$$\alpha:(f\circ g)\sim\mathsf{id}_B.$$

Pointwise, this says

$$\alpha_b:f(g(b))=b\qquad\text{for every }b:B.$$

Starting with any $b$, translating backward with $g$ and then forward with $f$ returns $b$. Thus the forward map does not leave any value of $B$ unreachable. The function $g$ is called a right inverse of $f$.

Different values of $A$ are not collapsed together

Choose a function

$$h:B\to A$$

and prove

$$\beta:(h\circ f)\sim\mathsf{id}_A.$$

Pointwise, this says

$$\beta_a:h(f(a))=a\qquad\text{for every }a:A.$$

Starting with any $a$, translating forward with $f$ and then backward with $h$ returns $a$. In particular, if $f(a_1)=f(a_2)$, applying $h$ shows that $a_1=a_2$. Thus $f$ does not merge distinct inputs. The function $h$ is called a left inverse of $f$.

Why are there three functions?

The definition names three functions because it records these two guarantees separately:

• $f:A\to B$ is the translation being tested.
• $g:B\to A$ proves that nothing in $B$ is missed.
• $h:B\to A$ proves that nothing in $A$ is collapsed.

The functions $g$ and $h$ are not competing translations. Once both inverse laws hold, one can prove that they agree. For any $b:B$,

$$h(b) =h(f(g(b))) =g(b).$$

The first equality uses $\alpha_b:f(g(b))=b$, and the second uses $\beta_{g(b)}:h(f(g(b)))=g(b)$. Thus the separate left and right inverses together behave like one genuine inverse.

Formally, the two requirements are packaged as

$$\mathsf{isequiv}(f) :\equiv \left(\sum_{g:B\to A}(f\circ g)\sim\mathsf{id}_B\right) \times \left(\sum_{h:B\to A}(h\circ f)\sim\mathsf{id}_A\right).$$

Then an equivalence of types is

$$A\simeq B\;:\equiv\;\sum_{f:A\to B}\mathsf{isequiv}(f).$$

An inhabitant of $A\simeq B$ can therefore be read as a five-part package

$$(f,g,\alpha,h,\beta),$$

containing the forward translation, its right- and left-inverse functions, and the two pointwise inverse proofs.

Why are functions in both directions not enough?

Two unrelated functions $A\to B$ and $B\to A$ need not undo one another. For example, there are constant functions in both directions between many nonempty types. The inverse laws are the part that shows the representations preserve all information.

Suppose $A$ and $B$ are types in a universe $\mathcal U$. A path

$$p:A=_{\mathcal U}B$$

allows us to transport elements and properties from $A$ to $B$. Path induction produces a canonical map

$$\mathsf{idtoeqv}_{A,B}:(A=B)\to(A\simeq B).$$

On reflexivity, this map produces the identity equivalence:

$$\mathsf{idtoeqv}(\mathsf{refl}_A)\equiv\mathsf{idEquiv}_A.$$

Ordinary intensional type theory therefore proves

$$A=B\longrightarrow A\simeq B.$$

The other direction is not available in general. The constructor

$$\mathsf{refl}_A:A=A$$

directly proves only self-equality; it cannot manufacture a path between differently presented types such as $\mathsf{Numeral}$ and $\mathbb N$.

The univalence axiom states that

$$\mathsf{idtoeqv}_{A,B}:(A=B)\to(A\simeq B)$$

is itself an equivalence. Equality of types and equivalence of types carry the same information.

Because $\mathsf{idtoeqv}$ is an equivalence, it has an inverse customarily written

$$\mathsf{ua}_{A,B}:(A\simeq B)\to(A=B).$$

The two maps satisfy inverse laws, including

$$\mathsf{idtoeqv}(\mathsf{ua}(e))=e.$$

Thus an equivalence

$$e:\mathsf{Numeral}\simeq\mathbb N$$

gives a path

$$\mathsf{ua}(e):\mathsf{Numeral}=\mathbb N.$$

This path is useful because any type family $P:\mathcal U\to\mathcal U$ supports transport:

$$\mathsf{transport}^{P}(\mathsf{ua}(e)):P(\mathsf{Numeral})\to P(\mathbb N).$$

Suppose we prove

$$\prod_{n:\mathbb N}n+n=2n.$$

Can we immediately replace $\mathbb N$ by $\mathsf{Numeral}$? There is a subtlety: this statement mentions more than a carrier type. It also uses a distinguished number $2$, addition, and multiplication.

There are two principled ways forward:

1. Transport the entire arithmetic structure—zero, successor, addition, and multiplication—along $\mathsf{ua}(e)$.
2. Define the operations independently and prove that $e$ preserves them.

If the operations on $\mathsf{Numeral}$ are obtained by transport, arithmetic theorems transport with them. If they were defined separately, preservation proofs connect the two implementations.

This idea leads to the structure identity principle: for suitably defined mathematical structures, identity corresponds to structure-preserving equivalence. Isomorphic groups, for example, can be treated as equal as groups—not merely as carrier sets.

We can now state the foundational problem that HoTT addresses. Mathematical objects are normally characterized only up to a suitable notion of equivalence, while foundational equality is often sensitive to how those objects were constructed. Univalence closes that gap.

HoTT interprets a type as a space, an inhabitant as a point, and an equality proof

$$p:a=_A b$$

as a path from $a$ to $b$. The familiar laws of equality become natural path operations:

Equality operation	Path interpretation	Type
Reflexivity	Stay at the same point	$\mathsf{refl}_a:a=a$
Symmetry	Reverse a path	$p^{-1}:b=a$
Transitivity	Concatenate paths	$p\mathbin{\cdot}q:a=c$
Congruence	Map a path through a function	$\mathsf{ap}_f(p):f(a)=f(b)$
Substitution	Move data along a path	$\mathsf{transport}^{P}(p):P(a)\to P(b)$

Identity types may contain several distinguishable paths. Since $a=b$ is itself a type, two paths $p,q:a=b$ may themselves be equal:

$$\alpha:p=q.$$

• Points: $a,b:A$
• Paths: $p,q:a=b$
• Paths between paths: $\alpha,\beta:p=q$
• Higher paths: equalities between those equalities, continuing indefinitely

This higher structure is not decorative. It records coherent ways that transformations agree, exactly the kind of information needed in homotopy theory and higher-dimensional mathematics.

Let $\mathsf{Bool}$ have inhabitants $\mathsf{true}$ and $\mathsf{false}$, and let $\mathsf{Bit}$ have inhabitants $0$ and $1$. There are two equivalences between them.

$$\begin{aligned} e_1(\mathsf{true})&=1,& e_1(\mathsf{false})&=0,\\ e_0(\mathsf{true})&=0,& e_0(\mathsf{false})&=1. \end{aligned}$$

Univalence turns them into two paths:

$$p_1\coloneqq\mathsf{ua}(e_1):\mathsf{Bool}=\mathsf{Bit},$$ $$p_0\coloneqq\mathsf{ua}(e_0):\mathsf{Bool}=\mathsf{Bit}.$$

Show that $p_1$ and $p_0$ are different paths

Suppose $p_1=p_0$. Applying $\mathsf{idtoeqv}$ to both sides gives

$$\mathsf{idtoeqv}(p_1)=\mathsf{idtoeqv}(p_0).$$

By the inverse law for univalence, this reduces to $e_1=e_0$. Applying the forward functions to $\mathsf{true}$ would then give

$$e_1(\mathsf{true})=e_0(\mathsf{true}),$$

and hence $1=0$, which is impossible in $\mathsf{Bit}$. Therefore $p_1\ne p_0$.

We can obtain a loop at one type as well. Boolean negation is an equivalence

$$\mathsf{notEquiv}:\mathsf{Bool}\simeq\mathsf{Bool},$$

so univalence produces

$$\mathsf{ua}(\mathsf{notEquiv}):\mathsf{Bool}=\mathsf{Bool}.$$

This is distinct from $\mathsf{refl}_{\mathsf{Bool}}$, because $\mathsf{idtoeqv}$ sends one to Boolean negation and the other to the identity function. The universe of types therefore has nontrivial loops.

Ordinary inductive types are generated by point constructors. A higher inductive type may also be generated by path constructors and higher-path constructors.

The circle $S^1$ has a point constructor

$$\mathsf{base}:S^1$$

and a path constructor

$$\mathsf{loop}:\mathsf{base}=\mathsf{base}.$$

The type

$$\Omega(S^1)\;:\equiv\;(\mathsf{base}=\mathsf{base})$$

is the loop space of the circle: the type of paths that start and end at $\mathsf{base}$. We will investigate the structure of this type and prove that it is equivalent to the integers:

$$\Omega(S^1)\simeq\mathbb Z.$$

To begin, we can concatenate the generating loop or reverse it:

$$\mathsf{loop}^0\coloneqq\mathsf{refl}_{\mathsf{base}},\qquad \mathsf{loop}^2\coloneqq\mathsf{loop}\cdot\mathsf{loop},\qquad \mathsf{loop}^{-1}\coloneqq(\mathsf{loop})^{-1}.$$

Positive powers travel around $\mathsf{loop}$ repeatedly, negative powers travel around the reversed loop, and the zeroth power stays still. This gives the easy direction of the proposed equivalence between $\mathbb Z$ and the loop space:

$$\mathsf{decode}:\mathbb Z\to(\mathsf{base}=\mathsf{base}),\qquad \mathsf{decode}(n)\coloneqq\mathsf{loop}^n.$$

For example,

$$\mathsf{decode}(0)=\mathsf{refl},\qquad \mathsf{decode}(2)=\mathsf{loop}\cdot\mathsf{loop},\qquad \mathsf{decode}(-1)=\mathsf{loop}^{-1}.$$

But defining $\mathsf{decode}$ does not yet prove that the loop space is equivalent to $\mathbb Z$. We still have to answer two questions:

1. Are $\mathsf{loop}^m$ and $\mathsf{loop}^n$ different whenever $m\ne n$?
2. Is every path $p:\mathsf{base}=\mathsf{base}$ equal to $\mathsf{loop}^n$ for some $n$?

Both questions would be answered by an inverse function

$$\mathsf{encode}:(\mathsf{base}=\mathsf{base})\to\mathbb Z$$

that measures the winding number of an arbitrary loop.

It is tempting to define $\mathsf{encode}$ by pattern matching:

$$\mathsf{encode}(\mathsf{loop}^n)\coloneqq n.$$

But this would assume the result we are trying to prove. Before we have constructed the equivalence, we do not know that every path $\mathsf{base}=\mathsf{base}$ has the form $\mathsf{loop}^n$, nor that the integer $n$ would be unique. An arbitrary equality proof is not presented to us as a list of clockwise and counterclockwise steps that we can simply count. We therefore need a way to measure a path without first assuming that we already know its complete structure.

Step 1: Design a counter that travels along paths

Since we cannot inspect an arbitrary loop directly, we will carry a counter along it and see how the counter changes. To do this, define a type family

$$\mathsf{code}:S^1\to\mathcal U.$$

A type family assigns a type $\mathsf{code}(x)$ to every point $x:S^1$. At the base point, we want the available counter values to be the integers:

$$\mathsf{code}(\mathsf{base})\coloneqq\mathbb Z.$$

Step 2: Move values along paths using transport

For any type family $P:A\to\mathcal U$, any path $p:x=y$, and any value $u:P(x)$, type theory provides

$$\mathsf{transport}^{P}(p,u):P(y).$$

Transport moves a value belonging to the type attached to $x$ into the type attached to $y$. It does not arbitrarily choose a result. Transport is defined by equality elimination, starting with the rule

$$\mathsf{transport}^{P}(\mathsf{refl}_x,u)\;:\equiv\;u.$$

Path induction extends this rule to every equality proof. It also forces transport to respect path composition:

$$\mathsf{transport}^{P}(p\cdot q,u) = \mathsf{transport}^{P} \bigl(q,\mathsf{transport}^{P}(p,u)\bigr).$$

Thus a journey made of two paths moves the value along the first path and then along the second.

There is also a precise connection between the family $P$ and transport. Applying $P$ to a path $p:x=y$ produces a path between the corresponding types:

$$\mathsf{ap}_{P}(p):P(x)=P(y).$$

Any path of types $q:X=Y$ determines a conversion function

$$\mathsf{coe}(q):X\to Y,$$

where $\mathsf{coe}(\mathsf{refl}_X)$ is the identity function. Transport is exactly the conversion determined by the path of types that $P$ assigns to $p$:

$$\mathsf{transport}^{P}(p,u) = \mathsf{coe}\bigl(\mathsf{ap}_{P}(p)\bigr)(u).$$

Equivalently, $\mathsf{coe}(q)$ is the forward function of $\mathsf{idtoeqv}(q)$. Therefore the path $\mathsf{ap}_{P}(p)$ and the behavior of transport along $p$ are not two independent definitions. Once the family’s action on the path is fixed, transport along that path is fixed as well.

Step 3: Decide what one trip around the circle should record

Our goal is an encoder satisfying

$$\mathsf{encode}(\mathsf{loop}^n)=n.$$

We will start the counter at $0$. For one trip around $\mathsf{loop}$ to be recorded as $1$, transporting around $\mathsf{loop}$ should increment the counter:

$$\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},n)=n+1.$$

This is a deliberate design choice forced by the behavior we want from this encoder. Other choices define other measuring systems:

• If one loop acted by $n\mapsto n$, every loop would be measured as $0$.
• If one loop acted by $n\mapsto n+2$, then $\mathsf{loop}$ would be labeled $2$ and $\mathsf{loop}^k$ would be labeled $2k$. That map would never produce odd integers, so it could not be inverse to our $\mathsf{decode}(n)=\mathsf{loop}^n$.
• Using $n\mapsto n-1$ would also work after consistently reversing our orientation: the generating loop would count as $-1$ instead of $1$.

Successor is therefore not an automatic consequence of transport. We choose successor because we want the chosen generating loop to correspond to the integer $1$.

Step 4: Finish defining the family $\mathsf{code}$

We have said what $\mathsf{code}$ does to the point constructor:

$$\mathsf{code}(\mathsf{base})\coloneqq\mathbb Z.$$

Because $S^1$ also has the path constructor $\mathsf{loop}$, the circle recursion rule requires us to say what path of types $\mathsf{code}$ assigns to it. Since both ends of $\mathsf{loop}$ are $\mathsf{base}$, the required type is

$$\mathsf{ap}_{\mathsf{code}}(\mathsf{loop}): \mathsf{code}(\mathsf{base})=\mathsf{code}(\mathsf{base}),$$

or, after substituting our definition at the base point,

$$\mathsf{ap}_{\mathsf{code}}(\mathsf{loop}):\mathbb Z=\mathbb Z.$$

We want transport along this path to perform successor. We already know that successor is an equivalence:

$$\mathsf{succEquiv}:\mathbb Z\simeq\mathbb Z,\qquad \mathsf{succEquiv}(n)=n+1,$$

with predecessor as its inverse. But the circle recursion rule needs an equality of types, not merely an equivalence. Univalence supplies exactly the missing path:

$$\mathsf{ua}(\mathsf{succEquiv}):\mathbb Z=\mathbb Z.$$

We can therefore complete the definition:

$$\begin{aligned} \mathsf{code}(\mathsf{base}) &\coloneqq \mathbb Z,\\ \mathsf{ap}_{\mathsf{code}}(\mathsf{loop}) &\coloneqq \mathsf{ua}(\mathsf{succEquiv}). \end{aligned}$$

Now the formal connection from Step 2 determines transport. Since

$$\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},n) = \mathsf{coe}\bigl( \mathsf{ap}_{\mathsf{code}}(\mathsf{loop}) \bigr)(n),$$

substituting the definition of $\mathsf{code}$ gives

$$\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},n) = \mathsf{coe}\bigl( \mathsf{ua}(\mathsf{succEquiv}) \bigr)(n).$$

The inverse law connecting $\mathsf{ua}$ and $\mathsf{idtoeqv}$ says that converting along $\mathsf{ua}(e)$ performs the original equivalence $e$. Therefore,

$$\mathsf{transport}^{\mathsf{code}}(\mathsf{loop},n)=n+1.$$

Step 5: Define $\mathsf{encode}$

Now the measuring device is ready. Given any path $p:\mathsf{base}=x$, start with

$$0:\mathsf{code}(\mathsf{base})$$

and transport it along $p$:

$$\mathsf{encode}_x(p) \;:\equiv\; \mathsf{transport}^{\mathsf{code}}(p,0) \;:\; \mathsf{code}(x).$$

For a loop, $x$ is again $\mathsf{base}$, so the output belongs to

$$\mathsf{code}(\mathsf{base})=\mathbb Z.$$

Restricting to loops gives the function we wanted:

$$\mathsf{encode}: (\mathsf{base}=\mathsf{base})\to\mathbb Z.$$

Step 6: Watch path composition count repeated loops

Transport along reflexivity leaves the initial counter unchanged:

$$\mathsf{encode}(\mathsf{refl}) = \mathsf{transport}^{\mathsf{code}}(\mathsf{refl},0) = 0.$$

Transporting once around $\mathsf{loop}$ applies successor once:

$$\mathsf{encode}(\mathsf{loop}) = \mathsf{transport}^{\mathsf{code}}(\mathsf{loop},0) = \mathsf{succ}(0) = 1.$$

Since $\mathsf{loop}^2=\mathsf{loop}\cdot\mathsf{loop}$ and transport respects concatenation,

$$\begin{aligned} \mathsf{encode}(\mathsf{loop}^2) &= \mathsf{transport}^{\mathsf{code}} (\mathsf{loop}\cdot\mathsf{loop},0)\\ &= \mathsf{transport}^{\mathsf{code}} \bigl(\mathsf{loop}, \mathsf{transport}^{\mathsf{code}}(\mathsf{loop},0)\bigr)\\ &= \mathsf{succ}(\mathsf{succ}(0))\\ &=2. \end{aligned}$$

Reversing the path applies the inverse equivalence, predecessor, so

$$\mathsf{encode}(\mathsf{loop}^{-1})=-1.$$

Step 7: Show that encode and decode are inverses

The full encode–decode proof establishes

$$\mathsf{encode}(\mathsf{decode}(n))=n$$

and

$$\mathsf{decode}(\mathsf{encode}(p))=p.$$

The first law says that building $\mathsf{loop}^n$ and measuring it returns $n$. The second says that measuring an arbitrary loop and rebuilding the corresponding power of $\mathsf{loop}$ returns the original loop. The second law is what proves that no additional, unaccounted-for loops exist.

Together they give

$$\Omega(S^1)\simeq\mathbb Z.$$

The fundamental group $\pi_1(S^1,\mathsf{base})$ consists of loops based at $\mathsf{base}$, identified when they are connected by a higher path. Its group operation is path concatenation.

Under the encode–decode correspondence, concatenation becomes integer addition:

$$\mathsf{loop}^m\cdot\mathsf{loop}^n \quad\longleftrightarrow\quad m+n.$$

Thus we obtain an isomorphism of groups

$$\pi_1(S^1,\mathsf{base})\cong(\mathbb Z,+).$$

This result is often abbreviated as $\pi_1(S^1)=\mathbb Z$. The symbol $\cong$ is more precise because it emphasizes that both the elements and the group operation correspond.

The striking part is methodological: we defined the circle and computed a topological invariant entirely inside type theory. No external construction of points in the plane was required. This is an example of synthetic homotopy theory.

What is $\mathsf{loop}^2\cdot\mathsf{loop}^{-1}$?

Under the correspondence with integers, the expression represents $2+(-1)=1$. It is therefore equal to $\mathsf{loop}$.

• Abstraction becomes foundational. Clients can reason through an interface or structure without depending on its representation.
• Proofs become reusable. Results transport across equivalent presentations once the relevant structure is included.
• Definitions become invariant. The theory rewards properties that respect equivalence rather than inspecting accidental implementation details.
• Higher mathematics becomes internal. Paths, quotients, spaces, and homotopy invariants can be constructed within type theory.
• Formalization gains a structural foundation. Univalence and higher inductive types support libraries where equivalent constructions do not require parallel theorem hierarchies.

The point of HoTT is therefore not simply that equality can be drawn as a path. Its deeper contribution is a theory of identity that knows when representations are interchangeable while retaining the higher structure of how they are identified.

1. Explain why allowing both 3 and 03 prevents parsing and printing from being strict inverses.
2. Prove that the identity equivalence and Boolean negation are distinct inhabitants of $\mathsf{Bool}\simeq\mathsf{Bool}$.
3. Use univalence to obtain two distinct paths in $\mathsf{Bool}=\mathsf{Bool}$.
4. Explain why an equivalence of carrier types need not preserve independently chosen multiplication operations.
5. Explain why constructing $\mathsf{loop}^n$ for every $n:\mathbb Z$ proves only one direction of $\Omega(S^1)\simeq\mathbb Z$.

Show exercise guidance

1. Printing the parsed value of 03 produces the canonical numeral 3, not the original input.
2. Assume the equivalences are equal and apply their forward functions to $\mathsf{true}$.
3. Apply $\mathsf{ua}$ to the two equivalences, then use $\mathsf{idtoeqv}$ to prove the paths cannot coincide.
4. An arbitrary equivalence can permute the carrier. Preservation of an operation is additional structure.
5. It constructs $\mathsf{decode}$. Surjectivity, injectivity, and the inverse laws require the encode–decode argument.

1. The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Chapters 2 and 4 cover homotopies, equivalences, and univalence; Chapter 6 introduces higher inductive types; Chapter 8 computes the fundamental group of the circle.
2. Daniel R. Licata and Michael Shulman, “A formal proof that $\pi_1(S^1)=\mathbb Z$”. An overview of the formalized circle calculation.
3. Egbert Rijke, Introduction to Homotopy Type Theory. A self-contained modern introduction to univalent mathematics.

---

¹ Polytropos is a Greek word meaning “many-turning” or “of many turns,” famously used as an epithet for Odysseus at the opening of the Odyssey. Here it is a small joke about the paths $\mathsf{loop}^n$: each integer records how many times and in which direction a path turns around the circle. ↩