Quest 1 - Loop Space of the Circle

Part 0 - Definition of the Loop Space

In this quest, we continue to formalise the problem statement.

The problem statement

The fundamental group of is .

Intuitively, the fundamental group of at base consists of loops based as base up to homotopy of paths. In homotopy type theory, we have a native description of loops based at base : it is the space base base.

In general the loop space of a space A at a point a is defined as follows :

loopSpace : (A : Type) (a : A)  Type
loopSpace A a = a  a

For now, we will treat the loop space of as the fundamental group. Later we will understand why this is illegal in general (the fundamental group is set truncated) but legitimate in this special case (the loop space of turns out to be a set anyway).

Exercise - loop_times

Clearly for each integer n : we have a path that is “loop around n times”. Locate loop_times in 1FundamentalGroup/Quest1.agda (note how agda treats underscores)

loop_times :   loopSpace  base
loop n times = {!!}


You can use underscores when you name a function. agda will put the inputs in the underscores in order.

Try casing on n, you should see

loop_times :   loopSpace  base
loop pos n times = {!!}
loop negsuc n times = {!!}

It says to map out of it suffices to map the non-negative integers (pos) and the negative integers (negsuc). The definition of in agda is

data  : Type where
  pos    :     negsuc :   

It says is is two copies of where the first copy represents 0, 1, 2, ..., and the second represents -1, -2, ... (negsuc n is meant to mean - (n + 1)). This definition of uses the naturals, so try casing on n again, you should see

loop_times :   Ω  base
loop pos zero times = {!!}
loop pos (suc n) times = {!!}
loop negsuc n times = {!!}

It says to map out of it suffices to map zero and map each successive integer suc n inductively. We can do the same with negsuc n, obtaining four cases.

loop_times :   Ω  base
loop pos zero times = {!!}
loop pos (suc n) times = {!!}
loop negsuc zero times = {!!}
loop negsuc (suc n) times = {!!}

These four cases represent :

  • If you “loop 0 times” then you stay at base.

  • If you “loop n + 1 times”, you “loop n times” then “loop once more”.

  • If you “loop -1 times”, you “loop once in reverse”

  • If you “loop -(n + 2) times”, you loop “loop -(n + 1) times” then “loop once more in reverse”


  • Try filling the first hole with what we get when we loop 0 (pos zero) times.

  • For looping pos (suc n) times we loop n times and loop once more. For this we need composition of paths.

    _∙_ : x  y  y  z  x  z

    Try typing _∙_ or ? ? in the hole (input \.) and refining. Checking the new holes you should see that now you need to give two loops.

    loop pos (suc n) times = {!!}  {!!}

    Try giving it “loop n times” concatenated with loop.

  • To “loop in reverse” we use

    sym : x  y  y  x

    Use this to define “loop -1 times”.

  • For the last case “concatenate loop -(n + 1) times with loop in reverse”.

Part 1 - Making a Path From to Itself

In the previous part we have defined the map loop_times : Ω base. Creating the inverse map is difficult without access to the entire circle. Similarly to how we used doubleCover to distinguish refl (Refl is now refl which is more general) from loop, the idea is to replace Bool with , allowing us to distinguish between all loops on . In this quest we will construct one of the two comparison maps across the whole circle, called windingNumber.

The plan is :

  1. Define a function sucℤ : that increases every integer by one

  2. Prove that sucℤ is an isomorphism by constructing an inverse map predℤ : .

  3. Turn the isomorphism sucℤ into a path sucℤPath : using isoToPath

  4. Define helix : Type by mapping base to and a generic point loop i to sucℤPath i.

  5. Use helix and endPt to define the map windingNumberBase : base base . Intuitively it counts how many times a path loops around . a generic point loop i to sucℤPath i.

  6. Generalize this across the circle.

In this part, we focus on 1, 2 and 3.

Defining sucℤ

  • Set up the definition of sucℤ so that it is of the form :

    Name : TypeOfSpace
    Name inputs = ?

    Just writing in the name and the type of the space is enough for now. Load the file and check that it is looks like:

    sucℤ :   ℤ
    sucℤ = ?

  • We will define sucℤ the same way we defined loop_times : by induction. Do cases on the input of sucℤ. You should have something like :

    sucℤ :   ℤ
    sucℤ pos n = ?
    sucℤ negsuc n = ?

  • For the non-negative integers pos n we want to map to its successor. Recall that the n here is a point of the naturals whose definition is :

    data  : Type where
      zero :   suc :   

    Use suc to map pos n to its successor.

  • The negative integers require a bit more care. Recall that annoyingly negsuc n means “- (n + 1)”. We want to map - (n + 1) to - n. Try doing this. Then realise “you run out of negative integers at -(0 + 1)” so you must do cases on n and treat the -(0 + 1) case separately.


    Do C-c C-c on n. Then map negsuc zero to pos zero. For negsuc (suc n), map it to negsuc n.

  • This completes the definition of sucℤ. Use C-c C-n to check it computes correctly. E.g. check that sucℤ (negsuc zero) computes to pos zero and sucℤ (pos zero) computes to pos (suc zero).

sucℤ is an Isomorphism

  • The goal is to define predℤ : which “takes n to its predecessor n - 1”. This will act as the (homotopical) inverse of sucℤ. Now that you have experience from defining sucℤ, try defining predℤ.

  • Imitating what we did with flipIso and give a point sucℤIso : by using predℤ as the inverse and proving section sucℤ predℤ and retract sucℤ predℤ.

sucℤ is a Path

  • Imitating what we did with flipPath, upgrade sucℤIso to sucℤPath.

Part 2 - Winding Number

The -bundle helix

We want to make a -bundle over by ‘copying ℤ across the loop via sucℤPath’. In Quest1.agda locate

helix :   Type
helix = {!!}

Try to imitate the definition of doubleCover to define the bundle helix. You should compare your definition to ours in Quest1Solutions.agda. Note that we have called this helix, since the picture of this -bundle looks like

Counting Loops

Now we can do what was originally difficult - constructing an inverse map (over all points). Now we want to be able to count how many times a path base base loops around , which we can do now using helix and finding end points of ‘lifted’ paths. For example the path loop should loop around once, counted by looking at the end point of ‘lifted’ loop, starting at 0. Hence try to define

windingNumberBase : base  base  helix base
windingNumberBase = {!!}

  • endPt evaluates the end point of ‘lifted paths’.

Try computing a few values using C-c C-n, you can try it on refl, loop, ‘loop three times’, ‘loop negative one times’ and so on.


The function windingNumberBase can actually be improved without any extra work to a function on all of .

windingNumber : (x : )  base  x  helix x
windingNumber = {!!}

Try filling this in. We will show that this and a general version of loop_times are inverses of each other over , in particular obtaining an isomorphism between base base and .