Spaces and Homotopy Theory

The source code for this module: PartII/Spaces.ard
The source code for the exercises: PartII/SpacesEx.ard

By now we have been mostly living in the world of propositions and sets, where the structure of the type x = y is degenerate so that we could think of it either as a mere propositional equality type or as a set of bijections between x and y if x y : \Set are sets (by univalence).

In this module we will undertake a brief detour to a nondegenerate side of homotopy type theory, where it becomes important that the type x = y is actually the type of paths between points x and y of a space.

We give several examples of datatypes of spaces, namely, spheres of various dimensions and the torus. One way to think about these types is as being generated not only by usual constructors, but also by path-constructors. The corresponding elimination principles are called higher recursion/induction.

Under the types-are-spaces view one can prove various theorems from homotopy theory. As an example, we discuss type-theoretic version of the classical proof that the fundamental group of the circle is isomorphic to integers. We also discuss the Eilenberg-Maclane spaces and equivalence between the category of connected pointed 1-types and the category of groups.

Types as spaces

In Part I we defined the equality type x = y, where x y : A, as the type I -> A of functions f such that f left ==> x and f right ==> y. We showed that this type behaves as you would expect equality to behave.

An obvious observation about this definition, which we now make explicitly: if we think of types as topological spaces, the type I as the interval and functions as continuous functions, then x = y is precisely the type of paths between x and y.

Let us explore this view a bit further. Consider a dependent type B : I -> \Type over I and a point b : B left. Eliminator for I, the function coe, can be used to lift the path left = right to a path p := path (\lam i => coe B b i) starting at b. This path in general goes across different types B i and lies in the heterogeneous type of paths Path B b (coe B b right). The right point transport B p b ==> (coe B b right) can be thought of as b transported along the path p.

Thus one can recognize that B defines a fibration over I and (\lam i => coe B b i) : \Pi (i : I) -> B i is a section of the fibration. More generally, dependent types B : A -> \Type correspond to fibrations p1 : \Sigma A B -> A (here p1 is the projection to the first component) over A with fibers B x over points x : A and the total space \Sigma A B. Note that if b : B x, then heterogeneous paths Path (\lam i => B (p @ i)) b (transport B p b) correspond to paths in the total space of fibration (that is a homogeneous path in \Sigma A B) lying over p. We will discuss examples of fibrations (namely, universal cover and path fibration) of topological nature in the section about the fundamental group of the circle below.

Another important remark: if f : A -> B is a “bijection” between types, namely, it satisfies isBij where \Set replaced with \Type, then the types A and B correspond to homotopy equivalent spaces and f is an equivalence. The function iso allows to construct a path between such spaces and the univalence says that the type of equivalences between types is equivalent to the type of paths between the types.

Spaces: spheres, torus

We can use datatypes with conditions to define the circle: just take the interval I and glue its two endpoints left and right. Specifically, we add the constructor base for the basepoint, the loop constructor loop I and conditions saying that endpoints of the loop evaluate to the basepoint: loop left ==> base, loop right ==> base.

\data Circle
  | base
  | loop I \with {
    | left => base
    | right => base
  }

Higher dimensional spheres are also easy to define using the construction called suspension. For a type A its suspension Susp A is a type with two points south and north and for every element a : A a path merid a i between north and south: merid a left ==> north, merid a right ==> south.

\data Susp (A : \Type)
   | south
   | north
   | merid A (i : I) \elim i {
      	| left => north
        | right => south
   }

The spheres can now be defined inductively as follows:

\func Sphere (n : Nat) : \Type \lp \oo
    | 0 => Susp Empty
    | suc n => Susp (Sphere n)

It is easy to see that the type Circle is equivalent to the type Sphere 1:

\func CircleToSphere1 (x : Circle) : Sphere 1
    | base => north
    | loop i => (path (merid north) *> inv (path (merid south))) @ i 

\func Sphere1ToCircle (x : Sphere 1) : Circle
    | south => base
    | north => base
    | merid north i => loop i
    | merid south i => base
    | merid (merid () _) _

Exercise 1: Prove that CircleToSphere1 and Sphere1ToCircle are mutually inverse.

