Here, we discuss concepts from Ch.2 of the HoTT book
The central idea is that types can be interpreted as higherdimensional groupoids in category theory, or spaces in homotopy theory. Space
The fundamental group of a fundamental
We will refer to
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
The induction principle endows each type with the structure of an
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
To state our second lemma:
The proof proceeds as follows:
This proof raises the question of why an induction on
We will now state some results without the obvious proofs. For

and 
and 

Given a type
The EckmannHilton theorem can be stated as
First, notice that
In the following diagram,
Composing the two upper and lower paths, we get
where
where
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
Now, suppose that
The foregoing fact, known as the EckmannHilton 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
Given a pointed type
An element of it will be called a loop at a. For
An element of it will be called an nloop at
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
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
We will now provide some facts about
These are themselves paths, which have to satisfy coherence laws, as usual.
Type families are fibrations
If
Transport lemma. Suppose
Let
then we have the function
so that the induction principle gives us
Sometimes, it is necessary to notate the type family
Topologically, the transport lemma can be viewed as a "path lifting" operation on a fibration. We think of a type famiy
The defining property of a fibration is that given a 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
in
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
We can now prove a dependent version of the lemma
The solution is to use the transport lemma; we have a canonical path
Dependent map. Suppose
(** 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
Then
and now, path induction gives us
We will refer generally to paths which "lie over paths" in this sense as dependent paths. Since a nondependently typed function is a special case of a dependently typed function, we have the following relation between
If
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
By concatenating
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
Note that this is not the same thing as
Just as functions in type theory are automatically functors, homotopies are automatically natural transforms:
Suppose
We may also draw the commutative diagram:
To supply a proof by induction, we may assume that
But this follows since both sides are equal to
(** 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
That is,
(** 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
is poorly behaved. For instance, a single function
Given
In general, we will reserve the use of the term isomorphism in the special case when

For each
, there is a function 
Similarly, for each
, we have 
For any two inhabitants
, we have
Later, we will see many different definitions of
For the moment, the main takeaway is that we have a welldefined meaning for "
Type equivalence is an equivalence relation on

For any
, the identity fuction is an equivalence; 
For any
, we have an equivalence 
For any
, , we have
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
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
Finally, the type forming rules are also functorial, and if a function
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:
It is, however, important to note that not all identity types can be determined by induction over the construction of types. Counterexamples include most nontrivial higher inductive types (HITs). For instance, calculating the identity types of types
Cartesian product types
We have the following function which we will prove is an equivalence by exhibiting its quasiinverse:
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
For
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.
types
Suppose we have a path
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
Definition eta_sigma `{P : A > Type} (u : sigT P)
: (u.1; u.2) = u
:= 1.
Suppose we have the type families
For any path
(** 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
For
It's tempting to do this proof by
Definition equiv_path_unit (z z' : Unit) : Unit <~> (z = z')
:= Build_Equiv _ _ (path_unit_uncurried z z') _.
We expect type
The functional extensionality axiom says that the above relation is an equivalence. This implies that there is a quasiinverse:
We can regard this as an introduction rule for the type
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,
and a propositional uniqueness principle,
We can also compute identity, inverses, and compositions in
For the nondependent function
Given type families
(** 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
is equal to the composite:
Universes and the univalence axiom
For types
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
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
We can also identify reflexvivity, concatenation, and inverses of equalities:
For any type family
Identity type
Just as the type
If
To prove this, let
The quasiinverse of
However, in order to obtain an element of
We can prove the latter by simply canceling inverse paths.
Thus, for some type
Next, we consider transport in families of paths; ie.e. transport in
For any
We now dump some lemmas for
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 encodedecode method to define
defined by double recursion over
We also define, by recursion, a dependent function
For all
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
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
Note that
In the case of cartesian products, the nondependent 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 righttoleft 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
For colimits, however, we need a new ingredient, which we will discuss later.