Here, we discuss concepts from Ch.2 of the HoTT book

The central idea is that types can be interpreted as higher-dimensional groupoids in category theory, or spaces in homotopy theory. Space $X$ is a set of points equipped with a topology, and a path betwen points $x$ and $y$ is represented by a continuous map $p : [0, 1] \rightarrow X$ where $p(0) = x, p(1) = y$. The function can be thought of as giving a point $x$ at each moment in time. A homotopy between a pair of continuous maps $H : X_1 \times [0, 1] \rightarrow X_2$, so that $H(s, 0) = p(s)$ and $H(s, 1) = q(s)$, can be thought of as a continuous deformation from $p$ to $q$.

The fundamental group of a fundamental $\infty$-groupoid of a space will agree with the classical definition of a fundamental group of the space: this correspondence illustrates how homotopy theory and higher-dimensional category theory are intimately related.

We will refer to $x =_A y$ as a path between the start point $x$ and endpoint $y$. $r : p =_{x =_A y} q$ can be thought of as a homotopy or a 2-path or 2-dimensional path. All of the basic constructions and axoims arises automatically from the induction principle for identity types. In other words, given the dependent funtions:

- $D : \Pi_{x, y : A} (x = y) \rightarrow \mathscr{U}$
- $d : \Pi_{a : A} D(a, a, \texttt{refl}_a)$

there is a dependent function:

such that

Informally, the induction principle for identity types says that if we want to construct an object which depends on an inhabitant $p : x =_A y$ of an identity type, then it suffices to perform the construction in the special case when $x, y$ are judgementally the same, and $p$ is the reflexivity element $\texttt{refl}_x x = x$.

The induction principle endows each type with the structure of an $\infty$-groupoid, and each function between two types with the structure of the an $\infty$-functor betwen two such groupoids.

## Types are higher groupoids

To state our first lemma:

The proof of this lemma would involve constructing an inhabitant of this type. Let us write the proof in an informal style, as this is preferred. We want to construct $x, y :A$, $p : x = y$, and $p^{-1} : y = x$. By induction, it suffices to consider the case when $y = x$ and $p = \texttt{refl}_x$. In this case, the type of $x = y$ and $y = x$, in which we're trying to construct $p^{-1}$, are both equal to $x = x$. Thus, in the reflexivity case, we can define $\texttt{refl}_x^{-1}$ to simply be $\texttt{refl}_x$. The general case therefore proceeds by the induction principle, and the conversion rule $\texttt{refl}_x^{-1} \equiv \texttt{refl}_x$.

To state our second lemma:

The proof proceeds as follows: $\forall x, y, z : A$, every $p : x = y$ and every $q : y = z$, we need to construct an inhabitant of $x = z$. By induction on $p$, it sufficces to assume that $y = x$ and $p$ is $\texttt{refl}_x$. In this case, the type of $y = z$ of $q$ is $x = z$. By induction on $q$, it suffices to assume that $z = x$ and $q$ is $\texttt{refl}_x$. In this case, $x = z$ is $x = x$, and we have $\texttt{refl}_x : (x = x)$.

This proof raises the question of why an induction on $q$ is required at all, when we already have the equality $x = z$. Indeed, we could have done an induction on $p$ yielding the computation rule $p \circ \texttt{refl}_x \equiv p$, an induction on $q$ yielding the computation rule $\texttt{refl}_y \circ q \equiv q$, or, as above, induction on both $p$ and $q$, yeilding $\texttt{refl}_x \circ \texttt{refl}_x \equiv \texttt{refl}_x$. We would merely have three different elements of the same type.

We will now state some results without the obvious proofs. For $\Pi_{A : \mathscr{U}} \Pi_{x, y, z, w : A}$, $p : x = y$, $q : y = z$, $r : z = w$:

- $p = p \circ \texttt{refl}_y$ and $p = \texttt{refl}_x \circ p$
- $p^{-1} \circ p = \texttt{refl}_y$ and $p \circ p^{-1} = \texttt{refl}_x$
- $(p^{-1})^{-1} = p$
- $(p \circ q) \circ r = p \circ (q \circ r)$