Consider another elementary topological space: the torus. We can directly apply the standard way of constructing the torus by identifying opposite sides of the square.

\data Torus
  | point
  | line1  I \with { left => point | right => point }
  | line2  I \with { left => point | right => point }
  | face I I \with {
    | left, i => line2 i
    | right, i => line2 i
    | i, left => line1 i
    | i, right => line1 i
  }

Exercise 2: Prove that Torus is equivalent to the direct product \Sigma Circle Circle of circles.

Higher induction principles

We have shown how to define spaces using the interval type and ordinary datatypes with conditions. The types of spaces defined in this way thus satisfy the ordinary elimination principle for datatypes with conditions.

Alternatively, we can look at the type of a space as being generated by ordinary constructors, called point-constructors, together with higher level path-constructors. For example, the circle is generated by the point-constructor base and the path-constructor loop : base = base, the 2-sphere is generated by base and 2-path-constructor surf : idp {base} = idp {base}, and so on.

Let us illustrate the idea of how to formulate the higher recursion and higher induction principles in the simple case of the circle. The higher recursion principle for the circle says, that a function from Circle to a type B can be defined by choosing a point b : B and a loop l : b = b in B.

\func circRec {B : \Type} {b : B} (l : b = b) (x : Circle) : B \elim x 
    | base => b
    | loop i => l @ i

If we denote circRec {b} l as f : Circle -> B, then f base ==> b and pmap f (path loop) = l.

This can be generalized to the higher induction principle, that is to the case when B : Circle -> \Type is a dependent type. In that case we should pick a point b : B base and specify a dependent loop in B. Since we do have in Arend heterogeneous path types, we can specify a dependent loop simply as an element in Path (\lam i => B (loop i)) b b. However, in some cases it is more convenient to use characterisation of dependent loops in terms of homogeneous path types: it can be shown that dependent loops correspond to paths transport B (path loop) b = b.

