HoTT II: The essentials

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 is a set of points equipped with a topology, and a path betwen points and is represented by a continuous map where . The function can be thought of as giving a point at each moment in time. A homotopy between a pair of continuous maps , so that and , can be thought of as a continuous deformation from to .

The fundamental group of a fundamental -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 as a path between the start point and endpoint . can be thought of as a homotopy or a 2-path or 2-dimensional path. All of the basic constructions and axioms arises automatically from the induction principle for identity types. In other words, given the dependent functions:

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 of an identity type, then it suffices to perform the construction in the special case when are judgmentally the same, and is the reflexivity element .

The induction principle endows each type with the structure of an -groupoid, and each function between two types with the structure of the an -functor between 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 , , and . By induction, it suffices to consider the case when and . In this case, the type of and , in which we're trying to construct , are both equal to . Thus, in the reflexivity case, we can define to simply be . The general case therefore proceeds by the induction principle, and the conversion rule .

To state our second lemma:

The proof proceeds as follows: , every and every , we need to construct an inhabitant of . By induction on , it sufficces to assume that and is . In this case, the type of of is . By induction on , it suffices to assume that and is . In this case, is , and we have .

This proof raises the question of why an induction on is required at all, when we already have the equality . Indeed, we could have done an induction on yielding the computation rule , an induction on yielding the computation rule , or, as above, induction on both and , yeilding . We would merely have three different elements of the same type.

We will now state some results without the obvious proofs. For , , , :

Given a type with point , we define its loop space to be the type ; we could concatenate this to if is understood from the context. Since any two elements of are paths with the same start and endpoints, we have . It can also be fruitful to consider the loop space of a loop space of , the space of 2-dimensional loops, written , represented as .

The Eckmann-Hilton theorem can be stated as being commutative: for any .

First, notice that induces an operation:

In the following diagram,

Composing the two upper and lower paths, we get . The horizontal composition can be written as defined as follows. First, we define by path induction on so that

where is the right unit lemma, which we previously mentioned. We can also define by induction on so that

where denotes the left unit law. The operations and 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 and are composable 2-paths, we can define horizontal composition by:

Now, suppose that so that all paths are elements of , and assume moreover that , so that and 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 is a type together with a point called its basepoint. We write for the type of pointed types in universe .

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

An element of it will be called a loop at a. For , the n-fold iterated loop space of a pointed type is defined recursively by:

An element of it will be called an n-loop 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 , then for , there is an operation

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 is . In this case, we may define . We will often write as , 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 without proof.

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

Type families are fibrations

If and , then and are elements of distinct types, so that a priori, we cannot even ask whether they are equal. The misssing ingredient is that itself gives us a way to relate and . This problem was stated as indiscrenability of identicals in our previous note.

Transport lemma. Suppose is a type family over and , then there is a function .

Let be the type family defined by:

then we have the function

so that the induction principle gives us .

Sometimes, it is necessary to notate the type family 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 family as a fibration with base space , with being the fiber over , and with being the total space of the fibration, with first projection .

The defining property of a fibration is that given a path in the base space and a point in a fiber over , we may lift we may lift the path to a total space starting at , and this lifting can be done continuously. The point 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 be a type family over , and assume we have for some . Then, for , we have:

in , such that .

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 is regarded as a fibration, the base is , and the total space is . We may also refer to the dependent function as the section of the fibration , and we may say that something happens fiberwise if it happens for each . For instance, a section shows that is "fiberwise inhabited".

We can now prove a dependent version of the lemma as follows. Given , we can define a non-dependent version of the function by setting and consider . Since , we have ; thus does "lie over" in this sense. However, it is not obvious from the type of that it lies over any specific path in (in this case ), which is sometimes important.

The solution is to use the transport lemma; we have a canonical path from to , which lies over . Thus, any path from to lying over should factor through .

Dependent map. Suppose , 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 be the type family defined by

Then is (. Then we get . Thus, we find the function:

and now, path induction gives us for each .

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 and :

If is defined by for a fixed , then for any , , and , 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 is , and is . But , so in this case, we have to prove that , which can be discharged by .

By concatenating 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 be two sections of of the type family . A homotopy from to is the dependent function:

Note that this is not the same thing as , 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 is a homotopy between functions and let . Then we have:

We may also draw the commutative diagram:

To supply a proof by induction, we may assume that is . Since and compute on reflexivity, in this case, what we must show is:

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 be a homotopy with . Then for any , we have:

That is, . We can now whisker by to cancel 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 is an isomorphism if there is a function such that composites and . 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 , 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 , a quasi-inverse of is a triple consisting of a function and homotopies and . The quasi-inverse of is denoted .

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

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 , 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 " is an equivalence" by exhibiting a quasi-inverse to it. We can write

Type equivalence is an equivalence relation on . More specifically,

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 , , , 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 is built up fiberwise, up to homotopy, in terms of the corresponding operations on the data that went into . For instance, . Then, we have:

Finally, the type forming rules are also functorial, and if a function is built from this functorially, then the operations and can be computed based on the corresponding ones on the data going into into . For instance, and , and we define by , then modulo equivalence, we can identify with .

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: types and universes. For 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 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 as an introduction rule for . to The elimination rules can then be written out as:

For and , 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.

-types

Suppose we have a path in . Then, we get . However, we cannot ask if is identical to , since they don't have the same type, but we can transport along the path , and this gives us an element of the same type as . By path induction, we obtain the path , which we can regard as the type of paths from to .

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 , we have

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

Suppose we have the type families and , then we can construct the type family over defined by:

For any path , we have , 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 $𝟙$ .

For $𝟙$ , $𝟙$ .

It's tempting to do this proof by $𝟙$ -induction, but we'd get stuck and be unable to perform a path induction on . A function $𝟙$ is easy to define by sending everything to . We may assume, by path induction, that , in which case, we have , yielding a constant function $𝟙$ . To show the inverses, consider an element $𝟙$ , and safely assume that , but this is also the result of the composite $𝟙 𝟙$ .

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

-types and functional extensionality

We expect type of paths from to in 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 .

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, is an elimination rule, while the homotopies witnessing as quasi-inverse to become a propositional computation rule:

and a propositional uniqueness principle,

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

For the non-dependent function , a special case of the corresponding dependent function, the rules for transport are quite straightforward:

Given type families , , , and , 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 corresponds under this equivalence to , then for , the path

is equal to the composite:

Universes and the univalence axiom

For types , 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 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

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

For any type family and with a path and , we have:

Identity type

Just as the type is characterized upto isomorphism, with a separate definition for each , there is no simple characterizion of the type of paths between paths .

If is an equivalence, then for all so is:

To prove this, let be a quasi inverse of with the homotopies:

The quasi-inverse of is essentially:

However, in order to obtain an element of from we must concatenate with and on either side. For and , we have:

We can prove the latter by simply canceling inverse paths.

Thus, for some type , we have a full characterizion of and the type is determined as well. For example, paths where are equivalent to homotopies:

Next, we consider transport in families of paths; ie.e. transport in where each is an identity type.

For any and with , we have

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 encode-decode method to define . The codes for identites are a type family:

defined by double recursion over as follows:

We also define, by recursion, a dependent function with

For all , we have

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 . To prove that this is an equivalence, given , 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 types are a generalization of cartesian product types, we can straightaway jump to the dependently typed version; if we have a type and type families and , then we have:

Note that can be read as "there exists a choice function such that for all , we have ". 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 and , we define:

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