Given a type $A$ with point $a : A$, we define its loop space $\Omega(A, a)$ to be the type $a =_A a$; we could concatenate this to $\Omega A$ if $a$ is understood from the context. Since any two elements of $\Omega A$ are paths with the same start and endpoints, we have $\Omega A \times \Omega A \rightarrow \Omega A$. It can also be fruitful to consider the loop space of a loop space of $A$, the space of 2-dimensional loops, written $\Omega^2(A, a)$, represented as $\texttt{refl}_a =_{a =_A a} \texttt{refl}_a$.

The Eckmann-Hilton theorem can be stated as $\Omega^2(A) \times \Omega^2(A) \rightarrow \Omega^2(A)$ being commutative: $\alpha \circ \beta = \beta \circ \alpha$ for any $\alpha, \beta : \Omega^2(A)$.

First, notice that $\Omega A \times \Omega A \rightarrow \Omega A$ induces an operation:

In the following diagram,

Composing the two upper and lower paths, we get $p \circ r, q \circ s : a = c$. The horizontal composition can be written as $\alpha \star \beta : p \circ r = q \circ s$ defined as follows. First, we define $\alpha \circ_r r = p \circ_r = q \circ r$ by path induction on $r$ so that

where $\texttt{ru}_p = p \circ \texttt{refl}_b$ is the right unit lemma, which we previously mentioned. We can also define $q \circ_l \beta : q \circ r = q \circ s$ by induction on $q$ so that

where $\texttt{lu}_r$ denotes the left unit law. The operations $\circ_l$ and $\circ_r$ are called whiskering.

```
Definition whiskerL {A : Type} {x y z : A} (p : x = y)
{q r : y = z} (h : q = r) : p @ q = p @ r
:= 1 @@ h.
Definition whiskerR {A : Type} {x y z : A} {p q : x = y}
(h : p = q) (r : y = z) : p @ r = q @ r
:= h @@ 1.
```

Next, since $\alpha \circ_r r$ and $q \circ_l \beta$ are composable 2-paths, we can define horizontal composition by:

Now, suppose that $a \equiv b \equiv c$ so that all paths $p, q, r, s$ are elements of $\Omega(A, a)$, and assume moreover that $p \equiv q \equiv r \equiv s \equiv \texttt{refl}_a$, so that $\alpha : \texttt{refl}_a = \texttt{refl}_a$ and $\beta : \texttt{refl}_a = \texttt{refl}_a$ are composable in both orders. In this case, we have:

The foregoing fact, known as the Eckmann-Hilton argument comes from classical homotopy theory and is used later to show that higher homotopy groups of a type are always abelian groups.

```
Definition eckmann_hilton {A : Type} {x:A} (p q : 1 = 1 :> (x = x)) : p @ q = q @ p :=
(whiskerR_p1 p @@ whiskerL_1p q)^
@ (concat_p1 _ @@ concat_p1 _)
@ (concat_1p _ @@ concat_1p _)
@ (concat_whisker _ _ _ _ p q)
@ (concat_1p _ @@ concat_1p _)^
@ (concat_p1 _ @@ concat_p1 _)^
@ (whiskerL_1p q @@ whiskerR_p1 p).
```

A pointed type $(A, a)$ is a type $A : \mathscr{U}$ together with a point $a : A$ called its basepoint. We write $\mathscr{U}_\bullet :\equiv \Sigma_{A : \mathscr{U}}$ for the type of pointed types in universe $\mathscr{U}$.

Given a pointed type $(A, a)$, we can define the loop space of $(A, a)$ to be the following pointed type:

An element of it will be called a loop at a. For $n : \mathbb{N}$, the n-fold iterated loop space $\Omega^n(A, a)$ of a pointed type $(A, a)$ is defined recursively by:

An element of it will be called an n-loop at $a$.

## Functions are functors

From a type theoretic perspective, functions should respect equality; topologically, this corresponds to saying that every function is continuous (or preserves paths).

Given function $f : A \rightarrow B$, then for $x, y : A$, there is an operation

$\texttt{ap}_f$ can be read as the application of a function to a path.

```
Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y
:= match p with idpath => idpath end.
```

To provide a simple proof, it suffices to assume that $p$ is $\texttt{refl}_x$. In this case, we may define $\texttt{ap}_f(p) :\equiv \texttt{refl}_{f(x)} f(x) = f(x)$. We will often write $\texttt{ap}_f(p)$ as $f(p)$, and this matches the common category theory convention of using the same symbol for application of a functor to objects and morphisms.