\func concat {A : I -> \Type} {a : A left} {a' a'' : A right} (p : Path A a a') (q : a' = a'') : Path A a a'' \elim q
  | idp => p

\func circInd (B : Circle -> \Type) (b : B base) (l : transport B (path loop) b = b) (x : Circle) : B x \elim x
  | base => b
  | loop i => (concat {\lam i => B (loop i)} (path (\lam i => coe (\lam j => B (loop j)) b i)) l) @ i

Below, while proving theorems about the fundamental group, we will see that this induction principle is useful.

The fundamental group

In the module Equality we showed how the equality type of a 1-type X gives rise to a groupoid structure on X. This is precisely the groupoid of paths in the space X: morphisms between points x : X and y : Y are paths between x and y. In particular, the loops x = x at a point x : X form a group with composition as the group operation. This group pi1(X, x) is called the fundamental group of X. In the Arend standard library the corresponding instance of the class Group is called Aut.

-- The instance of 'Group' defined in 'Algebra.Group.Aut' 
\instance Aut {A : \1-Type} (a : A) : Group (a = a)
  | ide => idp
  | * => *>
  | ide-left => idp_*>
  | ide-right _ => idp
  | *-assoc => *>-assoc
  | inverse => inv
  | inverse-left => inv_*>
  | inverse-right => *>_inv

\func pi1-1 (X : \1-Type) (x : X) => Aut x

\func pi1Mult {X : \1-Type} {x : X} (a b : pi1-1 X x) => a * b

Assume X is connected, that is for all pairs x y : X the proposition TruncP (x = y) holds, where TruncP is the propositional truncation. It is easy to see, that the definition pi1(X, x) does not depend on x in the sense that the groups pi1-1(X, x) for different choice of x are isomorphic. This group assigned to a space is one of the simplest examples of an algebraic invariant of a space: the fundamental groups of homotopy equivalent spaces are isomorphic.

Exercise 3: Let X : \1-Type be connected. Prove that the groups pi1-1 X x and pi1-1 X y are isomorphic for all x y : X.

The definition of pi1-1 above can, of course, be generalized from 1-types to arbitrary types by means of truncation.

\truncated \data Trunc1 (A : \Type) : \1-Type
  | trunc A

\func pi1 (X : \Type) (x : X) : Group => pi1-1 (Trunc1 X) (trunc x)

\truncated \data Trunc0 (A : \Type) : \Set
  | trunc A

-- Equivalently, we can truncate 'x = x'.
-- The group structure 'Aut' can be straightforwardly translated to this case.
\func pi1' (X : \Type) (x : X) : \Set => Trunc0 (x = x)

Exercise 3 implies that pi1 maps connected pointed spaces to groups:

\func isConnected (X : \Type) => \Pi (x y : X) -> TruncP (x = y)

-- The class 'Pointed' is defined in 'Homotopy.Pointed'.
\func pi1 (A : \Sigma (X : Pointed) (isConnected X)) : Group  => pi1-1 (Trunc1 A.1) (trunc base)

As we will see later in this module, there is an inverse function K1 : Group -> \Sigma (X : Pointed) (isConnected X), called the Eilenberg-Maclane space. The corresponding functors of pi1 and K1 establish equivalence of the category of pointed connected 1-types and the category of groups.

The fundamental group of the circle

Let us now consider an example of a calculation of the fundamental group. We will outline the proof from the Arend standard library that for Sphere1 holds (base1 = base1) = Int, where Sphere1 is Circle and base1 is base in the notation we used above. This implies that pi1 Sphere1 base1 = Int as well as that Sphere1 is 1-type.

The type-theoretic proof of (base1 = base1) = Int follows quite closely the classical homotopy-theoretic proof. First note, that it is very easy to construct a “winding” homomorphism from the group Int to the group base1 = base1, which sends the generator 1 to the generator path loop:

\func wind (x : Int) : base1 = base1
  | pos 0 => idp
  | pos (suc n) => wind (pos n) *> path loop
  | neg (suc n) => wind (neg n) *> inv (path loop)

In order to construct the inverse map we will need to define a fibration over the circle, called the universal cover. This amouts to constructing a specific dependent type, which we denote as code.

Geometrically the universal cover of the circle is a winding of the real line over the circle and can be visualized as a helix. Note that code x would be the fiber over x and \Sigma (x : Sphere1) (code x) the total space, that is the real line in our case. If y : code base1 is a point in the fiber over base1, then a loop l : base1 = base1 can be lifted to a path y = transport code l y in the covering space, where transport code l y is a point in the same fiber.

This gives us a map from loops base1 = base1 to points in the fiber over base1. We can identify the fiber with Int so that the map becomes a homomorphism of groups: simply set code base1 ==> Int and define code (loop i) in such a way that transporting of n along path loop results in n + 1. The latter can be easily done by means of employing nontrivial structure of equality of types given by iso and univalence: mutually inverse automorphisms isuc (which is (+1)) and ipred(which is (-1)) of Int define a loop on Int, which we can use!

\func code (x : Sphere1) : \Set0
  | base1 => Int
  | loop i => iso isuc ipred ipred_isuc isuc_ipred i

We can now define the map encode that maps a path p : base1 = x to the point in the fiber code x, which is the transport of 0 along p:

\func encode (x : Sphere1) (p : base1 = x) : code x => transport code p 0

Thus we have defined functions in both directions wind : Int -> base1 = base1 and encode base1 : base1 = base1 -> Int. It remains to prove that they are mutually inverse. The key idea is inspired by the classical proof: prove equivalence between universal cover and the path fibration \lam x : Sphere1 => base1 = x, which represents all the paths in Sphere1 with one endpoint fixed at base1. The equivalence of fibers over base1, that is of code base1 ==> Int and base1 = base1, would follow.

We have already defined the map encode from path fibration to universal cover. The inverse function decode (x : Sphere1) : code x -> base1 = x can be defined using the higher induction principle for the circle, which we described above. The full definition of decode as well as the proofs encode_decode, decode_encode that encode and decode are mutually inverse are technical, we omit them here. The rest of the proof can be found in the Arend standard library.

Eilenberg-Maclane space

Given a group G we now construct a pointed connected 1-type K1 G such that the fundamental group of K1 G is G. The type K1 G is called the Eilenberg-Maclane space. This type can be defined as the type with the base point base, for every g : G the loop constructor loop g i and for every g g’ : G the 2-cell relation g g’ i j, which equalizes the composition of loops path (loop g) *> path (loop g’) and the loop path (loop (g * g’)).

\data K1 (G : Group)
  | base
  | loop G (i : I) \elim i {
    | left => base
    | right => base
  }
  | relation (g g' : G) (i : I) (j : I) \elim i, j {
    | left, j => base
    | right, j => loop g' j
    | i, left => loop g i
    | i, right => loop (g * g') i
  }

\func K1-connected (G : Group) : isConnected (K1 G)
  => {?}
    
\func grp-to-ptconn (G : Group) : \Sigma (X : Pointed) (isConnected X) => (\new Pointed (K1 G) { | base => base}, K1-connected G)

Exercise 4: Prove that K1 G is connected.

Note that relation g g’ fills the square with path (loop g) (top), path (loop g’) (right), path (loop (g * g’)) (bottom) and idp (left). Therefore path (loop g) *> path (loop g’) = path (loop (g * g’)).

The homomorphism, analogous to wind : Int -> base1 = base1 for Sphere1, is simply \lam g => path (loop g) : G -> base = base.

The proof that (base = base) = G employs the same ideas as in the proof (base1 = base1) = Int for Sphere1. Namely, we need to define the universal cover code : K1 G -> \Type and mutually inverse functions encode (x : K1 G) : code x -> base = x and decode (x : K1 G) : base = x -> code x between the universal cover and the path fibration.

As in the case of Sphere1, the fiber of code over base is G and the transport along path (loop g) defines the homomorphism \lam g’ => g’ * g : G -> G. In order to ensure the latter we need to prove that the right multiplication is an equivalence. We can use the class QEquiv of quasi-equivalences to store the data: the inverse map * (inverse g) and the proofs that the maps * g and * (inverse g) are mutually inverse.

\func rightMulEquiv {G : Group} (g : G) : QEquiv (`* g) \cowith
  | ret => `* (inverse g) 
  | ret_f h => (*-assoc _ _ _) *> pmap (h *) (inverse-right g) *> ide-right h
  | f_sec h => (*-assoc _ _ _) *> pmap (h * ) (inverse-left g) *> ide-right h

We can now define code on base and loop g i:

\func code {G : Group} (x : K1 G) : \Type \lp \oo \elim x
  | base => G
  | loop g j => Equiv-to-= (rightMulEquiv g) @ j 
             -- 'Equiv-to-=' is essentially 'iso'.
  | relation g g' i j => {?}

It remains to define a filling of the square with sides Equiv-to-= (rightMulEquiv g) (top), Equiv-to-= (rightMulEquiv g’) (right), Equiv-to-= (rightMulEquiv (g * g’)) (bottom), idp (left). The function Cube2.map allows to construct such filling out of a proof that code preserves the relation path (loop g) *> path (loop g’) = path (loop (g * g’)).

-- Proof that 'code' preserves the relation on loops.
-- path (\lam i => code (loop g i)) *> path (\lam i => code (loop g' i)) = path (\lam i => code (loop (g * g') i))
\func equivPathComposition {G : Group} (g g' : G)
  : (Equiv-to-= (rightMulEquiv g)) *> (Equiv-to-= (rightMulEquiv g')) = (Equiv-to-= (rightMulEquiv (g * g')))
=> {?}

\func code {G : Group} (x : K1 G) : \Type \lp \oo \elim x
  | base => G
  | loop g j => Equiv-to-= (rightMulEquiv g) @ j 
  | relation g g' i j => Cube2.map (Equiv-to-= (rightMulEquiv g)) (Equiv-to-= (rightMulEquiv (g * g'))) idp (Equiv-to-= (rightMulEquiv g'))
                                   (movePath (equivPathComposition g g')) @ j @ i
  \where {
    \func movePath {A : \Type} {a a' a'' : A} {p : a = a'} {q : a' = a''} {r : a = a''} (h : p *> q = r) : p = r *> inv q
      => (inv (pmap (p *>) (*>_inv q)) *> inv (*>-assoc p q (inv q))) *> pmap (`*> inv q) h
  }

The rest of the proof, which includes definitions of encode and decode, is technical and essentially repeats the corresponding parts of the proof for the circle. It can be found in the Arend standard library.