We will now provide some facts about $\texttt{ap}_f$ without proof.

- $\texttt{ap}_f(p \circ q) = \texttt{ap}_f(p) \circ \texttt{ap}_f(q)$
- $\texttt{ap}_f(p^{-1}) = \texttt{ap}_f(p)^{-1}$
- $\texttt{ap}_g(\texttt{ap}_f(p)) = \texttt{ap}_{g \circ f}(p)$
- $\texttt{ap}_{\texttt{id}_A} = p$

These are themselves paths, which have to satisfy coherence laws, as usual.

## Type families are fibrations

If $\Pi_{x : A} B(x)$ and $p : x = y$, then $f(x) : B(x)$ and $f(y) : B(y)$ are elements of distinct types, so that a priori, we cannot even ask whether they are equal. The misssing ingredient is that $p$ itself gives us a way to relate $B(x)$ and $B(y)$. This problem was stated as indiscrenability of identicals in our previous note.

Transport lemma. Suppose $P$ is a type family over $A$ and $p : x =_A y$, then there is a function $p_\star : P(x) \rightarrow P(y)$.

Let $D : \Pi_{x, y : A}(x = y) \rightarrow \mathscr{U}$ be the type family defined by:

then we have the function

so that the induction principle gives us $\texttt{ind}_{=A}(D, d, x, y, p) : P(x) \rightarrow P(y)$.

Sometimes, it is necessary to notate the type family $P$ in which the transport operation happens:

Topologically, the transport lemma can be viewed as a "path lifting" operation on a fibration. We think of a type famiy $P : A \rightarrow \mathscr{U}$ as a fibration with base space $A$, with $P(x)$ being the fiber over $x$, and with $\Sigma_{x : A} P(x)$ being the total space of the fibration, with first projection $\Sigma_{x : A} P(x) \rightarrow A$.

The defining property of a fibration is that given a path $p : x = y$ in the base space $A$ and a point $u : P(x)$ in a fiber over $x$, we may lift we may lift the path $p$ to a total space starting at $u$, and this lifting can be done continuously. The point $p_\star(u)$ can be thought of as the other endpoint of this lifted path.

```
Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
match p with idpath => u end.
```

We now state path lifting property without proof. Let $P : A \rightarrow \mathscr{U}$ be a type family over $A$, and assume we have $u : P(x)$ for some $x : A$. Then, for $p : x = y$, we have:

in $\Sigma_{x : A} P(x)$, such that $\texttt{pr}_1(\texttt{lift}(u, p)) = p$.

```
Definition equiv_path_sigma `(P : A -> Type) (u v : sigT P)
: {p : u.1 = v.1 & p # u.2 = v.2} <~> (u = v)
:= Build_Equiv _ _ (path_sigma_uncurried P u v) _.
```

In classical homotopy theory, a fibration is defined as a map for which there exist liftings of paths, while in contrast, we have shown that in type theory, every type family comes with a specified "lifting function".

When the type family $P : A \rightarrow \mathscr{U}$ is regarded as a fibration, the base is $A$, and the total space is $\Sigma_{x : A} P(x)$. We may also refer to the dependent function $\Pi_{x : A} P(x)$ as the section of the fibration $P$, and we may say that something happens fiberwise if it happens for each $P(x)$. For instance, a section $f : \Pi_{x : A} P(x)$ shows that $P$ is "fiberwise inhabited".

We can now prove a dependent version of the lemma $\texttt{ap}_f : (x =_A y) \rightarrow (f(x) =_B f(b))$ as follows. Given $\Pi_{x : A} P(x)$, we can define a non-dependent version of the function $f' : A \rightarrow \Sigma_{x : A} P(x)$ by setting $f'(x) :\equiv (x, f(x))$ and consider $f'(p) : f'(x) = f'(y)$. Since $\texttt{pr}_1 \circ f' \equiv \texttt{id}_A$, we have $\texttt{pr}_1(f'(p)) \equiv p$; thus $f'(p)$ does "lie over" $p$ in this sense. However, it is not obvious from the type of $f'(p)$ that it lies over any specific path in $A$ (in this case $p$), which is sometimes important.

The solution is to use the transport lemma; we have a canonical path $\texttt{lift}(u, p)$ from $(x, u)$ to $(u, p_\star(u))$, which lies over $p$. Thus, any path from $u : P(x)$ to $v : P(y)$ lying over $p$ should factor through $\texttt{lift}(u, p)$.

Dependent map. Suppose $f : \Pi_{x : A} P(x)$, we have a map

```
(** Similarly, dependent functions act on paths; but the type is a bit more subtle.
If [f : forall a:A, B a] and [p : x = y] is a path in [A], then [apD f p] should somehow
be a path between [f x : B x] and [f y : B y]. Since these live in different types,
we use transport along [p] to make them comparable: [apD f p : p # f x = f y].
The type [p # f x = f y] can profitably be considered as a heterogeneous or
dependent equality type, of "paths from [f x] to [f y] over [p]". *)
Definition apD {A : Type} {B : A->Type} (f : forall a: A, B a) {x y : A} (p : x=y):
p # (f x) = f y
:=
match p with idpath => idpath end.
```

We prove it as follows. Let $D : \Pi_{x, y : A} (x = y) \rightarrow \mathscr{U}$ be the type family defined by

Then $D(x, x, \texttt{refl}_x)$ is ($\texttt{refl}_x)_\star = f(x)$. Then we get $D(x, x, \texttt{refl}_x) \equiv f(x) = f(x)$. Thus, we find the function:

and now, path induction gives us $\texttt{apd}_f(p) : p_\star(f(x)) = f(y)$ for each $p : x = y$.

We will refer generally to paths which "lie over paths" in this sense as dependent paths. Since a non-dependently typed function is a special case of a dependently typed function, we have the following relation between $\texttt{apd}_f$ and $\texttt{ap}_f$:

If $P : A \rightarrow \mathscr{U}$ is defined by $P(x) :\equiv B$ for a fixed $B : \mathscr{U}$, then for any $x, y : A$, $p : x = y$, and $b : B$, we have a path:

The corresponding Coq code looks like:

```
(** Transporting in a constant fibration. *)
Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
: transport (fun x => B) p y = y.
Proof.
destruct p. exact 1.
Defined.
```

In English, it suffices to assume that $y$ is $x$, and $p$ is $\texttt{refl}_x$. But $\texttt{transport}^P(\texttt{refl}_x, b) \equiv b$, so in this case, we have to prove that $b = b$, which can be discharged by $\texttt{refl}_b$.

By concatenating $\texttt{transportconst}$ and its inverse, we obtain:

Let us now dump a few definitions and lemmas in Coq:

```
(** In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. *)
Lemma apD_const {A B} {x y : A} (f : A -> B) (p : x = y) :
apD f p = transport_const p (f x) @ ap f p.
Proof.
destruct p; reflexivity.
Defined.
```

```
(** Transporting in a pulled back fibration. *)
Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
(p : x = y) (z : P (f x))
: transport (fun x => P (f x)) p z = transport P (ap f p) z.
Proof.
destruct p; reflexivity.
Defined.
```

```
Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) :
f y (p # z) = (p # (f x z)).
Proof.
by induction p.
Defined.
```

```
Definition transport_pp {A : Type} (P : A -> Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
p @ q # u = q # p # u :=
match q with idpath =>
match p with idpath => 1 end
end.
```

## Homotopies and equivalences

It is now time to talk about identifications between types and functions. For two functions to be equal, they must agree on every element in their domains. Let $f, g : \Pi_{x : A} P(x)$ be two sections of of the type family $P : A \rightarrow \mathscr{U}$. A homotopy from $f$ to $g$ is the dependent function:

Note that this is not the same thing as $f = g$, but we will revisit this when we talk about the univalence axiom.

Just as functions in type theory are automatically functors, homotopies are automatically natural transforms:

Suppose $H : f \sim g$ is a homotopy between functions $f, g : A \rightarrow B$ and let $p : x =_A y$. Then we have:

We may also draw the commutative diagram:

To supply a proof by induction, we may assume that $p$ is $\texttt{refl}_x$. Since $\texttt{ap}_f$ and $\texttt{ap}_g$ compute on reflexivity, in this case, what we must show is:

But this follows since both sides are equal to $H(x)$.

```
(** Naturality of [ap]. *)
Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) :
(ap f q) @ (p y) = (p x) @ (ap g q)
:=
match q with
| idpath => concat_1p _ @ ((concat_p1 _) ^)
end.
```

Let $H : f \sim \texttt{id}_A$ be a homotopy with $f : A \rightarrow A$. Then for any $x : A$, we have:

That is, $f(H x) \circ H x = H(f x) \circ H x$. We can now whisker by $(H x)^{-1}$ to cancel $H x$ obtaining:

```
(** Naturality of [ap] at identity. *)
Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
(ap f q) @ (p y) = (p x) @ q
:=
match q with
| idpath => concat_1p _ @ ((concat_p1 _) ^)
end.
```

Moving onto types from a traditional perspective, one may say that a function $f : A \rightarrow B$ is an isomorphism if there is a function $g : B \rightarrow A$ such that composites $f \circ g \sim \texttt{id}_B$ and $g \circ f \sim \texttt{id}_A$. A homotopical perspective suggests that this should be called a homotopy equivalence, and equivalence of higher groupoids from a category theoretic perspective. However, the type

is poorly behaved. For instance, a single function $f : A \rightarrow B$, there may be multiple unequal multiple inhabitants. This is closely related to the observation in higher category theory that one often needs to consider adjoint equivalences. Let us instead do the following:

Given $f : A \rightarrow B$, a quasi-inverse of $f$ is a triple $(g, \alpha, \beta)$ consisting of a function $g : B \rightarrow A$ and homotopies $\alpha : f \circ g \sim \texttt{id}_B$ and $\beta : g \circ f \sim \texttt{id}_A$. The quasi-inverse of $f$ is denoted $\texttt{qinv}(f)$.

In general, we will reserve the use of the term isomorphism in the special case when $A$ and $B$ behave like sets, where it is unproblematic. Let us define equivalence for an improved notation $isequiv(f)$ with the following properties:

- For each $f: A \rightarrow B$, there is a function $\texttt{qinv}(f) \rightarrow \texttt{isequiv}(f)$
- Similarly, for each $f$, we have $\texttt{isequiv}(f) \rightarrow \texttt{qinv}$
- For any two inhabitants $e_1, e_2 : \texttt{isequiv}(f)$, we have $e_1 = e_2$

Later, we will see many different definitions of $\texttt{isequiv}(f)$, all of which satisfy these properties. For now, let us be satiated with the easiest such definition:

For the moment, the main takeaway is that we have a well-defined meaning for "$f$ is an equivalence" by exhibiting a quasi-inverse to it. We can write

Type equivalence is an equivalence relation on $\mathscr{U}$. More specifically,

- For any $A$, the identity fuction $\texttt{id}_A$ is an equivalence; $A \simeq A$
- For any $f : A \simeq B$, we have an equivalence $f^{-1} : B \simeq A$
- For any $f : A \simeq B$, $g : B \simeq C$, we have $g \circ f : A \simeq C$

## The higher groupoid structure of type formers

The goal now is to form new types corresponding to the type theoretic ones from our previous note. For instance, a cartesian product $A = B \times C$, $x :\equiv (b, c)$, $y :\equiv (b', c')$, then we have:

In more traditional language, two ordered pairs are equal just when their components are equal. The higher structure of identity types can also be expressed in terms of those equivalences. Similarly, when a type family $P : A \rightarrow \mathscr{U}$ is built up fiberwise, up to homotopy, in terms of the corresponding operations on the data that went into $P$. For instance, $P(x) = B(x) \times C(x)$. Then, we have:

Finally, the type forming rules are also functorial, and if a function $f$ is built from this functorially, then the operations $\texttt{ap}_f$ and $\texttt{apd}_f$ can be computed based on the corresponding ones on the data going into into $f$. For instance, $g : B \rightarrow B'$ and $h : C \rightarrow C'$, and we define $f : B \times C \rightarrow B' \times C'$ by $f(b,c) :\equiv (g(b), h(c))$, then modulo equivalence, we can identify $\texttt{ap}_f$ with $(\texttt{ap}_g, \texttt{ap}_h)$.

Since our philosophy states that identity types are defined uniformly for all types by their induction principle, so we cannot redefine them to be different for different types. The previous note is insufficient to prove the desired theorems for two type formers: $\Pi$ types and universes. For $\Pi$ types, we use the axiom of functional extensionality, and for universes, we use the univalence axiom, which we will state shortly.

It is, however, important to note that not all identity types can be determined by induction over the construction of types. Counterexamples include most non-trivial higher inductive types (HITs). For instance, calculating the identity types of types $\mathbb{S}^n$ is equivalent to calculating the higher homotopy groups of spheres, a field of research in algebraic topology.

## Cartesian product types

We have the following function which we will prove is an equivalence by exhibiting its quasi-inverse:

```
Definition equiv_path_prod {A B : Type} (z z' : A * B)
: (fst z = fst z') * (snd z = snd z') <~> (z = z')
:= Build_Equiv _ _ (path_prod_uncurried z z') _.
```

We can now denote this by

It can be helpful view $\texttt{pair}^=$ as an introduction rule for $x = y$. to The elimination rules can then be written out as:

For $p : \texttt{pr}_1 x = \texttt{pr}_1 y$ and $q : \texttt{pr}_2 x = \texttt{pr}_2 y$, we get the following propositional uniqueness principle:

```
Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
(z : P a * Q a)
: transport (fun a => P a * Q a) p z = (p # (fst z), p # (snd z))
:= match p with idpath => 1 end.
```

```
Definition ap_functor_prod {A A' B B' : Type} (f : A -> A') (g : B -> B')
(z z' : A * B) (p : fst z = fst z') (q : snd z = snd z')
: ap (functor_prod f g) (path_prod _ _ p q)
= path_prod (functor_prod f g z) (functor_prod f g z') (ap f p) (ap g q).
Proof.
destruct z as [a b]; destruct z' as [a' b'].
simpl in p, q. destruct p, q. reflexivity.
Defined.
```

## $\Sigma$-types

Suppose we have a path $p : w = w'$ in $\Sigma_{x : A} P(x)$. Then, we get $\texttt{pr}_1(p) : \texttt{pr}_1(w) = \texttt{pr}_1(w')$. However, we cannot ask if $\texttt{pr}_1(w)$ is identical to $\texttt{pr}_1(w')$, since they don't have the same type, but we can transport $\texttt{pr}_2(w)$ along the path $\texttt{pr}_1(p)$, and this gives us an element of the same type as $\texttt{pr}_2(w')$. By path induction, we obtain the path $\texttt{pr}_1(p)_\star(\texttt{pr}_2(w) = \texttt{pr}_2(w'))$, which we can regard as the type of paths from $\texttt{pr}_2(w)$ to $\texttt{pr}_2(w')$.

We have already proved this previously, in the path lifting property. As usual, let us also deduce a propositional uniqueness principle as a special case:

For $z : \Sigma_{x : A} P(x)$, we have $z = (\texttt{pr}_1(z), \texttt{pr}_2(z))$

```
Definition eta_sigma `{P : A -> Type} (u : sigT P)
: (u.1; u.2) = u
:= 1.
```

Suppose we have the type families $P : A \rightarrow \mathscr{U}$ and $Q : (\Sigma_{x : A} P(x)) \rightarrow \mathscr{U}$, then we can construct the type family over $A$ defined by:

For any path $p : x = y$, we have $(u, z) : \Sigma_{u : P(x)} Q(x, u)$, we have

```
(** Dependent transport is the same as transport along a [path_sigma]. *)
Definition transportD_is_transport
{A : Type} (B : A->Type) (C: sigT B -> Type)
(x1 x2 : A) (p : x1 = x2) (y : B x1) (z : C (x1 ; y))
: transportD B (fun a b => C (a ; b)) p y z
= transport C (path_sigma' B p 1) z.
Proof.
destruct p. reflexivity.
Defined.
```

## The unit type

Let us briefly discuss the type $\mathbb{1}$.

For $x, y : \mathbb{1}$, $(x = y) \simeq \mathbb{1}$.

It's tempting to do this proof by $\mathbb{1}$-induction, but we'd get stuck and be unable to perform a path induction on $p : \star = \star$. A function $(x = y) \rightarrow \mathbb{1}$ is easy to define by sending everything to $\star$. We may assume, by path induction, that $x = y = \star$, in which case, we have $\texttt{refl}_\star : x = y$, yielding a constant function $\mathbb{1} \rightarrow (x = y)$. To show the inverses, consider an element $u : \mathbb{1}$, and safely assume that $u = \star$, but this is also the result of the composite $\mathbb{1} \rightarrow (x = y) \rightarrow \mathbb{1}$.

```
Definition equiv_path_unit (z z' : Unit) : Unit <~> (z = z')
:= Build_Equiv _ _ (path_unit_uncurried z z') _.
```

$\Pi$-types and functional extensionality

We expect type $f = g$ of paths from $f$ to $g$ in $\Pi_{x : A} B(x)$ to be equivalent to the type of pointwise paths:

The functional extensionality axiom says that the above relation is an equivalence. This implies that there is a quasi-inverse:

We can regard this as an introduction rule for the type $f = g$.

```
Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
f == g -> f = g
:=
(@apD10 A P f g)^-1.
```

From this point of view, $\texttt{happly}$ is an elimination rule, while the homotopies witnessing $\texttt{funext}$ as quasi-inverse to $\texttt{happly}$ become a propositional computation rule:

and a propositional uniqueness principle,

We can also compute identity, inverses, and compositions in $\Pi$-types; they are simply given by pointwise operations:

For the non-dependent function $A \rightarrow B$, a special case of the corresponding dependent function, the rules for transport are quite straightforward:

Given type families $A, B : X \rightarrow \mathscr{U}$, $p : x =_X y$, $f : A(x) \rightarrow B(x)$, and $g : A(y) \rightarrow B(y)$, we have an equivalence:

```
(** Usually, a dependent path over [p:x1=x2] in [P:A->Type] between [y1:P x1] and [y2:P x2]
is a path [transport P p y1 = y2] in [P x2]. However, when [P] is a function space,
these dependent paths have a more convenient description: rather than transporting
the argument of [y1] forwards and backwards, we transport only forwards but on both sides
of the equation, yielding a "naturality square". *)
Definition dpath_arrow
{A:Type} (B C : A -> Type) {x1 x2 : A} (p : x1=x2)
(f : B x1 -> C x1) (g : B x2 -> C x2)
: (forall (y1 : B x1), transport C p (f y1) = g (transport B p y1))
<~>
(transport (fun x => B x -> C x) p f = g).
Proof.
destruct p.
apply equiv_path_arrow.
Defined.
```

Moreover, if $q : p_\star(f) = g$ corresponds under this equivalence to $\hat{q}$, then for $a : A(x)$, the path

is equal to the composite:

## Universes and the univalence axiom

For types $A, B : \mathscr{U}$, there is a certain function

defined as follows.

```
Definition equiv_path (A B : Type) (p : A = B) : A <~> B
:= Build_Equiv _ _ (transport (fun X:Type => X) p) _.
```

The univalence axiom can be stated as the $\texttt{idtoequiv}$ being an equivalene.

```
Definition equiv_equiv_path (A B : Type) : (A = B) <~> (A <~> B)
:= (equiv_path_universe A B)^-1%equiv.
```

As previously done, it is fruitful to break up this equivalence into:

- Introduction rule:

- Elimination rule:

- Propositional computation rule:

- Propositional equivalence principle, for any $p : A = B$

We can also identify reflexvivity, concatenation, and inverses of equalities:

For any type family $B : A \rightarrow \mathscr{U}$ and $x, y : A$ with a path $p : x = y$ and $u : B(x)$, we have:

## Identity type

Just as the type $a =_A a'$ is characterized upto isomorphism, with a separate definition for each $A$, there is no simple characterizion of the type $p =_{a =_A a'} q$ of paths between paths $p, q : a =_A a'$.

If $f : A \rightarrow B$ is an equivalence, then for all $a, a' : A$ so is:

To prove this, let $f^{-1}$ be a quasi inverse of $f$ with the homotopies:

The quasi-inverse of $ap_f$ is essentially:

However, in order to obtain an element of $a =_A a'$ from $\texttt{ap}_{f^{-1}}(q)$ we must concatenate with $\beta_\alpha^{-1}$ and $\beta_{\alpha'}$ on either side. For $p : a =_A a'$ and $q : f(a) =_B f(a')$, we have:

We can prove the latter by simply canceling inverse paths.

Thus, for some type $A$, we have a full characterizion of $a =_A a'$ and the type $p =_{a_{=A}} q$ is determined as well. For example, paths $p = q$ where $p, q : f =_{\Pi_{x : A} B(x)} g$ are equivalent to homotopies:

Next, we consider transport in families of paths; ie.e. transport in $C : A \rightarrow \mathscr{U}$ where each $C(x)$ is an identity type.

For any $A$ and $a : A$ with $p : x_1 = x_2$, we have

We now dump some lemmas for $\texttt{transport}$:

```
Definition transport_paths_FlFr {A B : Type} {f g : A -> B} {x1 x2 : A}
(p : x1 = x2) (q : f x1 = g x1)
: transport (fun x => f x = g x) p q = (ap f p)^ @ q @ (ap g p).
Proof.
destruct p; simpl.
exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
Defined.
```

```
Definition transport_paths_FlFr_D {A : Type} {B : A -> Type}
{f g : forall a, B a} {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1)
: transport (fun x => f x = g x) p q
= (apD f p)^ @ ap (transport B p) q @ (apD g p).
Proof.
destruct p; simpl.
exact ((ap_idmap _)^ @ (concat_1p _)^ @ (concat_p1 _)^).
Defined.
```

```
Definition transport_paths_lr {A : Type} {x1 x2 : A} (p : x1 = x2) (q : x1 = x1)
: transport (fun x => x = x) p q = p^ @ q @ p.
Proof.
destruct p; simpl.
exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
Defined.
```

## Natural numbers

We will introduce an encode-decode method to define $\mathbb{N}$. The codes for identites are a type family:

defined by double recursion over $\mathbb{N}$ as follows:

We also define, by recursion, a dependent function $r : \Pi_{n : \mathbb{N}} \texttt{code}(n, n)$ with

For all $m, n : \mathbb{N}$, we have $(m = n) \simeq \texttt{code}(m, n)$

```
Definition equiv_path_nat {n m} : (n =n m) <~> (n = m)
:= Build_Equiv _ _ (@path_nat n m) _.
```

## Universal properties

By combining the path computation rules described in the previous sections, we can show that various type forming operations satisfy the expected universal properties, interpreted in a homotopical way as equivalences.

defined by $f \mapsto (\texttt{pr}_1 \circ f, \texttt{pr}_2 \circ f)$. To prove that this is an equivalence, given $f : X \rightarrow A \times B$, the round-trip composite yields the function:

We also have a dependently typed version of this universal property:

defined as before.

```
(* First, a positive version of the universal property *)
Definition equiv_prod_ind `(P : A * B -> Type)
: (forall (a : A) (b : B), P (a, b)) <~> (forall p : A * B, P p)
:= Build_Equiv _ _ (prod_ind P) _.
```

```
(* Now the negative universal property. *)
Definition prod_coind_uncurried `{A : X -> Type} `{B : X -> Type}
: (forall x, A x) * (forall x, B x) -> (forall x, A x * B x)
:= fun fg x => (fst fg x, snd fg x).
```

Since $\Sigma$ types are a generalization of cartesian product types, we can straightaway jump to the dependently typed version; if we have a type $X$ and type families $A : A \rightarrow \mathscr{U}$ and $P : \Pi_{x : A} A(x) \rightarrow \mathscr{U}$, then we have:

Note that $\Sigma_{g : \Pi_{x : X} A(x)} \Pi_{x : X} P(x, g(x))$ can be read as "there exists a choice function $g : \Pi_{x : X} A(x)$ such that for all $x : X$, we have $P(x, g(x))$". The classical mathemtician may find that the axiom of choice doesn't carry its usual meaning.

In the case of cartesian products, the non-dependent version simply expresses the cartesian closure adjuction:

Some other induction principles are also part of universal properties of this sort. For instance, path induction is the right-to-left direction of an equivalence as follows:

However, for inductive types with recursion, such as natural numbers, have more complicated universal properties, as we intend to describe later.

As such, we have described the usual universal property of a cartesian product, but the reader may wonder about limits and colimits of types. For pullbacks, the expected explicit construction works; given $f: A \rightarrow C$ and $g : B \rightarrow C$, we define:

For colimits, however, we need a new ingredient, which we will discuss later.