The HoTT Game
The Homotopy Type Theory (HoTT) Game is a project written by mathematicians for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying out mathematics in HoTT.
To get started with the HoTT Game, go to Getting Started.
This game was created by Joseph Hua, Ken Lee, and Bendit Chan.
Getting Started
The HoTT Game
The Homotopy Type Theory (HoTT) Game is a project written by mathematicians for mathematicians interested in HoTT and no experience in proof verification, with the aim of introducing cubical agda as a tool for trying out mathematics in HoTT. This page will help you get the Game working for you.
Agdapad
The HoTT Game can be played entirely in your browser using
Agdapad.
If you want a quick start to the game without installing anything,
you can go straight to the site, create your own agda
session, and start playing.
Specifically, once you open an agda
session, you should see a welcome page
(which contains useful information).
Around the top left of the screen there is a folder icon.
Click on the folder icon, and open the directory TheHoTTGame
.
This contains everything you need for the game.
Many thanks to Ingo Blechschmidt for incorporating the game into Agdapad
.
Installing Agda and the Cubical Agda library
A more longterm setup for using agda
would be to install it locally.
If you would like detailed instructions on how to install agda and a supportive text editor
then we recommend you follow instructions on Installation.
More general instructions follow:
Our Game is in agda
, which can be installed following instructions
on their site.
It is recommended that you use agda
in the text editor
emacs,
specifically we recommend
doom emacs,
but it can also work in
atom and
vscode.
Once you have emacs
and agda
, clone the
cubical library repository (version 0.3)
and make sure agda
knows where your copy of the cubical library is
by following instructions on the
library management page.
In short: locate (or create) your libraries
file and add a line
thedirectory/cubical.agdalib
to it, where thedirectory
is the location of cubical.agdalib
on your computer.
Get the HoTT Game by
cloning our repository
into a folder and then making sure that agda
knows where the HoTT Game is
by adding a line
thedirectory/TheHoTTGame.agdalib
to your libraries
file as above.
Try opening 1FundamentalGroup/Quest0.agda
in Emacs
and do Ctrlc Ctrll
.
Some text should be highlighted, and any {!!}
should turn into { }
.
Where to start?
You can start with trinitarianism if you are interested in
how logic, type theory and category theory come together
as different ways to view the same thing.
If you are more interested in homotopy theory,
try Fundamental Group of the Circle where we show that the
fundamental group of S¹
is ℤ
.
We recommend starting with Fundamental Group of the Circle for intuition,
then going to trinitarianism.
How to start?
To start with Fundamental Group of the Circle (for example),
go to Quest 0  Working with the Circle
and follow the instructions there.
Any agda
should happen in Agdapad
or your local copy of the repository.
Emacs issues
If you can’t figure out emacs
or forget some command, then
try consulting the Emacs Commands page.
Special thanks
We would like to thank Kevin Buzzard for introducing us to formalization,
making the Natural Numbers Game for learning lean
(which inspired this project), and helping the game gain publicity.
We would also like to thank all those involved in the HoTT community
and writing the HoTT book, especially Steve Awodey,
who helped us post about the Game on homotopytypetheory.org.
Lastly we thank all those who are trying out the game and giving us feedback.
If you would like to get involved, simply open and issue and let us know what
you would like to do.
Installation
Overview
To get things up and running you will need five things
agda
installed on your computer. This is what will check if your code makes sense. (Automatic if using theNix
installation)A text editor, for example
doom emacs
,atom
,vscode
, orvim
. This is an environment for you to edit files in.support for
agda2mode
oragdamode
in your text editor. This should do syntax highlighting for your code (pretty colours) and make sure the text editor has the right shortcuts.A clone of the cubical library. (Automatic if using the
Nix
installation.)A clone of the HoTT Game, which is our code.
There are many ways to install agda
.
On this page we will try to describe some ways to install it.
There are roughly three ways:
Using
Nix
. If you use windows this is probably the easiest and most rewarding method. It involves getting theNixOS
, a linux operating system inside your computer, so you also get to try out linux.Installing
agda
and the cubical library yourselfUsing VScode and getting the
agdaLanguageServer
Text editors
Important
No matter the text editor you choose, you will need emacs
installed somewhere on your computer,
as agdamode
relies on emacs
in the background.
Whilst we will assume you use doom emacs
in our guides (since it is the hardest to get used to),
there are other options :
atom
:Here is a set of instructions by Andrew Swan for getting
agda
working inatom
.vscode
: Here is a set of instructions for gettingagda
working invscode
(scroll down toinstallation
). You might be able to skip steps1
,2
and3
by enablingagdaMode.connection.agdaLanguageServer
in the settings. (We haven’t tried this  feedback is welcome.)vim
: Here is a set of instructions for gettingagda
working invim
. (We haven’t tried this  feedback is welcome).
Installing agda
Here we give instructions for installing agda
on each operating system.
If you have specific advice / issues specific to your operating system then please let us know in
issues.
Another source for information is
official installation guide,
but our advice might be more relevant to you.
Debian and Ubuntu
Ubuntu already should have a version of emacs
installed.
If not, go to a terminal and type in
sudo aptget install emacs
To get agda
, go to a terminal and type in
sudo apt install agdabin
Now you need to set up agdamode
(is this necessary if you can get agdamode
in emacs
?  feedback welcome) :
sudo apt install agdamode
followed by
agdamode setup
You can check the version of agda
by doing agda version
in the terminal.
MacOS
This will give you both agda
and agdamode
at once.
Open a terminal.
We will directly clone the
agda
repo for development version. First usecd
(“change directory”) in the terminal to navigate to where you want to place theagda
library. Then do the followinggit clone https://github.com/agda/agda.git
This gets a copy of the
agda
repo.Go into folder of agda repo then do
cabal update make install
This will compile
agda
to make it usable.Once process is finished, you can check
agda
is installed and its version by doing the following interminal
:agda version
This is all you need to get agda
and agdamode
, now you just need a text editor.
Windows
We used powershell as the terminal, but others probably work too.
Warning
Always use powershell as admin.
For the prerequisites
install chocolatey: follow instructions on their page
In (admin) powershell do (via chocolatey, cabal) 
choco install ghc
choco install cabal
cabal update
In order to makecabal
seeghc
, close and reopen the terminal before doing the next steps. You might want to also tryrefreshenv
for this. cabal install happy
cabal install alex
Now to install agda
, first try using cabal
by doing cabal install make
in the terminal. If this works then go with “using cabal”, if not
then try “using stack”
Using ``cabal``
You should have installed
make
withcabal install make
by this point, if not do so now.Directly clone the repo for development version. You can choose where to put this by navigating to some specific folder in the terminal and doing
git clone https://github.com/agda/agda.git
It should create a folder called
agda
(a copy of the github repo). You should docd agda
to go into that folder, then once you’re in there domake install
which installs
agda
usingmake
(it says “run the file calledMAKEFILE
from the folder”).Once installation is finished, try typing
agda version
in powershell to check the version.
Using ``stack``
Get stack using the installer here.
Run
stack upgrade
in the terminalDoing
cabal get Agda
in the terminal will create a folder calledAgda2.6.2
where you are at in the terminal. You can choose where to put this by navigating to some specific folder in the terminal usingcd FILENAME
.Once you have created this
Adgda2.6.2
, go into it by doingcd Agda2.6.2
.In the folder
Agda2.6.2
, there should be a file calledstack9.0.1.yaml
. Now you can try doingstack stackyaml stack9.0.1.yaml install
in the terminal (when you’re in the folderAgda2.6.2
) to run that file.Once installation is finished, try typing
agda version
to check the version.
In either case we should have agda
and agdamode
.
So we should just need to get a text editor.
Installing doom emacs
Here we give instructions for installing doom emacs
on each operating system.
If you have specific advice / issues specific to your operating system then please let us know in
issues.
Linux
We have experience difficulties with getting doom
on ubuntu
specifically,
so you might be better off using one of the other options,
in particular atom
appears to work well.
Try installing doom emacs
according to
the instructions on their github repository.
A quick guide follows:
Go to a terminal and type in
git clone depth 1 https://github.com/hlissner/doomemacs ~/.emacs.d
~/.emacs.d/bin/doom install
You’ll probably want to answer “yes” to the options unless you know better.
We recommend you add ~/.emacs.d/bin
to your PATH
so you can call doom directly and from anywhere;
accomplish this by going to the file ~/.bashrc
located in your home directory
(or ~/.zshrc
file if you use zsh as your shell)
and adding the line export PATH=$PATH:~/.emacs.d/bin
at the end.
This should give you doom emacs
.
You might need to restart your computer and or emacs
to make sure everything works correctly.
MacOS
Make sure you have the right version of git.
Do the following in a terminal to get doom emacs
.
# required dependencies
brew install git ripgrep
# optional dependencies but install them anyway
brew install coreutils fd
# Installs clang. This may take a long time.
xcodeselect install
# For fonts
brew install fontconfig
# Installs emacsmac wth sexy icon
brew tap railwaycat/emacsmacport
brew install emacsmac withmodules withemacssexyicon
# Make an app link in Applications
ln s /usr/local/opt/emacsmac/Emacs.app /Applications/Emacs.app
# doom emacs
git clone https://github.com/hlissner/doomemacs ~/.emacs.d
~/.emacs.d/bin/doom install
# so that you can use 'doom' anywhere
export PATH=”$HOME/.emacs.d/bin:$PATH”
This should give you doom emacs
.
You might need to restart your computer and or emacs
to make sure everything works correctly.
Windows
NixOS and WSL2
If you came from the NixOS and WSL2 instructions then go to the linux section.
There are detailed instructions for getting doom emacs
on windows
here.
The advice given there for installing fonts might not work.
If it doesn’t work, try installing a font (for example
Iosevka)
by following
these instructions.
Then go to .doom.d/config.el
and add the line (anywhere)
(setq doomfont (fontspec :family "Iosevka SS04" :size 18 :weight 'medium))
Here the font name is Iosevka SS04
. You can also change the font size and weight.
Operating system specific issues
If you have specific advice or issues specific to your operating system then please let us know in issues.
Getting agda2mode
or agdamode
support for your text editor
If you have decided to use doom emacs
then you can get agda2mode
inside doom emacs
(details below).
For other text editors, you must first install agdamode
,
and then find the relevant adon to the text editor to support agdamode
(details below).
Getting agda2mode
on doom emacs
Here we install agda2mode
in Doom Emacs
.
Note that this is not agda
itself, but syntax highlighting and shortcuts for agda
.
Do the shortcut
Mx
indoom emacs
. (See Emacs Commands for how to do shortcuts indoom emacs
.) A window should pop up where you can type things. Type in :packageinstall
Press enter and type in
agda2mode
.Now do the shortcut
SPC f p
. A selection of files should appear. Type ininit.el
and hit enter (RET
).Now you are in
init.el
. Look for thelang
section and uncommentagda
. Save the file and closedoom emacs
usingSPC q q
. (If you came from theNix
installation guide replaceagda
with(agda +local)
instead.)Open
terminal
. To make the configurations ofdoom emacs
up to date, dodoom sync
If there are no errors, you should have
agda2mode
indoom emacs
.
Getting agdamode
on atom
In
atom
select
Edit > Preferences (GNU/Linux)
Atom > Preferences (macOS)
File > Settings (Windows)
Select Install from the side menu.
Type agda into the search box.
Install the packages
agdamode
andlanguageagda
Check the agda
and agdamode
installations
Once you have installed agda
, a text editor,
and support for agdamode
in your text editor,
you should test it.
Make a test.agda
file anywhere you’d like.
Open
test.agda
indoom emacs
.Type in
open import Agda.Builtin.Nat
Use
Cc Cl
to load the file. An**Agda Information**
window should pop up and if all goes well, there should be nothing in it.Use
Cc Cd
then enterNat
. The output in the agda info window should beSet
.
Congratulations, you now have agda
and
can use emacs
bindings for agda
.
However, you have nothing more than the
builtin types.
So we need to get the library.
Getting the cubical library
The HoTT Game currently requires the cubical0.3
library.
We walk through an example of an installation of the cubical0.3
library.
See the
Agda documentation
for more about libraries.
Go here. Under ‘version 0.3’, download the ‘Source Code’ file in either formats
zip
ortar.gz
.Open the ‘Source Code’ file. It should turn into a folder which contains a folder called ‘cubical’. Choose a place for it to permanently stay, this can be anywhere you like.
Rename the folder ‘cubical’ to ‘cubical0.3’. Inside it, there should be a
cubical.agdalib
file with contentsname: cubical0.3 include: . depend: flags: cubical noimportsorts
This is the file that tells
agda
“this is a library” whenagda
looks into this folder. You can place the folder (now) calledcubical0.3
anywhere you like. For the sake of this guide, let’s say you put it in a place so that the path isLOCATION/cubical0.3
.
Now we need to tell agda
this cubical0.3
library exists,
so that it will look for it when an agda
file uses code from it.
Open a terminal and do
agda l fjdsk Dummy.agda
Assuming you don’t already have an
agda
library calledfjdsk
, you should see an error message of the formLibrary 'fjdsk' not found. Add the path to its .agdalib file to 'BLAHBLAHBLAH/libraries' to install. Installed libraries: none
The
BLAHBLAHBLAH/libraries
is where we tellagda
of the location of libraries.Examples in common operating systems :
On
linux
this might look something like :/home/USERNAME/.agda/libraries
where
USERNAME
is your username on your computer.On
MacOS
this might look something like :/Users/USERNAME/.agda/libraries
where
USERNAME
is your username on your computer.On
windows
this might look something like :C:\Users\USERNAME\AppData\Roaming\agda\libraries
where
USERNAME
is your username on your computer.
Navigate to
home/USERNAME
orUsers/USERNAME
orC:\Users\USERNAME\AppData\Roaming\agda
usingcd
.Do the following to see hidden files :
ls la
If there is no
.agda
(agda
for windows) folder, simply create one by doingmkdir .agda (or mkdir agda for windows)
If you do
ls la
again, you should see.agda
in the list.Go into that folder by doing
cd .agda
Check the contents of
.agda
by doingls la
. Create a filelibraries
if there isn’t one already. Inside it, putLOCATION/cubical0.3/cubical.agdalib
Save the file and close it.
Restart the terminal. Now do
agda l fjdsk Dummy.agda
in the terminal again. This time the error message should beLibrary 'fjdsk' not found. Add the path to its .agdalib file to 'BLAHBLAHBLAH/libraries' to install. Installed libraries: cubical0.3 (LOCATION/cubical0.3/cubical.agdalib)
Congratulations,
agda
is now aware of the existence of thecubical0.3
library.
Getting The HoTT Game
The HoTT Game is also an agda
library
so we need to repeat the above process for it.
In a terminal, navigate to where you would like to put the HoTT Game, as with the cubical library it can go anywhere. (You can use
cd
to navigate folders.)Use
git clone https://github.com/thehottgame/TheHoTTGame.git
. This should copy the HoTT Game repository as a folder calledTheHoTTGame
. For the purposes of this guide, let’s say you have put the HoTT Game in your computer at the pathLOCATION1/TheHoTTGame
Inside it, you should see many files, one of which should be
TheHoTTGame.agdalib
.Go back to
BLAHBLAHBLAH/libraries
and add the following lineLOCATION1/TheHoTTGame/TheHoTTGame.agdalib
In
terminal
, useagda l fjdsk Dummy.agda
again. The error message should now look something likeLibrary 'fjdsk' not found. Add the path to its .agdalib file to 'BLAHBLAHBLAH/libraries' to install. Installed libraries: cubical0.3 (LOCATION/cubical0.3/cubical0.3.agdalib) TheHoTTGame (LOCATION1/TheHoTTGame/TheHoTTGame.agdalib)
In Doom Emacs, open
TheHoTTGame/1FundamentalGroup/Quest0.agda
and doCc Cl
(Controlc Controll
). If all went correctly, the text should be highlighted and you should be ready to go. Congratulations, you can now play the HoTT Game.
Installing with Nix
Linux and MacOS
Nixpkgs
maintains a set of agda
libraries that can be added to a
derivation managed by the nix package manager,
see here
for details.
The file shell.nix
in our repository contains a derivation that will add emacs
, agda
, the agda standard library
,
and cubical agda
to your local nix store and subsequently to a local shell environment by adding these locations to your PATH
.
However, because user configurations for emacs
are mutable,
it will not (easily) manage your (emacs configuration) dotfiles,
so we will use the underlying emacs
provided by nixpkgs
but install doom emacs
normally in your local user’s environment.
Install
doom emacs
(or whichever text editor you prefer) via the method described for your operating system here. (If you are on Windows with NixOS on WSL2 then you are a linux user for the rest of the installation and should do everything in a termial inside NixOS.)Get
agda2mode
support todoom
(or whichever editor you prefer) via the method described above.Clone our repository into a folder by going to some directory using
cd
and doinggit clone https://github.com/thehottgame/TheHoTTGame.git
This can be done anywhere you like.
Install
Nix
(notNixOS
) using following the guidance on the official site. We install the singleuser version for linux (compare this with what is written on the official website):sh <(curl L https://nixos.org/nix/install) nodaemon
If you are on MacOS this will be different, and if you are on Windows using NixOS then this should also be exactly what you need.
Open a terminal, and use cd to navigate to the folder
TheHoTTGame
, which was cloned before. InTheHoTTGame
, donixshell
It might be that you need to restart your computer for this to work, and you might need to wait a little bit for it to start working, it might stay blank for a while. Later booting of nixshell should be faster than the first.
This should open up a
Nix
shell (inside your usual terminal), from which you can do all the usual things in a terminal and more. The above mentioned packages should automatically be loaded on yourPATH
. The above is all defined by the package set inshell.nix
in the folderTheHoTTGame
.Each time you wish to use
agda
(in particular its libraries), you should do step 5 to load the requisite packages onto thePATH
so that they can be found.If you got
doom
, go back to.doom.d/init.el
and make sure that instead of uncommenting;; agda
in the;; lang
, replace it with(agda +local)
to tell doom to use theagdamode
version specified by the local environment. Once the file is saved, syncdoom
from within thenixshell
that was loaded above:doom sync
You can now load the agda source code in this by starting doom from the nixshell:
doom run .
Open the file
0Trinitarianism/Quest0.agda
and tellagdamode
to load and check it by doingSPC m l
(space
,m
andl
, in that order.) If everything is configured correctly, you should get nice colors and any{!!}
will become interactive holes to fill.
Windows
First have a read of the previous section for Linux and MacOS for an overview, since once you get NixOS with WSL2, you will be using a Linux operating system anyway.
Get WSL2 following instructions here. You might also like to follow a video guide. Reboot your system.
By default WSL2 will get ubuntu, which is fine, but is not the operating system we will use. We want to get
NixOS
, which we can do by following instructions in the quick start section of this github page. Reboot your system.Reopen
NixOS
and follow the rest of the installation instructions as if you are a linux user.
Emacs Commands
Agdapad
Agdapad
uses emacs
but not doom emacs
,
so only the agda
shortcuts (below) are relevant.
Notation
SPC
means space barCx
meansCtrlx
Mx
meansAltx
for nonMacs andOptionx
for MacsSx
meansShiftx
RET
means enter
Example Cc Cl
in Agda files is Ctrlc
, let go, Ctrll
General Doom Emacs usage
The ‘ambient mode’ is called evil mode and follows vimlike bindings. The following commands are for evil mode:
SPC h b b
to look for bindings (keyboard shortcuts)SPC f f
to find files. can useTAB
for autocompleting paths andBackspace
to go up a directoryh j k l
for left down up rightSPC b k
to kill ‘buffers’ (any little window is a buffer). In generalSPC b
gives you many options for buffers.SPC w k
to kill unwanted windows (emacs can get split up into many windows) In generalSPC w
gives you many options for windows.i
to go into insert mode (in insert mode you can insert text) andESC
orCg
to go back to evil mode.C_
to undo (be careful with this, undo can go too far; going into and out of insert mode is considered “one change” in evil mode, so undoing might undo a lot of changes made in insert mode).r
to redo (be careful with this, redo can go too far).SPC h '
to look up how to write a symbol. (Put your cursor on the symbol first.)
Agda usage
Important
To insert text in the agda
file use i
to enter insert mode.
To escape insert mode do ESC
or Cg
.
All the commands below should be done whilst in insert mode.
Load :
Cc Cl
loads the fileCheck the goal :
Cc C,
checks goal of the hole your cursor is in.Fill the goal :
Cc CSPC
fills hole your cursor is in.Refine the goal :
Cc Cr
refines the hole your cursor is in.Case on
x
:Cc Cc
does cases onx
, wherex
is in the hole your cursor is in.Deduce :
Cc Cd
asks you to give it term / pointx
, it deduces the type / space thatx
belongs toNormalise :
Cc Cn
asks you to give it term / pointx
, it ‘reduces’x
to its ‘simplest (normalised) form’Combo :
Cc C.
doesCc C,
andCc Cd
Looking up definitions : in
agdapad
, clicking on something with the wheel of your mouse looks up the definitions of that thing (try clicking onType
for example). Indoom emacs
,MSPC c d
looks up the definition of the thing you are hovering over.
You can find more commands for agda
in emacs
here.
Unicode commands
In general follow the guidance given above to learn unicode commands. However here are some commonly used ones to get you started
insert
\to
for→
insert
\==
for≡
insert
\==n
for≢
insert
\bot
for⊥
insert
\neg
for¬
insert
\GS
forΣ
insert
\cong
for≅
insert
\^
for superscript, e.g.S\^1
forS¹
insert
\bN
forℕ
and\bZ
forℤ
insert
\.
for∙
insert
\sqcup
for⊔
You can find more common symbols here.
Getting Git on MacOS
On certain older verions of MacOS
one needs to get the right version of git
.
Check the version
Check if you have the right version of ``git` <gettingGit>`_.
Macs come with git
preinstalled.
You can open terminal
and type
git version
to see what version of git
you have.
It is most likely outdated if you’ve never used git
before.
Get the right version
To get the latest version visit this site .
To tell your computer to use the correct version of git
,
we need to do the following :
Open
terminal
and do the following to bring yourself to your home “directory”.cd
Do the following to show all files in this “directory”.
ls la
Amongst these we are interested in a file called
.zprofile
or.bash_profile
if your mac is older.Look at the top of your terminal window and you should see
zsh
orbash
if you’re on an older mac. This is the “shell” that your mac is using forterminal
. If it iszsh
,open .zprofile
This should open the file
.zprofile
withtext editor
. Now add the following to the end of the fileIf you terminal was using
bash
instead, doopen .bash_profile
This should open
.bash_profile
withtext editor
. Now add the the following to the end of the fileOnce you’ve done this, save the files and close them.
Restart
terminal
and do the following againYou should see the version has now updated.
Trinitarianism
Overview
This arc introduces the setting “a place to do maths”. The “types” that will populated this “place” will have three interpretations:
Proof theoretically, with types as propositions
Type theoretically, with types as programs
Category theoretically (geometrically), with types as objects (spaces) in a category (the space of spaces)
Terms and Types
Here are some things that we could like to have in a ‘place to do maths’
objects to reason about (E.g.
ℕ
)recipes for making things inside objects (E.g.
n + m
forn
andm
in naturals.)propositions to reason with (E.g.
n = 0
forn
in naturals.)a notion of equality
In proof theory, types are propositions and terms of a type are their proofs. In type theory, types are programs / constructions and terms are algorithms / recipes. In category theory, types are objects (spaces) and terms are generalised elements (points in the space).
Nondependent Types
false / empty / initial object
true / unit / terminal object
or / sum / coproduct
and / pairs / product
implication / functions / internal hom
Dependent Types
predicate / type family / bundle
substitution / substitution / pullback (of bundles)
existence / Σ type / total space of bundles
for all / Π type / space of sections of bundles
What is ‘the Same’?
The last missing piece is a notion of equality. How HoTT treats equality is where it deviates from its predecessors.
Quest 0  Terms and Types
There are three ways of looking at A : Type
.
proof theoretically, “
A
is a proposition”type theoretically, “
A
is a construction”geometrically / categorically, “
A
is a space andType
is the category of spaces”.
A first example of a type construction is the function type.
Given types A : Type
and B : Type
,
we have another type A → B : Type
which can be seen as
the proposition “
A
impliesB
”the construction ways to convert
A
recipes toB
recipes”the space of maps from
A
toB
, i.e. maps fromA
toB
correspond to points ofA → B
.internal hom of the category
Type
To give examples of this, lets make some types first.
Part 0  True / Unit / Terminal object
data ⊤ : Type where
tt : ⊤
It reads “⊤
is an inductive type with a constructor tt
”,
with interpretations
⊤
is a proposition “true” and there is a proof of it, calledtt
.⊤
is a construction “top” with a recipe calledtt
⊤
is the singleton space⊤
is a terminal object: every object has a morphism into⊤
given by· ↦ tt
In general, the expression a : A
is read “a
is a term of type A
”,
and has interpretations interpretations,
a
is a proof of the propositionA
a
is a recipe for the constructionA
a
is a point in the spaceA
a
is a generalised element of the objectA
in the categoryType
.
The above tells you how we make a term of type ⊤
.
Lets see an example of using a term of type ⊤
:
TrueToTrue : ⊤ → ⊤
TrueToTrue = {!!}
enter
Cc Cl
(this meansCtrlc Ctrll
). Whenever you do this,agda
will check the document is written correctly. This will open the*Agda Information*
window looking like?0 : ⊤ → ⊤ ?1 : ⊤ ?2 : ⊤
This says you have three unfilled holes.
Now you can fill the first hole.
Navigate to the hole
{ }
usingCc Cf
(forward) orCc Cb
(backward)Enter
Cc Cr
. Ther
stands for refine. Whenever you do this whilst having your cursor in a hole,agda
will try to help you.You should see
λ x → { }
. This isagda
notation forx ↦ { }
and is calledλ
abstraction, think “λ
for let”.Navigate to the new hole
Enter
Cc C,
(this meansCtrlc Ctrlcomma
). Whenever you make this command whilst having your cursor in a hole,agda
will check the goal.The goal (
*Agda information*
window) should look likeGoal: ⊤ ————————————————————————— x : ⊤
you have a proof/recipe/generalized element
x : ⊤
and you need to give a proof/recipe/generalized element of⊤
Write the proof/recipe/generalized element
x
of⊤
in the holePress
Cc CSPC
to fill the hole withx
. In general when you have some term (and your cursor) in a hole, doingCc CSPC
will tellagda
to replace the hole with that term.agda
will give you an error if it cant make sense of your term.The
*Agda Information*
window should now only have two unfilled holes left, this meansagda
has accepted your proof.?1 : ⊤ ?2 : ⊤
There is more than one proof (see Quest0Solutions.agda
).
Here is an important one:
TrueToTrue' : ⊤ → ⊤
TrueToTrue' x = { }
Naviagate to the hole and check the goal.
Note
x
is already taken out for you.You can try type
x
in the hole andCc Cc
c
stands for cases”. DoingCc Cc
withx
in the hole tellsagda
to do cases onx
”. The only case istt
.
One proof says for any term x : ⊤
give x
again.
The other says it suffices to do the case of tt
,
for which we just give tt
.
The same”
Are these proofs “the same”? What is “the same”?
(This question is deep and should be unsettling. The short answer is that they are internally but not externally the same.)
Built into the definition of ⊤
is the way agda
can make a map out of ⊤
into another type A
, which we have just used.
It says to map out of ⊤
it suffices to do the case when x
is tt
”, or
the only proof of
⊤
istt
the only recipe for
⊤
istt
the only point in
⊤
istt
the only one generalized element
tt
in⊤
Lets define another type.
Part 1  False / Empty / Initial object
data ⊥ : Type where
This reads “⊥
is an inductive type with no constructors”,
with interepretations
⊥
is a proposition “false” with no proofs⊥
is a construction “bot” with no recipes⊥
is the empty spaceThere are no generalized elements of
⊥
(it is a strict initial object)
We can make a map from ⊥
to any other type, in particular into ⊤
.
explosion : ⊥ → ⊤
explosion x = {!!}
Navigate to the hole and do cases on
x
.
agda
knows that there are no cases so there is nothing to do!
(See Quest0Solutions.agda
)
Our interpretations:
“false” implies “true”. In fact the same proof gives “false” implies anything (principle of explosion)
One can convert recipes of
⊥
to recipes of⊤
. In fact the same construction gives a recipe of any other construction since there are no recipes of⊥
.There is a map from the empty space to the singleton space. In fact given any space
A
, there is a map from the empty space toA
.⊥
is has a map into⊤
. This is due to⊥
being initial in the categoryType
.
Part 2  The natural numbers
We can also encode “natural numbers” as a type.
data ℕ : Type where
zero : ℕ
suc : ℕ → ℕ
Our interpretations are:
ℕ
has no interpretation as a proposition since there are “too many proofs”  mathematicians classically don’t distinguish between proofs of a single proposition. (ZFC doesnt even mention logic internally, but type theory does.) In this sense constructions are proof relevant types.As a construction :
ℕ
is a type of constructionzero
is a recipe forℕ
suc
takes an existing recipe forℕ
and gives another recipe forℕ
.
Categorically :
ℕ
is a natural numbers object in the categoryType
. This means it is equipped with morphismszero : ⊤ → ℕ
andsuc : ℕ → ℕ
such that given any⊤ → A → A
there exist a unique morphismℕ → A
such that the diagram commutes:
Geometrically :
ℕ
is a space with a pointzero
and for every pointn
inℕ
, there is another pointsuc n
inℕ
.
To see how to use terms of type ℕ
, i.e. to induct on ℕ
,
go to Quest 1  Dependent Types.
Part 3  Universes
You may have noticed the notational similarities between
zero : ℕ
and ℕ : Type
.
The type Type
has the following interpretations :
As a construction : any type of construction is a recipe for
Type
.Geometrically :
Type
is a space of spaces. Each individual point inType
is a space.
This may have lead you to the question, Type : ?
.
In type theory, we simply assert Type : Type₁
.
But then we are chasing our tail, asking Type₁ : Type₂
.
Type theorists make sure that every type
(i.e. anything the right side of :
)
itself is a term (i.e. anything on the left of :
),
and every term has a type.
So what we really need is
Type : Type₁, Type₁ : Type₂, Type₂ : Type₃, ⋯
These are called universes. The numberings of universes are called levels. It will be crucial that types can be treated as terms. This will allows us to
talk about predicates i.e. “propositions depending on a variable”. E.g. the proposition “
n
is even” depends on a natural numbern
. See the next quest where we elaborate on this example.reason about “structures” such as “the structure of a group”, to express “for all groups, …”
do category theory without stepping out of the theory. (For experts, we have Grothendieck universes.)
reason about when two types are “the same”, for example when are two definitions of the natural numbers “the same”? What is “the same”?
Quest 1  Dependent Types
In a “place to do maths” we would like to be able to express and “prove” the statement
The statement
There exists a natural that is even.
The goal of this quest is to define what it means for a natural to be even.
Part 0  Predicates / Dependent Constructions / Bundles
This requires the notion of a predicate.
In general a predicate on a type A : Type
is
a term of type A → Type
.
For example,
isEven : ℕ → Type
isEven n = ?
Do
Cc Cl
to load the file.Navigate to the hole.
Input
n
in the hole and doCc Cc
. You should now seeisEven : ℕ → Type isEven zero = {!!} isEven (suc n) = {!!}
It says “to define a function on
ℕ
, it suffices to define the function on the cases,zero
andsuc n
, since these are the only constructors given in the definition ofℕ
”. This has the following interpretations :propositionally, this is the principle of mathematical induction.
categorically, this is the universal property of a natural numbers object.
Navigate to the first hole and check the goal. You should see
Goal: Type ———————————
Fill the hole with
⊤
, since we wantzero
to be even.Navigate to the second hole.
Input
n
and doCc Cc
again. You should now seeisEven : ℕ → Type isEven zero = ⊤ isEven (suc zero) = {!!} isEven (suc (suc n)) = {!!}
We have just used induction again.
Navigate to the first hole and check the goal.
agda
should be asking for a term of typeType
, so fill the hole with⊥
, since we don”t wantsuc zero
to be even.Navigate to the next hole and check the goal. You should see in the
*Agda information*
window,Goal: Type —————————————— n : ℕ
We are in the “inductive step”, so we have access to the previous natural number.
Fill the hole with
isEven n
, since we wantsuc (suc n)
to be even precisely whenn
is even. The reason we have access to the termisEven n
is again because we are in the “inductive step”.There should now be nothing in the
*Agda information*
window. This means everything is working. (Compare yourisEven
with our solutions inQuest2Solutions.agda
.)
Part 1  Interpretations of Bundles
The interpretations of isEven : ℕ → Type
are
Propositionally : Already mentioned,
isEven
is a predicate onℕ
.As a construction :
isEven
is a dependent construction. Specifically,isEven n
is either⊤
or⊥
depending onn : ℕ
.Geometrically : seen as a map from the space
ℕ
to the space of spacesType
,isEven
assigns for every pointn
inℕ
a spaceisEven n
. Pictorially, it looks likeWe say
isEven
is a bundle of spaces overℕ
, or simply a bundle overℕ
for short. The spaceisEven n
lying above eachn
is called the fiber overn
. In this particular example the fibers are either empty or singleton.Note
In the above picture, we have implicitly drawn
ℕ
as a bunch of “disconnected” points, i.e. a discrete space. See a later arc where this is justified.Categorically :
isEven
is an object in the overcategoryType↓ℕ
.
In general given a type A : Type
,
a dependent type F
over A
is a term F : A → Type
.
This should be drawn as a collection of space parameterised
by the space A
.
You can check if 2
is even by asking agda
to “reduce” the term isEven 2
(do Cc Cn
, “n” for normalize) and type in isEven 2
.
(You can write in numerals since we are now secretly
using ℕ
from the cubical agda
library.)
Part 2  Using the Trinitarianism
We introduced new ideas through each perspectives, as each has their own advantage
Types as propositions is often the most familiar perspective, and hence can offer guidance for the other two perspectives. However the current mathematical paradigm uses “proof irrelevance” (two proofs of the same proposition are always “the same”), which is not compatible with HoTT. We will expand on this later.
Types as constructions conveys the way in which “data” is important, and should be preserved.
Types as objects/spaces allows us to draw pictures, thus guiding us through the syntax with geometric intuition.
For each new idea introduced, make sure to justify it proof theoretically, type theoretically and categorically/geometrically.
Quest 2  Sigma Types
We are still trying to express and “prove” the statement
The statement
There exists a natural that is even.
We will achieve this by the end of this quest.
Part 0  Existence / Dependent Pair / Total Space of Bundles
Recall from Quest 1  Dependent Types
that we defined isEven
.
What’s left is to be able write down “existence”.
In maths we might write
∃ x ∈ ℕ, isEven x
which in agda
notation is
Σ ℕ isEven
This is called a sigma type, which has three interpretations:
the proposition “there exists an even natural”
the construction “keep a recipe
n
of naturals together with a recipe ofisEven n
”the total space of the bundle
isEven
overℕ
, which is the space obtained by putting together all the fibers. Pictorially, it looks likewhich can also be viewed as the subset of even naturals, since the fibers are either empty or singleton. (It is a subsingleton bundle).
Part 1  Making terms in Sigma Types
Making a term of this type has three interpretations:
(giving a proof that there existence of an even natural amounts to giving) a natural
n : ℕ
and a proofhn : isEven n
thatn
is even.pairing a recipe
n : ℕ
with a recipehn : isEven n
.(giving a point in the total space is giving) a point
n : ℕ
downstairs together with a pointhn : isEven n
in its fiber.
Now you can prove that there exists an even natural:
Formulate the statement you need. Make sure you have it of the form
Name : Statement Name = {!!}
Load the file, go to the hole and refine the goal.
If you formulated the statement right it should split into
{!!} , {!!}
and you can check the types of terms the holes require.Fill the holes. There are many proofs you can do!
In general when A : Type
is a type and B : A → Type
is a
predicate/dependent construction/bundle over A
,
we can write the sigma type Σ A B
whose terms are pairs a , b
where a : A
and b : B a
.
In the special case when B
is not dependent on a : A
,
i.e. it looks like λ a → C
for some C : Type
then
Σ A B
is just
the proposition “
A
andC
” since giving a proof of this is the same as giving a proof ofA
and a proof ofC
a recipe
a : A
together with a recipec : C
B
is now a trivial bundle since the fibersB a
are constant with respect toa : A
. In other words it is just a productΣ A B ≅ A × C
. For this reason, some refer to the sigma type as the dependent product, but we will avoid this terminology.
_×_ : Type → Type → Type
A × C = Σ A (λ a → C)
agda
supports the notation _×_
(without spaces)
which means from now on you can write A × C
(with spaces).
Part 2  Using Terms in Sigma Types
There are two ways of using a term in a sigma type.
We can extract the first part using fst
or the second part using snd
.
Given x : Σ A B
there are three interpretations of fst
and snd
:
Viewing
x
as a proof of existencefst x
provides the witness of existence andsnd
provides the proof that the witnessfst x
has the desired propertyViewing
x
as a recipefst
extracts the first component andsnd
extracts the second componentViewing
x
as a point in the total space of a bundlefst x
is the point thatx
is over in the base space andsnd x
is the point in the fiber thatx
represents. In particular you can interpretfst
as projection from the total space to the base space, collapsing fibers.
For example to define a map that takes an even natural and divides it by two we can do
div2 : Σ ℕ isEven → ℕ
div2 x = {!!}
Load the file, go to the hole and case on
x
. You might want to renamefst₁
andsnd₁
.div2 : Σ ℕ isEven → ℕ div2 (fst₁ , snd₁) = {!!}
Case on
fst₁
and tellagda
what to give for0 , *
, i.e. what “zero divided by two” ought to be.div2 : Σ ℕ isEven → ℕ div2 (zero , snd₁) = {!!} div2 (suc fst₁ , snd₁) = {!!}
Navigate to the second hole and case on
fst₁
again. Notice thatagda
knows there is no term looking like1 , *
so it has skipped that case for us.div2 : Σ ℕ isEven → ℕ div2 (zero , snd₁) = 0 div2 (suc (suc fst₁) , snd₁) = {!!}
(n + 2) / 2
should just ben/2 + 1
so try writing insuc
and refining the goalHow do you write down
n/2
? Hint: we are in the “inductive step”.Try dividing some terms by
2
:Use
Cc Cn
and writediv2 (2 , tt)
for example.Try dividing
36
by2
.
Important observation :
the two proofs 2 , tt
and 36 , tt
of the statement
“there exists an even natural” are not “the same” in any sense,
since if they were div2 (2 , tt)
would be “the same” div2 (36/2 , tt)
,
and hence 1
would be “the same” as 18
.
“The same”
Are they “the same”? What is “the same”?
Quest 2  Side Quests
A Tautology / Currying / Cartesian Closed
In this side quest, you will construct the following functions.
uncurry : (A → B → C) → (A × B → C)
uncurry f x = {!!}
curry : (A × B → C) → (A → B → C)
curry f a b = {!!}
These have interpretations :
uncurry
is a proof that “ifA
implies (B
impliesC
)”, then “(A
andB
) impliesC
”. A proof of the converse iscurry
.this is a commonly occuring example of an adjunction. See here for a more detailed explanation.
Note that we have postulated the types A, B, C
for you.
private
postulate
A B C : Type
In general, you can use this to
introduce new constants to your agda
file.
The private
ensures A, B, C
can only be used
within this agda
file.
Tip
agda
is spaceandindentation sensitive,
i.e. the private
applies to anything beneath it
that is indented two spaces.
Quest 3  Pi Types
We will try to formulate and prove the statement
Problem statement
The sum of two even naturals is even.
Part 0  Defining Addition
To do so we must define +
on the naturals.
Addition takes in two naturals and spits out a natural,
so it should have type ℕ → ℕ → ℕ
.
_+_ : ℕ → ℕ → ℕ
n + m = ?
Try coming up with a sensible definition. It may not look the same as ours.
Hint
n + 0
should be n
and n + (m + 1)
should be (n + m) + 1
.
Part 1  The Statement
Now we can make the statement that a sum of even naturals is even in agda
.
Make sure it is of the form
Name : Statement
Name = ?
The statement should be of the form (x y : A) → B
where A
represents the subset of even naturals
and B
expresses what it means for the “sum of x
and y
” to be even.
Hint
Given x y : Σ ℕ isEven
we want to show that their sum
(really the sum of their fist components) is even,
so we should give isEven (x .fst + y .fst)
Tip
x .fst
is another notation for fst x
.
This works for all sigma types.
There are three ways to interpret this:
Spoiler
For all even naturals
x
andy
, their sum is even.isEven (x .fst + y .fst)
is a construction depending on two recipesx
andy
. Given two recipesx
andy
ofΣ ℕ isEven
, we break them down into their first components, apply the conversion_+_
, and form a recipe forisEven
of the result.isEven (_ .fst + _ .fst)
is a bundle over the categorical productΣ ℕ isEven × Σ ℕ isEven
andSumOfEven
is a section of the bundle. This means for every point(x , y)
inΣ ℕ isEven × Σ ℕ isEven
, it gives a point in the fiberisEven (x .fst + y .fst)
.
More generally given A : Type
and B : A → Type
we can form the pi type (x : A) → B x : Type
(in other languages Π (x : ℕ), isEven n
),
with interpretations :
it is the proposition “for all
x : A
, we haveB x
”, and each term of the pi type is a collection of proofs ``bx : B x`, one for eachx : A
.recipes of
(x : A) → B x
are made by converting eachx : A
to some recipe ofB x
. Indeed the function typeA → B
is the special case where the typeB x
is not dependent onx
. Hence pi types are also known as dependent function types. Note that terms in the sigma type are pairs(a , b)
whilst terms in the dependent function type are a collection of pairs(a , b)
indexed bya : A
Given the bundle
B : A → Type
, we have the total spaceΣ A B
which is equipped with a projectionfst : Σ A B → A
. A term of(x : A) → B x
is a section of this projection.
We are now in a position to prove the statement. Have fun!
Part 2  Remarks
Important
Once you have proven the statement,
check out our two ways of defining addition _+_
and _+'_
(in the solutions).
Use
Cc Cn
to check that they compute the same values on different examples.Uncomment the code for
Sum'OfEven
in the solutions. It is justSumOfEven
but with each+
changed to+'
.Load the file. Does the proof still work?
Our proof SumOfEven
relied on
the explicit definition of _+_
,
which means if we wanted to use our proof on
someone else’s definition of addition,
it might not work anymore.
Important Question
But _+_
and _+'_
compute the same values.
Are _+_
and _+'_
“the same”? What is “the same”?
Quest 3  Side Quests
Decidability of isEven
Try to express and prove in agda
the statement
Problem statement
Every natural number is even or not even.
We make a summary of what is needed:
a definition of the type
A ⊕ B
(input\oplus
), which has interpretationsthe proposition “
A
orB
”the construction with two ways of making recipes
left : A → A ⊕ B
andright : B → A ⊕ B
.the disjoint sum of two spaces
the coproduct of two objects
A
andB
. The type needs to take in parametersA : Type
andB : Type
data _⊕_ (A : Type) (B : Type) : Type where ???
a definition of negation. One can motivate it by the following
Define
A ↔ B : Type
for two typesA : Type
andB : Type
.Show that for any
A : Type
we have(A ↔ ⊥) ↔ (A → ⊥)
Define
¬ : Type → Type
to beλ A → (A → ⊥)
.
a formulation and proof of the statement above
Quest 4  Paths and Equality
If you have come here from Fundamental Group of the Circle then have a look at the overview to understand the philosophy of trinitarianism.
So far in trinitarianism there has been no mention of “equality”; we have never said what it meant for two types or two terms to be “the same”. However, in Fundamental Group of the Circle we have expressed what it means for two spaces to look the same, by creating a path from one space to the next (usually by an isomorphism). Indeed we will take this to be our definition of (internal) equality.
We will often adopt the geometric perspective, but change perspectives when appropriate.
Universe levels
In the solutions we always use Type u
,
but just write Type
here.
There is no conceptual difference with using
an arbitrary universe,
but in practice we want to be as general as possible.
It is useful to stick to just using Type
,
and realise why it is not general enough when problems arise.
Part 0  The Identity Type
The construction
Given A : Type
and x y : A
we have a type
Id x y : Type
, called the identity type of x
to y
.
data Id {A : Type} : (x y : A) → Type where
rfl : {x : A} → Id x x
The construction takes in (implicit) argument A : Type
,
then for each pair of points x y : A
it returns a space Id x y
with interpretations :
Id x y
is the proposition “x
equalsy
(internally)” and for everyx
, we have a proofrfl x
that “x
is equal to itself (internally)”. (Hence the namerfl
, which is short for reflexivity.)The only recipe for the construction
Id x y
is given whenx
is the same recipe asy
.Id x y
is the space of paths fromx
toy
, i.e. points in the space are paths fromx
toy
inA
. For every pointx
inA
, there is the constant pathrfl x
atx
.Id
is a bundle overA × A
and the diagonal mapA → A × A
, takingx ↦ (x , x)
, factors throughId → A × A
(viewingId
as the total spaceΣ (A × A) Id
).
Write this up in 0Trinitarinism/Quest4.agda
.
We recommend you first try having
the explicit argument for rfl
in rfl : (x : A) → Id x x
,
so you can see exactly what is going on,
but we will use rfl
with an implicit argument
rfl : {x : A} → Id x x
.
Internal versus external equality
In the first perspective use the word “internal”
since there is also the notion of “external equality”
that we want to distinguish.
In short x
and y
are externally equal if
the computer believes they are the same term,
i.e. the string of symbols they simplify (normalise) to are
exactly the same.
If two terms are externally equal then they are internally equal,
and the proof that they are internall equal is rfl
.
However, having a proof p : Id x y
is not enough for
the computer to recognise x
as the same term as y
.
Exercise  Symmetry
For Id
to be a good notion of equality it should at least be
an equivalence relation.
It is reflexive by having rfl
in the definition.
We show that it is symmetric:
idSym : (A : Type) (x y : A) → Id x y → Id y x
idSym = {!!}
This has interpretations:
Equality is symmetric
We can turn recipes for the construction
Id x y
into recipes for the constructionId y x
Paths can be reversed
Add this to the file 0Trinitarianism/Quest4.agda
and try showing it.
We give a detailed explanation in the hints and solution.
Hint 0
Assume we have a space A
, points x y : A
and
a proof of equality / recipe / path p : Id x y
.
It may help to view Id x y
as a construction
to think about how to proceed.
Hint 1
If you case on p : Id x y
then you should see the following
idSym : (A : Type) (x y : A) → Id x y → Id y x
idSym A x .x rfl = {!!}
We interpret this as
If
x
andy
are equal by proofp
and we want to show something aboutx
y
andp
, then it suffices to consider the case when they are externally equal; thaty
is literally the termx
andp
isrfl
.The only recipe we had for the construction
Id x y
isrfl
, so we should be able to reduce to this case.To map out of
Id
, viewed as a total space, it suffices to map out of the diagonal.
Solution
Since we have reduced to the case for when both points are x
,
we can simply supply a point in Id x x
.
There is an obvious one.
idSym : (A : Type) (x y : A) → Id x y → Id y x
idSym A x .x rfl = rfl
The Geometric Perspective
We have not included a justification via the geometric perspective. This is because intuitively it’s not quite obvious that to map out of the space of paths it suffices to map the constant path. We justify the mapping out property geometrically in a side quest.
We can also make the relevant arguments implicit. We will be using the following version from now on :
Sym : {A : Type} {x y : A} → Id x y → Id y x
Exercise  Transitivity
In 0Trinitarianism/Quest4.agda
, try to formalize (and then prove)
the following interpretations of the same statement :
Id
is transitive, which says ifId x y
andId y z
both hold, then so doesId x z
.recipes for
Id x y
andId y z
can be made into recipes forId x z
.paths can be concatenated
The statement
idTrans : (A : Type) (x y z : A) → Id x y → Id y z → Id x z
idTrans = {!!}
You may wish to make some of the arguments implicit. We could also introduce notation that suggests concatenation:
_*_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
_*_ = {!!}
We will use _*_
.
Hints
There are multiple ways of defining this.
Assuming p : Id x y
and q : Id y z
we could
case on
p
and identifyx
andy
case on
q
and identifyy
andz
case on both
p
andq
, identifying all three
Solutions
_*_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
rfl * q = q
_*0_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
p *0 rfl = p
_*1_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
rfl *1 rfl = rfl
These three definitions will work slightly differently in practice. We will use the first of the three, but you can use whichever you prefer.
Exercise  Groupoid Laws
The identity type satisfies some futher properties,
which you can formalize then prove.
You may notice that they look almost like the axioms of a group,
except a bit bigger  for example there is not just a single identity
element (refl
works at each point in the space).
Note that our solutions may differ to yours depending on your choice of how to define transitivity / concatenation.
concatenating
rfl
on the left and right does nothing,The statements
rfl* : {x y : A} (p : Id x y) → Id (rfl * p) p rfl* = {!!} *rfl : {x y : A} (p : Id x y) → Id (p * rfl) p *rfl = {!!}
The first says if you concatenate
rfl
on the left then it is equal to the original path.Solutions
rfl* : {x y : A} (p : Id x y) → Id (rfl * p) p rfl* p = rfl *rfl : {x y : A} (p : Id x y) → Id (p * rfl) p *rfl rfl = rfl
Note that we needed to case on the path in the second proof due to our definition of concatenation.
Tip
If you are tired of writing
{A : Type} {x y : A}
each time you can stickprivate variable A : Type x y : A
at the beginning of your
agda
file, and it will assumeA
,x
andy
implicitely whenever they are mentioned. Make sure it is indented correctly. Beware that anything declared like this will be an implicit argument.We also recommend reading about the module system in
agda
.concatenating a path
p
withSym p
on the left and right givesrfl
.The statements
Sym* : {A : Type} {x y : A} (p : Id x y) → Id (Sym p * p) rfl Sym* = {!!} *Sym : {A : Type} {x y : A} (p : Id x y) → Id (p * Sym p) rfl *Sym = {!!}
Solutions
Sym* : {A : Type} {x y : A} (p : Id x y) → Id (Sym p * p) rfl Sym* rfl = rfl *Sym : {A : Type} {x y : A} (p : Id x y) → Id (p * Sym p) rfl *Sym rfl = rfl
Concatenation is associative
The statement
Assoc : {A : Type} {w x y z : A} (p : Id w x) (q : Id x y) (r : Id y z) → Id ((p * q) * r) (p * (q * r)) Assoc = {!!}
Solution
Assoc : {A : Type} {w x y z : A} (p : Id w x) (q : Id x y) (r : Id y z) → Id ((p * q) * r) (p * (q * r)) Assoc rfl q r = rfl
These axioms say that any type is a groupoid, with the above structure. This aligns well with the geometric perspective of types : in classical homotopy theory any space has a groupoid structure and any groupoid can be made into a space.
Recursor  The Mapping Out Property of Id
We may wish to extract the way we have made maps out of the identity type :
Mapping out property of Id
Assuming a space A
and a point x : A
.
Given a bundle M : (y : A) (p : Id x y) → Type
over the “space of paths out of x
”,
in order to make a map {y : A} (p : Id x y) → M y p
,
it suffices to give a point in M x refl
.
This is traditionally called the “recursor” of Id
.
(We have still not justified this geometrically.)
For example, in order to prove *Sym : {A : Type} {x y : A} (p : Id x y) → Id (p * Sym p) rfl
,
we would choose our bundle M
to be λ y p → Id (p * Sym p) rfl
,
taking each y : A
and p : Id x y
to the space of paths from (p * Sym p)
to rfl
in Id x x
.
When we proved this in the previous section,
agda
figured out what M
needed to be and just asked for a proof of the case
M x rfl
.
In 0Trinitarianism/Quest4.agda
, try formalising the mapping out property,
and call it outOfId
.
The statement
outOfId : (M : (y : A) → Id x y → Type) → M x rfl
→ {y : A} (p : Id x y) → M y p
outOfId = {!!}
Note that we have used the symbol y
in the type of M
,
but it really is just a local variable and will not appear outside that bracket.
We made the last y
an implicit argument, since p
contains the data of y
.
Solution
outOfId : (M : (y : A) → Id x y → Type) → M x rfl
→ {y : A} (p : Id x y) → M y p
outOfId M h rfl = h
The proof is of course just casing on the path p
,
as we are trying to extract that idea.
Part 1  The Path Space
If you came here from the quest on Fundamental Group of the Circle
then you may be wondering why there has not been any mention of
the path space x ≡ y
.
The reason is that whilst ≡
and Id
are meant to represent the same idea,
the implementation of Id
is simple  we were able to write it down;
whereas the implementation of ≡
is “external”,
and purely existing in cubical agda
.
In this part we will show that the two are “the same” as spaces i.e. isomorphic,
and after this we will only use ≡
for equality and paths
(as is the convention in the cubical library).
We assert the following three axioms for the path space (we will add another (univalence) in later):
If
x
is a point in some space thenrefl
is a proof ofx ≡ x
.The mapping out property, called
J
:J : (M : (y : A) → x ≡ y → Type) → M x refl → {y : A} (p : x ≡ y) → M y p
This looks exactly like
outOfId
.The mapping out property applied to
refl
:JRefl : (M : (y : A) → x ≡ y → Type) (h : M x refl) → J M h refl ≡ h
This says that when we feed
refl
toJ M h
it indeed gives us what we expect  something equal toh
. Unfortunately, though (given correctM
andh
)outOfId M h rfl
would externally be equal toh
,J M h refl
is not externally equal toh
, but this is acubical agda
issue and not a HoTT issue.
Paths versus Id
The goal
Given two points x y : A
,
the path type x ≡ y
is isomorphic to Id x y
.
We introduce isomorphism in
Quest 0 of the Fundamental Group arc.
So we are trying to show
Path≅Id : (x ≡ y) ≅ (Id x y)
Path≅Id = {!!}
This involves a lot of small steps, which we split up into hints.
Hint 0
“Refining” in the hole will make it ask for the four components in the proof of an isomorphism.
Path≡Id : (x ≡ y) ≅ (Id x y)
Path≡Id = iso {!!} {!!} {!!} {!!}
Hint 1
To make an isomorphism we need to make maps forwards and backwards, these go in the first two holes.
Path→Id : x ≡ y → Id x y
Path→Id = {!!}
Id→Path : Id x y → x ≡ y
Id→Path = {!!}
Hint 2
To make the map forwards we will need to use J
 the mapping
out property of the path space.
To map backwards we can use outOfId
or just case on a path.
Path→Id : x ≡ y → Id x y
Path→Id {A} {x} = J {!!} {!!}
Id→Path : Id x y → x ≡ y
Id→Path rfl = {!!}
For the first, in order to state the motive we need the implicit arguments
A
and x
.
Solution
Path→Id : x ≡ y → Id x y
Path→Id {A} {x} = J (λ y p → Id x y) rfl
Id→Path : Id x y → x ≡ y
Id→Path rfl = refl
Hint 3
Filling in what we have so far and extracting the relevant lemmas we have
Path≅Id : (x ≡ y) ≅ (Id x y)
Path≅Id {A} {x} {y} = iso Path→Id Id→Path rightInv leftInv where
rightInv : section (Path→Id {A} {x} {y}) Id→Path
rightInv = {!!}
leftInv : retract (Path→Id {A} {x} {y}) Id→Path
leftInv = {!!}
We have filled in the necessary implicit arguments for you.
Hint 4
Since section Path→Id Id→Path
will first take in p : Id x y
we give such a p
and case on it.
It should of course just turn into rfl
.
Since retract Path→Id Id→Path
will first take in p : x ≡ y
we directly use J
.
Path≅Id : (x ≡ y) ≡ (Id x y)
Path≅Id {A} {x} {y} = iso Path→Id Id→Path rightInv leftInv where
rightInv : section (Path→Id {A} {x} {y}) Id→Path
rightInv rfl = {!!}
leftInv : retract (Path→Id {A} {x} {y}) Id→Path
leftInv = J {!!} {!!}
Hint 5
Checking the goal for rightInv
we should see it requires a point in
Path→Id (λ _ → x) ≡ rfl
, which is the same as Path→Id refl ≡ rfl
.
What’s happened is agda
knows that Id→Path rfl
is just refl
(they are externally equal), so instead of asking for a point of
Path→Id (Id→Path rfl) ≡ rfl
it just asks for a proof of the reduced version.
(In our heads we reduce (λ _ → x)
to refl
but agda
does the opposite.)
We extract the above result as a lemma :
Path→IdRefl : Path→Id (refl {x = x}) ≡ rfl
Path→IdRefl = {!!}
Solution
Since Path→Id
uses J
,
the only thing we can do here is use JRefl
:
Path→IdRefl : Path→Id (refl {x = x}) ≡ rfl
Path→IdRefl {x = x} = JRefl (λ y p → Id x y) rfl
Hint 6
For leftInv
, giving the correct motive requires knowing what retract
says.
It should look like
leftInv : retract (Path→Id {A} {x} {y}) Id→Path
leftInv = J (λ y p → Id→Path (Path→Id p) ≡ p) {!!}
Checking the goal we should see it requires a point in
Id→Path (Path→Id refl) ≡ refl
.
It should be that we just can replace Path→Id refl
with rfl
using our lemma Path→IdRefl : Path→Id refl ≡ rfl

but we haven’t proven anything about paths yet!
Let us do so now : if f : A → B
is a function (in our case Id→Path
)
then if two of its inputs are the same x ≡ y
then so are the outputs,
f x ≡ f y
.
cong : (f : A → B) (p : x ≡ y) → f x ≡ f y
cong = {!!}
We can prove this directly using J
or via Id
.
(We call it cong'
to avoid clashing with the library’s version)
Solutions
Cong : (f : A → B) → Id x y → Id (f x) (f y)
Cong f rfl = rfl
cong' : (f : A → B) (p : x ≡ y) → f x ≡ f y
cong' {x = x} f = J (λ y p → f x ≡ f y) refl
cong'' : (f : A → B) (p : x ≡ y) → f x ≡ f y
cong'' f p = Id→Path (Cong f (Path→Id p))
From now on we will just use cong
from the library,
but you can try to continue with your own version.
Now using cong
we can define leftInv
.
Noting that externally Id→Path rfl
is the same as refl
,
we just need to show that Id→Path (Path→Id refl) ≡ Id→Path rfl
.
Solution
leftInv : retract (Path→Id {A} {x} {y}) Id→Path
leftInv = J (λ y p → Id→Path (Path→Id p) ≡ p) (cong (λ p → Id→Path p) Path→IdRefl)
Concluding that the two types are isomorphic is a good reason to accept them as “the same” in the sense that if two spaces are isomorphic then they share the same properties, because isomorphism should interact nicely with other constructions. We expand upon this point in Part 3  Univalence.
Part 2  Properties of the Path Space
In Fundamental Group of the Circle we assume a couple of results about the path space, which we list here :
The basics : We can make
sym
(the analogue ofSym
) and composition of paths (called_∙_
); we can show that paths also satisfy groupoid laws.We have already made
cong
in the previous part (in Hint 6).The function
pathToFun
which takes a path between spaces and converts it to a function bewteen the spaces, following points along the path of spaces.The function
endPt
which follows a path along a bundle.
Some of these properties are what Homotopy Type theorists believe to be the absolute minimal necessary philosophical foundations for considering paths to be a good notion of equality :
refl
,sym
and_∙_
give us that it is an equivalence relationcong
tells us that any function respects equality.endPt
andpathToFun
approximately say that any predicate / family / bundleB : A → Type
respects equality.
The Basics
The direct proof of these are a good exercise on J
, or can be accomplished by
porting over results from the identity type using Path→Id
and Id→Path
.
We won’t go through each proof, but it is worth noting that since equalities tend
to be nonexternal, a little more work is required.
To see solutions for this, please see 0Trinitarianism/Quest4Solutions.agda
.
Chains of Equalities
Something that will help organizing the above proofs and work later on is a
notation for composition that suggests a “chain of equalities”.
Let’s say that we want to show that a + (b + c) ≡ c + (a + b)
for naturals a b c : ℕ
.
Then classically one might write
a + (b + c)
≡ by associativity
(a + b) + c
≡ by commutativity
c + (a + b)
In agda
we would have both proofs of associativity and commutativity.
Let’s call them ha
and hc
(in practice they would probably be something like
+assoc a b c
and +comm (a + b) c
).
Then using some cleverly defined notation, we can write in agda
example : (a b c : ℕ) → a + (b + c) ≡ c + (a + b)
example a b c =
a + (b + c)
≡⟨ ha ⟩
(a + b) + c
≡⟨ hc ⟩
c + (a + b)
∎
One you define _∙_
for composition of paths,
you can get access to this notation
by including the following code.
Try figuring out why it works.
_≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → x ≡ z  input \< and \>
_ ≡⟨ x≡y ⟩ y≡z = x≡y ∙ y≡z
_∎ : (x : A) → x ≡ x  input \qed
_ ∎ = refl
infixr 30 _∙_
infix 3 _∎
infixr 2 _≡⟨_⟩_
All of this is included in the solutions file.
pathToFun
The function pathToFun
(originally called transport
in the cubical library
)
has the following interpretations :
If two propositions are equal then one implies the other.
If two constructions can be identified then we can transport recipes of
A
over to recipes ofB
If two spaces look the same / if there is a path between spaces in the space of spaces then we can map one to the other (it turns out that we can make
pathToFun
always give us an isomorphism).
Try formalizing and defining pathToFun
in 0Trinitarianism/Quest4.agda
.
The Statement
pathToFun : A ≡ B → A → B
Hint 0
Use J
to reduce this to finding a map A → A
,
and choose the identity map.
Solution
id : A → A
id x = x
pathToFun : A ≡ B → A → B
pathToFun {A} = J (λ B p → (A → B)) id
Show that pathToFun
sends refl
to the identity map.
The Statment
pathToFunRefl : pathToFun (refl {x = A}) ≡ id
pathToFunRefl = {!!}
Solutions
Since the only thing we know about J
is how
it computes on refl
, we apply that :
pathToFunRefl : pathToFun (refl {x = A}) ≡ id
pathToFunRefl {A} = JRefl (λ B p → (A → B)) id
We might want to also make pathToFunReflx
 which says what
pathToFun refl
does at each point.
Solution
pathToFunReflx : (x : A) → pathToFun (refl {x = A}) x ≡ x
pathToFunReflx x = cong (λ f → f x) pathToFunRefl
endPt
The function endPt
(originally called subst
in the cubical library
)
has the following meanings :
If
B
is a predicate onA
andx ≡ y
are equal terms ofA
thenB x
impliesB y
. “We can substitutex
fory
in the proof ofB x
”.If
B
is a family of constructions dependent on terms ofA
andx ≡ y
are identified recipes ofA
, then recipes ofB x
can be turned into recipes ofB y
. “We can substitute the recipex
fory
in the recipe forB x
”.If
B
is a bundle over the spaceA
and we have a pathx ≡ y
between points inA
, then we can follow any “lifted path” starting at somebx : B x
to find its end pointby : B y
.
Predicates / families / bundles respect paths
If we have a predicate / family / bundle B
as above
and an equality x ≡ y
in A
,
then we know that cong
will give us an equality of spaces B x ≡ B y
.
However, only in the presence of pathToFun
is this equality any use 
surely if two spaces are equal then we should be able to
transport points from one to the other.
Hence endPt
/ pathToFun
(often both referred to as transport)
justify the statement “predicates / families / bundles” respect paths.
Try to formalize and prove endPt
in 0Trinitarianism/Quest4.agda
.
Then show that it sends refl
to what we expect.
Solutions
One option it is a raw application of J
.
endPt : (B : A → Type) (p : x ≡ y) → B x → B y
endPt {x = x} B = J (λ y p → B x → B y) id
endPtRefl : (B : A → Type) → endPt B (refl {x = x}) ≡ id
endPtRefl {x = x} B = JRefl ((λ y p → B x → B y)) id
We could also use cong
and pathToFun
as described above,
however due to size issues that we have not addressed in our
insufficiently general definition of cong
,
we have used the library’s version of cong
.
(Outside this quest we will be using the library’s version
of these definitions.)
endPt' : (B : A → Type) (p : x ≡ y) → B x → B y
endPt' B p = pathToFun (cong B p )
Part 3  Univalence
Paths on Other Constructions
The path space tends to interact nicely with other constructions. We give a list of examples here to demonstrate this point :
For points
(a0 , b0) (a1 , b1) : A × B
in the product of two spaces we have that(a0 , b0) ≡ (a1 , b1)
is “the same” space as the product of path spaces(a0 ≡ a1) × (b0 ≡ b1)
. Formally we express “the same” using an isomorphism :Path× : {A B : Type} (a0 a1 : A) (b0 b1 : B) → (_≡_ {A × B} ( a0 , b0 ) ( a1 , b1 )) ≅ ((a0 ≡ a1) × (b0 ≡ b1))
where we have some kind of product of spaces (however you wish to define it). We give a proof of this in
Quest4Solutions
; it is quite long but a good exercise in usingJ
.For points
x y : A ⊔ B
in the disjoint sum / coproduct of two spaces we have that the spacex ≡ y
is one of the four casesIf they are both “from
A
” thenx ≡ y
is “the same as” the corresponding path space inA
If they are respectively from
A
andB
thenx ≡ y
is “the same as” the empty spaceIf they are respectively from
B
andA
thenx ≡ y
is “the same as” the empty spaceIf they are both “from
B
” thenx ≡ y
is “the same as” the corresponding path space inB
We go through this example in detail here.
If we have two functions
f g : A → B
thenf ≡ g
is “the same” space as(a : A) → f a ≡ g a
. This is called “functional extensionality”. The HoTT proof of this is not straight forward, but in the side quests we will go through a cubicalspecific proof, which is much simpler.
Univalence
Now an important question arises from these considerations :
Important
We have nice ways of describing what paths between points in constructions are, but what should paths in the space of spaces be?
Looking back on this quest (an perhaps one’s life experience) we might think “isomorphism” as it is our competing notion of “the same” for spaces. The univalence axiom says something along the lines of this :
Univalence
If two spaces are isomorphic then they are equal.
isoToPath : {A B : Type} → A ≅ B → A ≡ B
Detail
Actually univalence tends to refer to something slightly different, whilst this is a corollary of it. Refer to The HoTT Book for more details.
Hence any isomorphism we have shown can be upgraded to a path between spaces
in cubical agda
.
For example (x ≡ y) ≡ (Id x y)
can now be shown.
Quest 4  Side Quests
Functional Extensionality
We show that two dependent functions
f g
being equal is the same as
them being equal when applied to each
value of the domain.
We call one of these directions
functional extensionality :
funExt : {B : A → Type} {f g : (a : A) → B a} →
((a : A) → f a ≡ g a) → f ≡ g
funExt = {!!}
Write this up in agda
and have a go at it.
We will cheat and use the native cubical definition of paths
(rather than using our axiomatic approach with J
and JRefl
etc),
since the HoTT proof of this is much more work.
A path in cubical agda
between two points x
and y
in a space A
can be defined by just taking an arbitrary
point i
on the “interval” I
, to a point in the space A
,
such that the end points agree.
Assuming we have the bundle B
, functions f g
,
a proof h
of (a : A) → f a ≡ ga
,
we can refine, and agda
will assume such an i
for us.
funExt : {B : A → Type} {f g : (a : A) → B a} →
((a : A) → f a ≡ g a) → f ≡ g
funExt B f g h = λ i a → {!!}
Checking the goal you should see something like the following (we have extracted the important parts):
Goal: B a
——————————————————————————————————
a : A
i : I
h : (a₁ : A) → f a₁ ≡ g a₁
g : (a₁ : A) → B a₁
f : (a₁ : A) → B a₁
B : A → Type
A : Type (not in scope)
———— Constraints ————————————————————————
?0 (i = i1) = g a : B a
?0 (i = i0) = f a : B a
We break this down :
agda
has assumed an arbitraryi : I
anda : A
, and is now asking for a point inB a
.Let’s call whatever we put in the goal
?0
; it has typeB a
. The constraints say that at the start and end points ofI
(calledi0
andi1
respectively)0? i
should bef a
andg a
respectively.To understand why
agda
also gave us ana : A
we can go back a step, removinga
. You should see that the goal at that point was a dependent function that at the start and end points aref
andg
respectively.Try to complete the quest. You will need that given a path
p
andi : I
along the interval, writingp i
gives the corresponding point along the pathp
.
Hint
The hypothesis h
applied to the point a
gives us a path from f a
to g a
in B a
.
Solution
funExt : {B : A → Type} {f g : (a : A) → B a} →
((a : A) → f a ≡ g a) → f ≡ g
funExt B f g h = λ i a → h a i
Now we can promote this to an isomorphism,
hence an equality between f ≡ g
and
(a : A) → f a ≡ g a
.
Try to formalize and prove this.
Solution
funExtPath : (B : A → Type) (f g : (a : A) → B a) → (f ≡ g) ≡ ((a : A) → f a ≡ g a) funExtPath {A} B f g = isoToPath (iso fun (funExt B f g) rightInv leftInv) where
fun : f ≡ g → (a : A) → f a ≡ g a fun h = λ a i → h i a
rightInv : section fun (funExt B f g) rightInv h = refl
leftInv : retract fun (funExt B f g) leftInv h = refl
Justifying J
Work in progress.
Fundamental Group of the Circle
Overview
One key attraction of HoTT (homotopy type theory)
is for doing homotopy theory synthetically  like
how one does Euclidean geometry from axioms without needing
the existence of the real numbers.
In this arc we will formalize what it means for the circle
S¹
to have fundamental group ℤ
in this setting.
Applying the philosophy of trinitarianism, is strongly recommended in this arc. However, it is designed so that anyone eager to see familiar geometric results can also start here with no prerequisites. Hence, this arc mostly adopts a geometric (hence categorical) perspective on types.
Quest 0  Working with the Circle
In this series of quests we will prove that the fundamental group
of S¹
is ℤ
.
In fact, our strategy will also show that the higher homotopy groups of
S¹
are all trivial.
You don’t need to know any prerequisites  in particular we will define
the fundamental group and higher homotopy groups
if you don’t know what they are already.
Important
In your cloned copy of the HoTT Game locate the file
1FundamentalGroup/Quest0.agda
,
and open this file in emacs
.
Before starting it is important to have a look at
our guide to emacs and list of emacs commands.
Part 0  The Circle
Theory  Definition of the Circle
We begin by formalising the problem statement.
A contruction of “the circle” is :
a point called
base
an edge from that point to itself called
loop
Here is our definition of the circle in agda
.
data S¹ : Type where
base : S¹
loop : base ≡ base
This reads :
S¹
is a point inType
, the space of spaces. In other words,S¹
is a space.base
is a point in the spaceS¹
loop
is a path inS¹
frombase
to itself. This is phrased as sayingloop
is a point inbase ≡ base
the space of paths frombase
tobase
.
Path
We think of a path in a space A
as consisting
of its starting point, its end point,
and some generic point in the middle
agreeing on the boundary.
You can see this as defining the circle via a CWcomplex.
Type theory notation
In general a : A
is read as a
is a point
in the space A
.
Note that in the above definition S¹
is seen
both as a point and a space depending on the context.
In cubical agda
,
everything is a point in a “unique” space.
Type theory notation
In general when a b : A
(a
and b
are points in a space A
),
we have a path space a ≡ b
,
whose points are paths from
a
to b
in the space A
.
Exercise  defining the constant path Refl
There are other paths in S¹
,
for example the constant path at base
.
In 1FundamentalGroup/Quest0.agda
navigate to
Refl : base ≡ base
Refl = {!!}
We will guide you through defining it.
We are about to construct a path Refl : base ≡ base
,
a path from base
to base
.
Tip
The {!!}
are called holes.
These are blanks in the agda
file that you can fill
to complete the quest.
You can write ?
to make a new hole.
We will fill the hole Refl = {!!}
.
Make sure you are in insert mode by pressing
i
. To escape insert mode pressESC
.Note
We have compiled a list of useful
emacs
andagda
commands in Emacs Commands.Enter
Cc Cl
(this meansCtrlc Ctrll
).
 Whenever you do this,
agda
will check the document is written correctly. We say
agda
compiles or loads the file. This will open the*Agda Information*
window looking like?0 : base ≡ base ?1 : (something) ?2 : (something) ...
This is the list of unfilled holes that are in your file currently. You should see that the holes in the file have changed in appearance, for example :
Refl : base ≡ base Refl = { }0
These are what holes look like when the file is compiled. The numbering is just for reference and may change upon reloading.
Navigate between holes using
Cc Cf
(forward) orCc Cb
(backward).Navigate to the first hole, making sure your cursor is inside the hole. Check the goal using
Cc C,
(this meansCtrlc Ctrlcomma
). Whenever you doCc C,
,agda
will tell you what kind of “point” it expects in the hole. The*Agda Information*
window should be focused on this hole only :Goal: base ≡ base
This says
agda
is expecting a path frombase
tobase
in the hole. Making sure your cursor is still inside the hole, enterCc Cr
. Ther
stands for refine. Whenever you do this whilst having your cursor in a hole,agda
will try to help you.You should now see
λ i → {!!}
. This is theagda
way of writingi ↦ {!!}
. Load the file again (usingCc Cl
) and the*Agda Information*
window should now look like :?0 : S¹ ... ?6 : (something) ———— Errors ——————————————— Failed to solve the following constraints: ?0 (i = i1) = base : S¹ (blocked on _3) ?0 (i = i0) = base : S¹ (blocked on _3)
Do not worry about the errors, we will soon explain it.
Navigate (
Cc Cf
andCc Cb
) to that new hole inλ i → {!!}
and enterCc C,
to check the goal. The*Agda information*
window should look like :Goal: S¹ ————————————————————————— i : I ———— Constraints —————————————— ?0 (i = i1) = base : S¹ (blocked on _3, belongs to problem 4) ?0 (i = i0) = base : S¹ (blocked on _3, belongs to problem 4) _4 := λ i → ?0 (i = i) (blocked on problem 4)
This says :
agda
is expecting a point inS¹
for this hole.you have a point
i
inI
available to you. You can think ofI
as the “unit interval” andi
as a generic point in the interval.The point in
S¹
that you give has to satisfy the constraints that it isbase
when “i = 1
” and “i = 0
”. Inagda
,i0
andi1
are the “start” and “end” point ofI
. Afterall, we are defining a path frombase
to itself.Don’t worry about the last line.
Since
Refl
is meant to be the constant path atbase
, writebase
in the hole.Press
Cc CSPC
to fill the hole withbase
. In general when you have some text (and your cursor) in a hole, doingCc CSPC
will tellagda
to replace the hole with that text.agda
will give you an error if it can’t make sense of your text.Tip
Everytime you are filling a hole, it is recommended that you first write what you want to fill in the hole then do
Cc CSPC
. You can do it in the reverse order, however the recommended order has other benefits down the line.Load the file again (
Cc Cl
). The*Agda Information*
window should now look like this :?0 : Bool ?1 : Bool ≅ Bool ?2 : Bool ≡ Bool ?3 : Type ?4 : doubleCover base ?5 : ⊥
The
?0 : S¹
has disappeared. This meansagda
has accepted what you filled this hole with.If you want to play around with this you reset this question by replacing what you wrote with
?
and doingCc Cl
.
Part 1  Refl ≡ loop
is empty
To get a better feel of S¹
,
we show that the space of paths (homotopies) between
Refl
and loop
, written Refl ≡ loop
, is empty.
Paths between paths
In general if we have p q : a ≡ b
in a space A
then a path Path : p ≡ q
in the path space a ≡ b
consists of
the starting path
p
the end path
q
and some generic path in between
Path i : a ≡ b
that agrees on the boundary
In algebraic topology this is called a path homotopy.
First, we define the empty space and what it means for a space to be empty.
Here is what this looks like in agda
:
data ⊥ : Type where
This says “the empty space ⊥
is a space with no points in it”.
Here are three candidate definitions for a space A
to be empty :
there is a point
f : A → ⊥
in the space of functions fromA
to the empty spacethere is a path
p : A ≡ ⊥
in the space of spacesType
fromA
to the empty spacethere is an isomorphism
i : A ≅ ⊥
of spaces
These turn out to be “the same” (see Different notions of “empty”), however for our present purposes we will use the first definition. Our goal is therefore to produce a point in the function space
( Refl ≡ loop ) → ⊥
The authors of this series have thought long and hard about how one would come up with the following argument. Unfortunately, sometimes mathematics is in need of a new trick and this was one of them.
The trick
We make a path p : true ≡ false
from the assumed path (homotopy) h : Refl ≡ loop
by
constructing a nontrivial Bool
bundle over the circle,
hence obtaining a map ( Refl ≡ loop ) → ⊥
.
To elaborate :
Bool
here refers to the discrete space with two points true, false
.
We will create a map doubleCover : S¹ → Type
that sends
base
to Bool
and the path loop
to
a nontrivial path flipPath : Bool ≡ Bool
in the space of spaces.
Viewing the picture vertically,
for each point x : S¹
,
we call doubleCover x
the fiber of doubleCover
over x
.
All the fibers look like Bool
, hence our choice of the name Bool
 *bundle*.
Homotopy type theory
A path p : X ≡ Y
between two spaces X Y : Type
(viewed as points in the space of spaces)
can be visualised as follows :
Two spaces
X
andY
as end points.For the generic point
i : I
in the intervalp i : Type
is a space that varies continuously with to respect toi
such thatp 0
isX
andp 1
isY
.
The continuity guarantees that each point along the path looks “the same”. In particular the end points look “the same”.
We will get a path from true
to false
in the fiber of doubleCover
over base
by “lifting the homotopy” h : Refl ≡ loop
and
considering the end points of the “lifted paths”.
Refl
will “lift” to a “constant path” and loop
will “lift” to
Let’s assume for the moment that we have flipPath
already and
define doubleCover
.
Make sure you are in insert mode.
Navigate to the definition of
doubleCover
and make sure you have loaded the file withCc Cl
.doubleCover : S¹ → Type doubleCover x = {!!}
Navigate to the hole and check the goal. It should look like
Goal: Type ———————————————————— x : S¹
This says it is expecting a point in
Type
, the space of spaces, i.e. it expects a space. We will first case on x by writingx
in the hole and doingCc Cc
(c
for cases). You should now see two new holes :doubleCover : S¹ → Type doubleCover base = {!!} doubleCover (loop i) = {!!}
This means :
S¹
is made from a pointbase
and an edgeloop
, so a map out ofS¹
to a space is the same as choosing a point to mapbase
to, and an edge to maploop
to respectively. Sinceloop
is a path frombase
to itself, its image must also be a path from the image ofbase
to itself.Navigate to the first new hole and check the goal. We want to map
base
to the spaceBool
so writeBool
in the hole, then doCc CSPC
to fill it.Navigate to the second new hole and check the goal. Here
loop i
is a generic point in the pathloop
, wherei : I
is a generic point of the “unit interval”. We are assuming we haveflipPath
defined already and want to maploop
toflipPath
, soloop i
should map to a generic point in the pathflipPath
.Note
We can use
flipPath
without completing the definition offlipPath
.Try filling the hole.
Once you think you are done, reload the
agda
file withCc Cl
and if it doesn’t complain this means there are no problems with your definition. Compare your definition to that in1FundamentalGroup/Quest0Solutions.agda
to check that your definition is the one we want. To navigate to solutions file escape insert mode usingESC
and doSPC f f
to find the file, see Emacs Commands. Here is a definition thatagda
will accept, but is not what we need:Bad definition
doubleCover : S¹ → Type doubleCover base = Bool doubleCover (loop i) = Bool
Defining flipPath
is quite involved and we will do so in the following part.
Part 2  Defining flipPath
via Univalence
In this part, we will define the path flipPath : Bool ≡ Bool
.
Recall the picture of doubleCover
.
This means we need flipPath
to correspond to
the unique nonidentity permutation of Bool
that flips true
and false
.
The function
We proceed in steps :
Define the function
Flip : Bool → Bool
.Promote this to an isomorphism
flipIso : Bool ≅ Bool
.We use univalence to turn
flipIso
into a pathflipPath : Bool ≡ Bool
. The univalence axiom asserts that paths inType
 the space of spaces  correspond to homotopyequivalences of spaces. As a corollary, we can make paths inType
from isomorphisms inType
.
Isomorphism
One with a topological mindset might worry if isomorphism means homeomorphism, homotopy equivalence, bijection or something else; one might even wonder what continuity is here. The answer is that this is synthetic homotopy theory, where
there is no need for real numbers
every map is continuous in the sense that they respect paths
an isomorphism
A ≅ B
is given by the data offun : A → B
inv : B → A
rightInv
that says (extensionally)fun ∘ inv
is homotopic to the identity, i.e. given anyb : B
we have a pathfun ∘ inv b ≡ b
.leftInv
that says (extensionally)inv ∘ fun
is homotopic to the identity.
You might notice that the above looks like the classical definition of homotopy equivalence. (They turn out to be “the same”.)
Univalence
We have described paths between points as giving a starting point, an ending point, and a generic point between that agrees on the boundary. Drawing a path between spaces in the space of spaces, we can see that such a path is the data of two spaces that “continuously look the same”:
We already have a notion of “the same” for spaces, which is isomorphism. Hence we assume the following “univalence” axiom : Any isomorphism can be turned into a path between spaces.
In
1FundamentalGroup/Quest0.agda
, navigate to :
Flip : Bool → Bool
Flip x = {!!}
Make sure you are in insert mode.
Check the goal. It should be asking for a point in
Bool
, since we have already given it anx : Bool
at the front.
Tip
Whenever you encounter a new hole, you should first check the goal.
Write
x
inside the hole, and case onx
usingCc Cc
with your cursor still inside. You should now see :Flip : Bool → Bool Flip false = {!!} Flip true = {!!}
This means : the space
Bool
is made of two pointsfalse, true
and nothing else, so to map out ofBool
it suffices to find images forfalse
andtrue
respectively.Since we want
Flip
to fliptrue
andfalse
, fill the first hole withtrue
and the second withfalse
.To check things have worked, try
Cc Cd
(d
stands for deduce its space). Thenagda
will ask you to input an expression. EnterFlip
. In the*Agda Information*
window, you should seeBool → Bool
This means
agda
recognisesFlip
as a wellformulated term and is a point in the space of maps fromBool
toBool
.We can also ask
agda
to compute outputs ofFlip
. TryCc Cn
(n
stands for normalise),agda
should again be asking for an expression. EnterFlip true
. In the*Agda Information*
window, you should seefalse
, as desired.
The isomorphism
Navigate to
flipIso : Bool ≅ Bool flipIso = {!!}
Refine with
Cc Cr
. You should now seeflipIso : Bool ≅ Bool flipIso = iso {!!} {!!} {!!} {!!}
Given two spaces
A
andB
,iso
(with respect toA
andB
) belongs to the following space :iso : (fun : A → B) (inv : B → A) (rightInv : section fun inv) (leftInv : retract fun inv) → A ≅ B
which says that
iso
will produce an isomorphism fromA
toB
given a mapfun
forwards and an inverseinv
backwards, and points of the spacesection fun inv
andretract fun inv
. Try to find out whatsection
andretract
are by doingCc Cn
and entering their respective names. They should respectively say thatinv
is a right and left inverse offun
.Check the first two holes,
agda
should expect functionsBool → Bool
to go in both of them. This is because it is expecting a function and its inverse, respectively, so fill them withFlip
and its inverseFlip
.Check the goal of the next two holes. They should be
section Flip Flip
and
retract Flip Flip
Add the following to your code (make sure you copy it exactly) :
flipIso : Bool ≅ Bool flipIso = iso Flip Flip {!!} {!!} where rightInv : section Flip Flip rightInv x = {!!} leftInv : retract Flip Flip leftInv x = {!!}
Then load the file with
Cc Cl
. Ifagda
gives an error it could be due tomissing spaces;
agda
is space sensitivewrong indentation before
rightInv
andleftInv
;agda
is intentation sensitivemissing the
where
in the second line.lower and upper case differences
where to use
where
The
where
allows you to make definitions local to the current definition, in the sense that you will not be able to accessrightInv
andleftInv
outside this proof. We will eventually fill the missing holes from before withrightInv
andleftInv
. If you like you can also place the definitions ofrightInv
andleftInv
beforeflipIso
.Check the goal of the hole
rightInv x = {!!}
. In the*Agda Information*
window, you should seeGoal: Flip (Flip x) ≡ x ————————————————————————————————— x : Bool
This says
rightInv
should give for eachx : Bool
a pathp : Flip (Flip x) ≡ x
. We gave anx : Bool
in front, so the goal is simply to give a pathp : Flip (Flip x) ≡ x
. Try to give such a path.Hint
You need to case on what
x
can be. Then for the case offalse
,Flip (Flip false)
should just befalse
by design, so you need to give a path fromfalse
tofalse
.The benefit of having
x
before the=
is that we can case on whatx
can be. This is called pattern matching.Do the same for
leftInv x = {!!}
.Fill in the missing goals from the original problem using
rightInv
,leftInv
.If you got the definition right then
agda
should not have any errors when you load usingCc Cl
.
The path
Navigate to
flipPath : Bool ≡ Bool flipPath = {!!}
In the hole, write in
isoToPath
and refine withCc Cr
. You should now haveflipPath : Bool ≡ Bool flipPath = isoToPath {!!}
If you check the new hole, you should see that
agda
is expecting an isomorphismBool ≅ Bool
.isoToPath
is the function from the cubical library that converts isomorphisms between spaces into paths between the corresponding points in the space of spacesType
.Fill in the hole with
flipIso
and useCc Cd
to checkagda
is happy withflipPath
.Try to normalise
pathToFun flipPath false
. You should gettrue
in the*Agda Information*
window.What
pathToFun
did is it took the pathflipPath
in the space of spacesType
and followed the pointfalse
asBool
is transformed alongflipPath
. The end result is of coursetrue
, sinceflipPath
is the path obtained fromflip
! Try to follow whatpathToFun
does in the animation.pathToFun
pathToFun
is calledtransport
in the cubical library.
Part 3  Lifting paths using doubleCover
By the end of this page we will have shown that
refl ≡ loop
is an empty space.
In 1FundamentalGroup/Quest0.agda
locate
Refl≢loop : Refl ≡ loop → ⊥
Refl≢loop h = ?
The cubical library has the result
true≢false : true ≡ false → ⊥
which says that the space of paths in Bool
from true
to false
is empty.
We will assume it here and leave the proof as a side quest,
see Proving true≢false.
Load the file with
Cc Cl
and navigate to the hole. Writetrue≢false
(input\==n
for≢
; see Emacs Commands) in the hole and refine usingCc Cr
,agda
knowstrue≢false
maps to⊥
so it automatically will make a new hole.Check the goal in the new hole using
Cc C,
it should be asking for a path fromtrue
tofalse
.
To give this path we need to visualise “lifting” Refl
, loop
and the homotopy h : Refl ≡ loop
along the Boolbundle doubleCover
.
When we “lift” Refl
 starting at the point true : doubleCover base

it will still be a constant path at true
,
drawn as a dot true
.
When we “lift” loop
 starting at the point true : doubleCover base

it will look like
The homotopy h : Refl ≡ loop
is “lifted”
(starting at “lifted Refl
”)
to some kind of surface
According to the pictures the end point of the “lifted”
Refl
is true
and the end point of the “lifted” loop
is false
.
We are interested in the end points of each
“lifted paths” in the “lifted homotopy”,
since this forms a path in the endpoint fiber doubleCover base
from true
to false
.
We can evaluate the end points of both “lifted paths” by using
something in the cubical library (called subst
) which we call endPt
.
endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
Note
It says given a bundle B
over space A
,
a path p
from x : A
to y : A
, and
a point bx
above x
,
we can get the end point of “lifted p
starting at bx
”.
So let’s make the function that takes
a path from base
to base
and spits out the end point
of the “lifted paths” starting at true
.
endPtOfTrue : base ≡ base → doubleCover base
endPtOfTrue p = {!!}
Check the goal. It should be asking for
Goal: Bool —————————————————————————─ p : base ≡ base ———— Constraints ——————————————— ?0 (p = loop) = false : Bool (blocked on _29, belongs to problem 90) ?0 (p = Refl) = true : Bool (blocked on _29, belongs to problem 90) _40 := λ p i → endPtOfTrue (p i) (blocked on problem 90)
We want to use
endPt
, which can output something in the spaceB y
(as described above). In this case we wantB y
to beBool
.agda
is smart and can figure out how to useendPt
:Type
endPt
into the hole and doCc Cr
.
Tip
In general if the goal of the hole
Goal: Y ———————————————————————— f : X → Y ...
is to find a point in a space
Y
and you have a functionf : X → Y
then you can writef
in the hole and doCc Cr
.You should see
endPtOfTrue : base ≡ base → doubleCover base endPtOfTrue p = endPt {!!} {!!} {!!}
Try to fill in these holes.
Once you think you are done, you can verify our expectation that
endPtOfTrue Refl
istrue
andendPtOfTrue loop
isfalse
usingCc Cn
.
Lastly we need to make the function endPtOfTrue
take the path h : Refl ≡ loop
to a path from true
to false
.
In general if f : A → B
is a function and p
is a path
between points x y : A
then we get a map cong f p
from f x
to f y
.
(Note that p
here is actually a homotopy h
.)
cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
We will define cong
in a side quest
Using cong
and endPtOfTrue
you should be able to complete Quest0
.
If you have done everything correctly you can reload agda
and see that
you have no remaining goals.
Quest 0  Side Quests
Different notions of “empty”
The following are “the same”,
there is a point
f : A → ⊥
in the space of functions fromA
to the empty spacethere is a path
p : A ≡ ⊥
in the space of spacesType
fromA
to the empty spacethere is an isomorphism
i : A ≅ ⊥
(input\cong
for≅
) of spaces
Here we will take “the same” to mean there are maps from any one to another (they are “propositionally the same”). We will first define the three.
In 1FundamentalGroup/Quest0.agda
, uncomment this side quest
and locate these three definitions :
_toEmpty : (A : Type) → Type
A toEmpty = {!!}
pathEmpty : (A : Type) → Type₁
pathEmpty A = {!!}
isoEmpty : (A : Type) → Type
isoEmpty A = {!!}
Note
You can use underscores when you name a function.
agda
will put the inputs in the underscores in order.
Tip
agda
supports unicode symbols such as ⊥
.
See here for how to insert ⊥
and other symbols.
Try to fill them in according to the above.
You may have noticed we used Type₁
in the second definition.
To find out what Type₁
is,
see Part 3  Universes in Trinitarianism.
Check that your definitions are the same as ours by comparing with
the solutions in
1FundamentalGroup/Quest0Solutions.agda
.
We will make maps from toEmpty A
to isoEmpty A
to pathEmpty A
and back to toEmpty A
.
First we show that the empty space maps into any other space. This is very useful when working with the empty space.
outOf⊥ : (A : Type) → ⊥ → A
outOf⊥ = {!!}
Try to fill in the definition without looking at the hint.
Hint
Recall the definition of the empty space being a CWcomplex with nothing in it. We can always case on variable points from CWcomplexes. What cases are there?
We fill in toEmpty→isoEmpty
toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A
toEmpty→isoEmpty A = {!!}
Tip
You can use where
to extract lemmas / make local definitions
like we did in defining flipIso
;
see here.
Hint 0
Check the goal to see what we have and what we need to give.
Assume
f : toEmpty A
by putting anf
before the=
.Refine the goal to see what
agda
suggests.
Hint 1
We need to give an isomorphism, i.e. a map from
A
to⊥
, and a map from⊥
toA
, and proofs that these satisfysection
andretract
respectively.If we have a point in
⊥
then we can get a point in any space.
Try filling in
isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
isoEmpty→pathEmpty A = {!!}
Hint
We converted an isomorphism to a path in quest 0.
Lastly try filling in
pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
pathEmpty→toEmpty A = {!!}
Check the goal
We can assume a path
p : pathEmpty A
Check the goal again
Since
toEmpty A
as defined asA → ⊥
we can assume a pointx : A
We can follow the point
x
along the pathp
usingpathToFun
, as we did forflipPath
in Quest 0  Working with the Circle.
Proving true≢false
Locate 1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda
we will show
true≢false : true ≡ false → ⊥
true≢false = {!!}
We do this by making a subsingleton bundle over Bool
whose fiber over true
is the singleton space ⊤
and fiber over false
is the empty space ⊥
.
The definition of ⊤
is
data ⊤ : Type where
tt : ⊤
Assume a path
h : true ≡ false
Define a map from
Bool
toType
(as a lemma or using where), that takestrue
to⊤
andfalse
to⊥
. This is a subsingleton bundle overBool
, since each fiber is⊤
and⊥
, having only a single or no points.We can follow how the point
tt : ⊤
changes along the pathh
usingpathToFun
, as we did forflipPath
in Quest 0  Working with the Circle. This should give you a point in the empty space⊥
.
Due to the previous side quest Different notions of “empty” this tells us
that the space true ≡ false
is empty.
Defining cong
Under construction
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 S¹
is ℤ
.
Intuitively,
the fundamental group of S¹
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 S¹
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 S¹
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 S¹ base
loop n times = {!!}
Note
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 S¹ base
loop pos n times = {!!}
loop negsuc n times = {!!}
It says to map out of ℤ
it suffices to
map the nonnegative 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 : ℤ → Ω S¹ 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 succesive integer suc n
inductively.
We can do the same with negsuc n
,
obtaining four cases.
loop_times : ℤ → Ω S¹ 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”
Individually
Try filling the first hole with what we get when we loop
0
(pos zero
) times.For looping
pos (suc n)
times we loopn
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 withloop
.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 : ℤ → Ω S¹ 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 S¹
.
In this quest we will construct one of the two comparison maps
across the whole circle, called windingNumber
.
The plan is :
Define a function
sucℤ : ℤ → ℤ
that increases every integer by oneProve that
sucℤ
is an isomorphism by constructing an inverse mappredℤ : ℤ → ℤ
.Turn the isomorphism
sucℤ
into a pathsucℤPath : ℤ ≡ ℤ
usingisoToPath
Define
helix : S¹ → Type
by mappingbase
toℤ
and a generic pointloop i
tosucℤPath i
.Use
helix
andendPt
to define the mapwindingNumberBase : base ≡ base → ℤ
. Intuitively it counts how many times a path loops aroundS¹
. a generic pointloop i
tosucℤPath i
.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:
Solution:
sucℤ : ℤ → ℤ sucℤ = ?
We will define
sucℤ
the same way we definedloop_times
: by induction. Do cases on the input ofsucℤ
. You should have something like :Solution:
sucℤ : ℤ → ℤ sucℤ pos n = ? sucℤ negsuc n = ?
For the nonnegative integers
pos n
we want to map to its successor. Recall that then
here is a point of the naturalsℕ
whose definition is :data ℕ : Type where zero : ℕ suc : ℕ → ℕ
Use
suc
to mappos 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 onn
and treat the(0 + 1)
case separately.Hint
Do
Cc Cc
onn
. Then mapnegsuc zero
topos zero
. Fornegsuc (suc n)
, map it tonegsuc n
.This completes the definition of
sucℤ
. UseCc Cn
to check it computes correctly. E.g. check thatsucℤ (negsuc zero)
computes topos zero
andsucℤ (pos zero)
computes topos (suc zero)
.
sucℤ
is an Isomorphism
The goal is to define
predℤ : ℤ → ℤ
which “takesn
to its predecessorn  1
”. This will act as the (homotopical) inverse ofsucℤ
. Now that you have experience from definingsucℤ
, try definingpredℤ
.Imitating what we did with
flipIso
and give a pointsucℤIso : ℤ ≅ ℤ
by usingpredℤ
as the inverse and provingsection sucℤ predℤ
andretract sucℤ predℤ
.
sucℤ
is a Path
Imitating what we did with
flipPath
, upgradesucℤIso
tosucℤPath
.
Part 2  Winding Number
The ℤ
bundle helix
We want to make a ℤ
bundle over S¹
by
‘copying ℤ across the loop via sucℤPath
’.
In Quest1.agda
locate
helix : S¹ → 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
S¹
, 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 = {!!}
Hint
endPt
evaluates the end point of ‘lifted paths’.
Try computing a few values using Cc Cn
,
you can try it on refl
, loop
, ‘loop three times’, ‘loop negative one times’ and so on.
Generalising
The function windingNumberBase
can actually be improved without any extra work to a function on all of S¹
.
windingNumber : (x : S¹) → 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 S¹
, in particular obtaining an isomorphism
between base ≡ base
and ℤ
.
Quest 2  ℤ
is a Set
An overview of this quest :
We want to show that the higher loop spaces of
S¹
are trivialWe note that it suffices to show that the loop space of
ℤ
is trivial, assuming the end resultloopSpace S¹ base ≡ ℤ
.Show that the loop space of any set is trivial, hence it suffices to show that
ℤ
is a setShow that
ℤ
looks like the sum of two disjoint copies ofℕ
, andℕ
is a set; it then suffices to show the general result that the disjoint sum of two sets is a set.To show that the disjoint sum of sets is a set we find ourselves trying to classify the path space of disjoint sums.
The bulk of the work will be to classify the path space of disjoint sums, and showing that it actually corresponds to the path space. This is the content of the last three parts.
Part 0  loopSpace loopSpace
We are interested in knowing what
the higher homotopy groups of S¹
might be.
Whilst the data of the fundamental group π₁ S¹
is captured
in loopSpace S¹ base
,
the data of π₂ S¹
would be captured in
loopSpace (loopSpace S¹ base) refl
;
loops in loopSpace S¹ base
based at refl
.
Points in the second loop space are paths h : refl ≡ refl
,
i.e. h
would be a homotopy from the constant path to itself.
The second loop space contains an obvious point refl : refl ≡ refl
(this is of course not the same “refl” as the one before),
and we could define the next loop space to be loops in
loopSpace (loopSpace S¹ base) refl
based at refl
(the one from loopSpace S¹ base
that is).
The important conclusion we will arrive at in this quest is
that the loop space of ℤ
 which will correspond to the
second loop space of S¹
(this is the conclusion of this entire arc) 
is trivial, in the sense that it just consists of a point (up to paths) :
loopSpace (loopSpace S¹ base) refl ≡ loopSpace ℤ 0 ≡ ⊤
Intuitively this is because the only loop (up to a path) in ℤ
from
0
to itself is refl
,
so loopSpace ℤ 0
is contractible 
it looks just like the singleton space ⊥
.
This is more general : any two paths in ℤ
are homotopic,
which we formalise in the definition isSet
.
isSet
isSet
The statement “any two paths in the space A
are homotopic”
is captured in the definition of isSet
:
isSet : Type → Type
isSet A = (x y : A) → isProp (x ≡ y)
In the above isProp
captures the statement
“any two points are (continuously) connected by a path” :
isProp : Type → Type
isProp A = (x y : A) → x ≡ y
If a type satisfies isSet
we say it is a set,
and if it satisfies isProp
we say it is a proposition.
Why the words "set" and "proposition"?
Intuitively a “set” is meant to be a bunch of disjoint points. However in homotopy type theory we consider points up to paths, and paths up to homotopy, hence a “set” is a bunch of disjoint blobs, where each blob is contractible to a point. In other words a “set” is a type where any circle (that lands in a blob) can be filled (hence the blob is contractible).
We will justify the use of the word “proposition” once we have introduced the propositional perspective on types, see trinitarianism and Part 5  Using the Propositional Perspective.
All maps are continuous in HoTT
There is a subtlety in the definition isProp
.
Having isProp A
is stronger than saying that the space A
is path connected.
Since A
is equipped with a continuous map taking pairs x y : A
to a path between them.
We will show in a later quest
that isProp S¹
is empty despite S¹
being path connected.
We can justify “the loop space of a set is trivial” by showing that
“if any two paths in a space A
are homotopic then
the loop space of A
at any point in A
looks like ⊤
”.
So we show that
isSet→LoopSpace≡⊤ : {A : Type} (x : A) → isSet A → (x ≡ x) ≡ ⊤
isSet→LoopSpace≡⊤ = {!!}
Locate this in 1FundamentalGroup/Quest2.agda
and try filling it in.
Hint 0
Imitating what we did with flipPath
and flipIso
reduce this to showing that for each x : A
and h : isSet A
we have
fun : x ≡ x → ⊤
inv : ⊤ → x ≡ x
rightInv : section fun inv
leftInv : retract inv fun
Hint 1
There is only one possible map from x ≡ x
to ⊤
since ⊤
is terminal (see trinitarianism).
To map out of ⊤
one can do cases and see that
you only need to map tt
.
Solution
fun
can just be(λ p → tt)
inv
can beinv : ⊤ → x ≡ x inv tt = refl
Hint 2
For rightInv
by casing on the point in ⊤
there should be nothing much to show.
For leftInv
we need to use our assumption
that “any two paths are homotopic”.
Solution
rightInv : section (λ p → tt) inv
rightInv tt = refl
leftInv : retract (λ p → tt) inv
leftInv p = h x x refl p
The goal
We have therefore reduced our goal to
showing that ℤ
is a set,
i.e. ℤ
only has trivial paths in it,
which will tell us that the second loop
(and in fact any higher loop space)
of S¹
is trivial.
Part 1  ℤ
as a disjoint sum ℕ ⊔ ℕ
As a first step, we note that ℤ
actually looks like
two disjoint copies of ℕ
, i.e. we have
ℤ≡ℕ⊔ℕ : ℤ ≡ ℕ ⊔ ℕ
where we have the definition of the disjoint sum of two spaces as follows
data _⊔_ (A B : Type) : Type where
inl : A → A ⊔ B
inr : B → A ⊔ B
It says there are two ways of making points in the space,
taking them from A
and taking them from B
.
Try proving ℤ ≡ ℕ ⊔ ℕ
in 1FundamentalGroup/Quest2.agda
.
Hint
As in defining flipPath
in quest 0
we first make an isomorphism and then convert it to a path/proof of equality.
To make the isomorphism note that
the definition of ℤ
is already as “two copies of ℕ
”,
as described in quest 1.
If you have made the function and inverse appropriately,
you should only need constant paths in the
proofs that they satisfy section
and retract
respectively.
Solution
ℤ≡ℕ⊔ℕ : ℤ ≡ ℕ ⊔ ℕ
ℤ≡ℕ⊔ℕ = isoToPath (iso fun inv rightInv leftInv) where
fun : ℤ → ℕ ⊔ ℕ
fun (pos n) = inl n
fun (negsuc n) = inr n
inv : ℕ ⊔ ℕ → ℤ
inv (inl n) = pos n
inv (inr n) = negsuc n
rightInv : section fun inv
rightInv (inl n) = refl
rightInv (inr n) = refl
leftInv : retract fun inv
leftInv (pos n) = refl
leftInv (negsuc n) = refl
We want to show that ℤ
is a set,
by using the path ℤ≡ℕ⊔ℕ
.
Intuitively if ℕ
is a set then two disjoint
copies of it should also be a set,
(think about filling circles on the disjoint sum).
Thus we can break down our goal into two :
Goal 1 : ℕ
is a set
isSetℕ : isSet ℕ
isSetℕ = {!!}
Goal 2
If A
and B
are both sets then A ⊔ B
is also a set.
Goal 1 will be handled in a side quest. We focus on Goal 2 from now on.
Part 2  Disjoint Sum of Sets is a Set
Try formulating (but not proving) the result isSet⊔
,
which should say “if spaces A
and B
are both sets
then so is their disjoint sum A ⊔ B
”.
This should be done in 1FundamentalGroup/Quest2.agda
where indicated.
Solution
isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ = {!!}
Without proving this, we can use this to show isSet (ℕ ⊔ ℕ)
using isSetℕ : isSet ℕ
,
which will be shown in a side quest.
Then using either pathToFun
or endPt
you can show
isSet ℤ
from isSet (ℕ ⊔ ℕ)
,
using the path from ℤ
to ℕ ⊔ ℕ
we made earlier.
Try to set up everything described in this paragraph where indicated
in 1FundamentalGroup/Quest2.agda
.
Hint : The statement
isSetℤ : isSet ℤ
Hint : following along paths
To use pathToFun
you must figure out what path you are following
and what point you are following the path along.
To use endPt
you must figure out what bundle you are making,
what the path in the base space is,
and what point you are starting at in the first fiber.
Partial solutions
The point you need to follow in either case
is the point in the space isSet (ℕ ⊔ ℕ)
:
isSetℤ : isSet ℤ
isSetℤ = pathToFun {!!} (isSet⊔ isSetℕ isSetℕ)
isSetℤ' : isSet ℤ
isSetℤ' = endPt {!!} {!!} (isSet⊔ isSetℕ isSetℕ)
Solutions
isSetℤ : isSet ℤ
isSetℤ = pathToFun (cong isSet (sym ℤ≡ℕ⊔ℕ)) (isSet⊔ isSetℕ isSetℕ)
isSetℤ' : isSet ℤ
isSetℤ' = endPt (λ A → isSet A) (sym ℤ≡ℕ⊔ℕ) (isSet⊔ isSetℕ isSetℕ)
Refining issues
If you tried refining using endPt
you may have been given 2 holes instead of 3.
This is because agda
had too many
possible options when trying to match up
the output of endPt
and the goal.
To add an extra hole simply add a ?
afterwards and reload.
Once this is complete we can go back and work on isSet⊔
.
Part 3  Path Space of Disjoint Sums
Motivation
Locate your formulation of
isSet⊔
.We assume
hA : isSet A
,hB : isSet B
, and pointsx y : A ⊔ B
. Currently our code looks likeisSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B) isSet⊔ hA hB x y = {!!}
Check the goal. It should be asking for a point in the space
isProp (x ≡ y)
.We need to consider how to get information on the path space of
A ⊔ B
when our hypotheses are about the path spaces ofA
andB
respectively. We could try to case onx
andy
.If
x
andy
are “both fromA
”, i.e. of the forminl ax
andinl ay
forax ay : A
, then we need to find a point inisProp (inl ax ≡ inl ay)
. This should be due tohA
, which gives ushA ax ay : isProp (ax ≡ ay)
. So somehow we need to identify the path spacesinl ax ≡ inl ay
andax ≡ ay
(try to formalize this, though we are not expecting a solution here).If
x
andy
are of the formsinl ax
andinr by
respectively forax : A
andby : B
then intuitively the spaceinl ax ≡ inr bx
should be empty, since the sum is disjoint (again we are not expecting a solution here).The other two cases are similar.
The conclusion is that we need some kind of classification of the path space of disjoint sums.
Classifying the Path Space of Disjoint Sums
Path space of disjoint sums
A path in the the disjoint sum should just be a path in one of the two parts.
This says points from A
cannot be confused with points from B
or points in A
that they were not already path connected to.
For now we leave isSet⊔
alone and define a function ⊔NoConfusion
that takes two points in A ⊔ B
and returns a space,
which is meant to represent the path space in each case,
as described in our motivation above.
Try to formulate (but not fill in) this where indicated in
Quest2.agda
.
It should look like:
Solution
⊔NoConfusion : {A B : Type} → A ⊔ B → A ⊔ B → Type
⊔NoConfusion = {!!}
Assume points x
and y
in the disjoint sum
and try to case on them.
There should be four cases.
When both points are from
A
, i.e. they areinl ax
andinl ay
, then we should give the spaceax ≡ ay
, which we expect to be isomorphic toinl ax ≡ inl ay
.(Two cases) When each is from a different space we expect the path space between them to be empty, so we should give
⊥
.If both are from
B
then we should imitate what we did in the first case
Solution
⊔NoConfusion : A ⊔ B → A ⊔ B → Type
⊔NoConfusion (inl x) (inl y) = x ≡ y  Path A x y
⊔NoConfusion (inl x) (inr y) = ⊥
⊔NoConfusion (inr x) (inl y) = ⊥
⊔NoConfusion (inr x) (inr y) = x ≡ y  Path B x y
Using the Classification
Now we have two of goals :
Path≡⊔NoConfusion
: We need to show that for eachx y : A ⊔ B
the path space looks like our classification, i.e. that(x ≡ y) ≡ (⊔NoConfusion x y)
isSet⊔NoConfusion
: ForisSet⊔
, givenhA : isProp A
,hB : isProp B
andx y : A ⊔ B
we needed to showisProp (x ≡ y)
. Hence we want to show that under the same assumptionsisProp (⊔NoConfusion x y)
.
Formalise (but don’t prove) both of these where indicated in
1FundamentalGroup/Quest2.agda
.
They should look like
Solutions
Path≡⊔NoConfusion : (x y : A ⊔ B) → (x ≡ y) ≡ ⊔NoConfusion x y
Path≡⊔NoConfusion = {!!}
isSet⊔NoConfusion : isSet A → isSet B → (x y : A ⊔ B) → isProp (⊔NoConfusion x y)
isSet⊔NoConfusion = {!!}
Tip
If you are tired of writing {A B : Type} →
each time
you can stick
private
variable
A B : Type
at the beginning of your agda
file,
and it will assume A
and B
implicitely
whenever they are mentioned.
Make sure it is indented correctly.
Without showing either of these new definitions,
try using them to complete isSet⊔
.
Hint
We can use pathToFun
or endPt
to follow how a point of “isProp
applied to ⊔NoConfusion
”
changes into a point of “isProp
on the path space x ≡ y
”.
Partial solutions
isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ hA hB x y = pathToFun {!!} (isSet⊔NoConfusion hA hB x y)
isSet⊔' : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔' hA hB x y = endPt {!!} {!!} (isSet⊔NoConfusion hA hB x y)
Solutions
isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ hA hB x y = pathToFun (cong isProp (sym (Path≡⊔NoConfusion x y)))
(isSet⊔NoConfusion hA hB x y)
isSet⊔' : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔' hA hB x y = endPt (λ A → isProp A) (sym (Path≡⊔NoConfusion x y))
(isSet⊔NoConfusion hA hB x y)
Proving isSet⊔NoConfusion
We will now show that ⊔NoConfusion
“is a set”.
Locate your definition of isSet⊔NoConfusion
and try proving it.
Hint
We need to case on the points in A ⊔ B
.
If they are both “from
A
” then we need to show that the path spaces inA
are propositions.(2 cases) If they are from different spaces then we must show that the path spaces in
⊥
are propositions.If they are both “from
B
” then it is similar to the first case.
Part 4  Proving Path≡⊔NoConfusion
It suffices to make an isomorphism
Replicate our proof of flipPath
in quest 0,
it suffices to show an isomorphism instead of an equality.
Make this precise in 1FundamentalGroup/Quest2
.
Spoiler
So that you can follow, we will make a lemma (you don’t have to) :
Path≅⊔NoConfusion : (x y : A ⊔ B) → (x ≡ y) ≅ ⊔NoConfusion x y
Path≅⊔NoConfusion = {!!}
To prove the isomorphism (for each arbitrary x
and y
) we need
four things, which we can extract as local definitions / lemmas using where
.
Spoiler
fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
fun x y = {!!}
inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y
inv x y = {!!}
rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
rightInv {A} {B} = {!!}
leftInv : (x y : A ⊔ B) → retract (fun x y) (inv x y)
leftInv = {!!}
inv
First try defining inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y
.
Hint 0
Check the goal.
You can assume points x y : A ⊔ B
and a point h : ⊔NoConfusion x y
.
If you case on x
and y
you might find there are fewer cases than you need.
This is because ⊔NoConfusion (inl ax) (inr by)
was defined to be empty, so agda
automatically removes the case.
Hint 1
In the case that both points are from x
we need to show that
given a proof p : ax ≡ ay
we get a proof of inl ax ≡ inr ay
.
We already have the result that if two points are equal then
their images under a function are equal.
Solution
inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y
inv (inl x) (inl y) p = cong inl p
inv (inr x) (inr y) p = cong inr p
Attempting fun
We try to define the map forward, which we called fun
.
If we assume and case on x
and y
in the disjoint sum then
When
x
andy
are both fromA
then they will beinl ax
andinl ay
, so checking the goal we should be required to give a point ininl x ≡ inl y → x ≡ y
. Reading this carelessly one could call this “inl
is injective”.When
x
andy
are from different spaces then checking the goal, we should be required to give a point ininl ax ≡ inr by → ⊥
. This says there are no paths between the disjoint parts.The last case is similar to the first.
We can extract the second case as a lemma :
Spoiler
disjoint : (a : A) (b : B) → inl a ≡ inr b → ⊥
disjoint a b p = {!!}
which we can prove by constructing a subsingleton bundle
over A ⊔ B
,
just like we did to prove that true ≡ false
is empty,
in the side quest.
In fact this is a generalisation of that result,
and the proof also generalises.
Hint
We make a bundle over the disjoint union
with the starting fiber as ⊤
and the
ending fiber as ⊥
.
Solution
disjoint : (a : A) (b : B) → inl a ≡ inr b → ⊥
disjoint a b p = endPt bundle p tt where
bundle : A ⊔ B → Type
bundle (inl a) = ⊤
bundle (inr b) = ⊥
The other case is quite problematic. This is what we want to show
inlInj : (x y : A) → (inl {A} {B} x ≡ inl y) → x ≡ y
inlInj x y p = {!!}
Here are the problems:
If we had a map backwards that cancelled
inl
we would be done, but in general this doesn’t exist. For example, ifA
were empty andB
had a point then we cannot expect to have a mapA ⊔ B → A
.There is nothing to induct on : we have no information about
x y : A
. More importantly :Important
We don’t know how to induct on paths.
Specifically we don’t yet know how to map out of a path space in general.
To find out how to induct on paths, complete quest 4 in trinitarianism, and return to this quest with a completely new perspective.
Part 5  Using the Propositional Perspective
After learning about the propositional perspective on equality, we can review some of the things we showed in a new light :
a ≡ b → ⊥
can be read asa
is not equal tob
since assuming a proof thata
is equal tob
we have a point in the empty space.In showing an isomorphism between spaces we must show that two functions satisfy
fun (inv x) ≡ x
for eachx
in the domain. This can now be read asfun
composed withinv
is equal to the identity on points.isoToPath
says that if two spaces are isomorphic then they are equal.endPt
(subst
for substitute in the library) takes a bundle and a proof thatx ≡ y
in the base space and substitutesx
fory
, hence replacing a point in the fiber ofx
with a point in the fiber ofy
.cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
says that if two points are equal then their images are equal.true
is not equal tofalse
refl
is not equal toloop
flipPath : Bool ≡ Bool
is a nontrivial equality betweenBool
and itself.inl
is injective (we still have not shown this yet).The objective of this whole arc is to show that the fundamental group of the circle is equal to
ℤ
.
isProp
says there is at most one point in the space; at most one proof of the proposition. Classically propositions are meant to only have a single proof (“proof irrelevance”), because for propositionsA
andB
, having implicationsA → B
andB → A
is enough to showA ≡ B
.
isSet
says between any two points there is at most one path between them, i.e. “there is onlyrefl
”, i.e. the space is disjoint.
We shall apply this perspective to the problem at hand.
fun
Now that we know how to induct on paths,
we need to pick a path to induct on.
Continuing with trying to show that inl
is injective
we will notice that path induction does not actually work here,
since we have
a start point
ax : A
a variable end point
ay : A
but the path is in the disjoint union
inl ax ≡ inl ay
not a path inA
We instead take a step back and look at fun
itself.
(You can now abandon inlInj
if you like,
this will become a corollary of the classification.)
We also remove the cases so that we are back to just having
fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
fun x y = {!!}
You might have noticed by now that we are in the perfect position to
induct on paths in x ≡ y
.
Path induction  J
 says that to make
a function (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
,
it suffices just to give a point in ⊔NoConfusion x x
.
Formalise the above
(without showing ⊔NoConfusion x x
yet) :
Spoiler
fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
fun x y = J (λ y' p → ⊔NoConfusion x y') {!!}
To prove ⊔NoConfusion x x
it would be convenient to be able to case on x
so we will extract it as a lemma.
Once you extract and case on x
this it should be quite easy to show.
Spoiler
⊔NoConfusionSelf : (x : A ⊔ B) → ⊔NoConfusion x x
⊔NoConfusionSelf (inl x) = refl
⊔NoConfusionSelf (inr x) = refl
rightInv
Try to define
rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
.
Hint 0
It is a good idea to case on x
and y
in the space A ⊔ B
,
since inv
is the first to take these inputs in here,
and inv
was defined by casing on x
and y
.
This should reduce us to just two cases,
like when defining inv
.
We will just describe the case when they are both from A
.
Hint 1
We can use J
to reduce to the case of when the path is refl
.
(No proof of the refl
case yet.)
Solution
rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
rightInv {A} {B} (inl x) (inl y) p =
J (λ y' p → fun {A} {B} (inl x) (inl y') (inv (inl x) (inl y') p) ≡ p) {!!}
We added the implicit arguments {A}
and {B}
so we can actually access them here.
The remaining hole is for showing that
fun (inl x) (inl x) (inv (inl x) (inl x) refl) ≡ refl
Hint 2
It would help to make a chain of equalities.
We defined inv (inl x) (inl x) refl
to be refl
,
so we only need to show that
fun (inl x) (inl x) refl ≡ refl
Since fun
was defined using J
we need to know how
J
computes when it is fed refl
.
We described this before, it is called JRefl
.
Solution
rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
rightInv {A} {B} (inl x) (inl y) p = J (λ y' p → fun {A} {B} (inl x) (inl y') (inv (inl x) (inl y') p) ≡ p)
(
fun {A} {B} (inl x) (inl x) refl
≡⟨ JRefl {x = inl x} ((λ y' p → ⊔NoConfusion {A} {B} (inl x) y')) _ ⟩
 uses how J computes on refl
refl ∎
) p
rightInv {A} {B} (inr x) (inr y) p = {!!}
leftInv
Try to define leftInv
.
Hint 0
We do this but each part of this proof will be relevant anywayuse J
since fun
“happens first”.
This should reduce the problem to showing
inv x x (fun x x refl) ≡ refl
Solution
leftInv : (x y : A ⊔ B) → retract (fun x y) (inv x y)
leftInv x y = J (λ y' p → inv x y' (fun x y' p) ≡ p) {!!}
Hint 1
If you extract what is needed as a lemma
you can case on the variable.
Remember to use JRefl
for the application of fun
.
Solution
leftInv : (x y : A ⊔ B) → retract (fun x y) (inv x y)
leftInv x y = J (λ y' p → inv x y' (fun x y' p) ≡ p)
(
(inv x x (fun x x refl))
≡⟨ cong (inv x x) (JRefl ((λ y' p → ⊔NoConfusion x y')) _) ⟩
inv x x (⊔NoConfusionSelf x)
≡⟨ lem x ⟩
refl ∎
) where
lem : (x : A ⊔ B) → inv x x (⊔NoConfusionSelf x) ≡ refl
lem (inl x) = refl
lem (inr x) = refl
Quest 3  The Loop Space is ℤ
In Quest 1  Loop Space of the Circle we introduced our main
method of proving that the fundamental group
(which we take to be loopSpace S¹ base
for now)
is ℤ
,
and in Quest 2  ℤ is a Set we decided that this
means to show that they are equal spaces.
.. admonition:: The Goal
loopSpace≡ℤ : loopSpace S¹ base ≡ ℤ loopSpace≡Z = {!!}
As usual we will show this via giving an isomorphism,
so we must make comparison maps forward and back.
However, we discovered we had to define the backwards map
over all of S¹
.
We already have windingNumber
, the forwards comparison map,
which gives us a map loopSpace S¹ base → ℤ
when applied to base
.
windingNumber : (x : S¹) → base ≡ x → helix x
In this quest our goal is to make a map backwards
Current Goal
rewind : (x : S¹) → helix x → base ≡ x
Since windingNumber
took a path and found how
many times the path loops around, in general “an integer twisted around the helix a bit”,
or “an integer plus a bit”.
We want to make rewind
do the reverse.
So rewind
should take “an integer n
plus a bit”,
loop around n
times, then add that extra corresponding bit,
the path from base
to x
to the end.
Part 0  rewind
Dependent paths
We try making rewind
.
We can assume a point x : S¹
,
then case on what it is.
rewind : (x : S¹) → helix x → base ≡ x
rewind base = {!!}
rewind (loop i) = {!!}
In the case of base
we want a map
from helix base
i.e. ℤ
, to base ≡ base
.
Try filling this in.
Solution
We want this to be the correct inverse,
described as looping around n
times and adding that extra bit on the end.
However there is nothing to add at the end in this case,
so it should just be loop_times
,
which we already defined in Quest 1  Loop Space of the Circle.
The case of loop i
will be a lot more work.
Checking the goal we see that at each point loop i
on the loop, it wants a point in the space
helix (loop i) → base ≡ (loop i)
,
which it might reduce to sucℤPath i → base ≡ (loop i)
according to the definition of helix
.
Collecting these spaces together along this i
,
we obtain a loop in the space of spaces based at the space ℤ → base ≡ base
given by
λ i → helix (loop i) → base ≡ (loop i) : (ℤ → base ≡ base) ≡ (ℤ → base ≡ base).
Now collecting the points we need to give into a “path” as well,
we obtain the notion of a dependent path :
each point of this “path” belongs to a space along the path of spaces.
We define dependent paths and design a way of mapping out of
S¹
in general in Quest 5  Dependent Paths from Trinitarianism.
We assume from now on knowledge of dependent paths.
Using outOfS¹
Now that we have a way of mapping out of S¹
(using PathD
),
called outOfS¹D
,
try to use it to repackage the work we have to far.
Solution
Originally we have
rewind : (x : S¹) → helix x → base ≡ x
rewind base = loop_times
rewind (loop i) = {!!}
Now we rearrange this to
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times {!!}
since our bundle over S¹
is (λ x → helix x → base ≡ x)
and our image for base
is loop_times
.
Checking the last goal, it remains to give a dependent path of type
PathD (λ i → sucℤPath i → base ≡ loop i) loop_times loop_times
.
Remembering the definition of PathD
,
this should be exactly giving a path
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times ≡ loop_times
,
since PathD
reduces the issue of dependent paths to just paths in
the end space, which is ℤ → base ≡ base
in this case.
Let’s make this a chain of equalities :
Solution
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ {!!} ⟩
loop_times ∎
)
Functions and pathToFun
The map loop_times
takes an integer and
does loop
that many times.
On the other hand pathToFun
follows how loop_times
changed along the path of spaces λ i → sucℤPath i → base ≡ loop i
,
and spits out the corresponding point at the end.
This path of spaces is specifically a path of function spaces,
so we need to find a more explicit way of describing what pathToFun
does to spaces of functions.
To generalize, suppose we have spaces A0 A1 B0 B1 : Type
and paths A : A0 ≡ A1
and B : B0 ≡ B1
.
Then let pAB
denote the path
λ i → A i → B i : (A0 → B0) ≡ (A1 → B1)
.
We want to figure out what pathToFun
does when it follows a function f : A0 → B0
along the path pAB
.
We know by functional extensionality that the function
pathToFun pAB f : A1 → B1
should be determined by what it does to terms in A1
,
so we can assume a1 : A1
.
The idea is we “apply f
by sending a1
back to A0
”.
Since pathToFun (sym A) a1
is meant to give the point in A0
that “looks like a1
”, we try applying f
to this point,
then send it across again via the path B
to the point
f (pathToFun (sym A) a1)
looks like in B1
.
We expect the outcome to be the same.
pathToFun→ : {A0 A1 B0 B1 : Type} {A : A0 ≡ A1} {B : B0 ≡ B1} (f : A0 → B0) →
pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
The proof of this in cubical agda
is simply refl
,
so we need not even extract it as a lemma.
A cubical hack
Is actually one of the axioms asserted in cubical agda
that pathToFun (λ i → A i → B i) f
is externally equal to
λ a1 → pathToFun B (f (pathToFun (sym A) a1))
.
Here we are using the cubical
definition of pathToFun
so we can simply give refl
for its proof.
However, according the definition of pathToFun
we gave
in Trinitarianism, they are not externally equal
but can be shown to be internally equal using J
.
We prove this from our own definitions
here.
We interpret what this result means in our specific case :
We are making pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
into another map in the space ℤ → base ≡ base
,
by following along the diagram
Specifically, this map should take n : ℤ
and first send it backwards along
sucℤPath
, supposedly giving us n  1
.
Then it applies loop_times
, obtaining the loop loop (n  1) times
.
Lastly it follows loop (n  1) times
along the path λ i → base ≡ loop i
(which itself is a loop starting and ending at base ≡ base
in the space of spaces),
obtaining some path from base ≡ base
, which we expect to be internally
equal to loop n times
.
Try putting this together in our definition of rewind
,
as a new intermediate step in our chain of equalities.
Solution
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ {!!} ⟩
loop_times ∎
)
We can simplify the above expression.
We know that pathToFun (sym sucℤPath) n
should follow n
along sucℤPath
backwards, so it should be n  1
.
We can use this to move a step closer to the goal.
Solution
This equality is definitional.
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop (predℤ n) times))
≡⟨ {!!} ⟩
loop_times ∎
)
The path fibration and pathToFun
It remains to find out how pathToFun
interacts with the path of loops coming out of base.
We call “the path of loops coming out of base” λ i → base ≡ loop i
the path fibration
at base
.
The animation tells us that we are gradually concatenating the input loop (n  1) times
with loop
.
Hence we should obtain loop (n  1) times ∙ loop
.
We are a bit lucky here, and these are in fact definitionally equal,
but to justify this in general, we can prove that
“following along the path fibration is the same as concatenating”.
pathToFunPathFibration : {A : Type} {x y z : A} (q : x ≡ y) (p : y ≡ z) →
pathToFun (λ i → x ≡ p i) q ≡ q ∙ p
This is in fact a quick exercise.
Hint
We take the propositional perspective 
without loss of generality we can assume
y
and z
are exactly the same.
Crucially : we know what pathToFun
does to refl
(recall pathToFunRefl
from the quest on paths).
Solution
pathToFunPathFibration : {A : Type} {x y z : A} (q : x ≡ y) (p : y ≡ z) →
pathToFun (λ i → x ≡ p i) q ≡ q ∙ p
pathToFunPathFibration {A} {x} {y} q = J (λ z p → pathToFun (λ i → x ≡ p i) q ≡ q ∙ p)
(
pathToFun refl q
≡⟨ pathToFunRefl q ⟩
q
≡⟨ ∙Refl q ⟩
q ∙ refl ∎
)
To include this in rewind
we have
Spoiler
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩  how pathToFun interacts with →
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩  sucℤPath is just taking successor, and so its inverse is definitionally taking predecessor
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (predℤ n)))
≡⟨ funExt (λ n → pathToFunPathFibration _ _) ⟩  how pathToFun interacts with the "path fibration"
(λ n → (loop (predℤ n) times) ∙ loop)
≡⟨ {!!} ⟩
loop_times ∎
)
There are several ways to complete this final part. We will leave the rest in a hint.
Hint
Applying functional extensionality we just need to show that for each n : ℤ
the outputs are equal, i.e. loop predℤ n times ∙ loop ≡ loop n times
.
By our design of loop_times
we should have that
loop m times ∙ loop
is equal to loop (m + 1) times
.
Then we are reduced to showing that loop (sucℤ predℤ n) times ≡ loop n times
,
or just sucℤ predℤ n ≡ n
.
Solution
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩  how pathToFun interacts with →
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩  sucℤPath is just taking successor, and so its inverse is definitionally taking predecessor
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (predℤ n)))
≡⟨ funExt (λ n → pathToFunPathFibration _ _) ⟩  how pathToFun interacts with the "path fibration"
(λ n → (loop (predℤ n) times) ∙ loop)
≡⟨ funExt (λ n →
loop predℤ n times ∙ loop
≡⟨ loopSucℤtimes (predℤ n) ⟩
loop (sucℤ (predℤ n)) times
≡⟨ cong loop_times (sucℤPredℤ n) ⟩
loop n times ∎) ⟩
loop_times ∎
)
We can check that rewind base
is indeed loop_times
by using Cc Cn
.
This is to be expected as outOfS¹
evaluated at base
should back exactly what we fed it,
as mentioned in the discussion on mapping out of the circle.
Part 1  rewind
is a right inverse
We are now in a position to approach the main goal :
loopSpaceS¹≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpaceS¹≡ℤ = {!!}
We have reduced this to giving an isomorphism,
which involves giving the map windingNumber base
forward
and loop_times
backwards,
and showing that they are inverses of each other.
Hence the next step is to show that
“looping n
times then taking the winding number gives back n
”.
Try to state and prove this in 1FundamentalGroup/Quest3.agda
.
In the hints we will use intuitive notation for integers
that may not align exactly with agda
code.
The statement
windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase = {!!}
We identify rewind base
with loop_times
,
since they are externally equal.
Hint 0
Since loop_times
was defined by casing on n
we case on n

it could be zero, a positive integer, negative one, or less than negative one.
Hint 1
Some of the cases are trivial 
we know exactly what loop 0 times
and windingNumber base loop
are.
Solution for Hint 1
windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase (pos zero) = refl
windingNumberRewindBase (pos (suc n)) = {!!}
windingNumberRewindBase (negsuc zero) = refl
windingNumberRewindBase (negsuc (suc n)) = {!!}
Hint 2
We can identify windingNumber base
with its definition,
reducing the problem to showing that
endPt helix (loop n times) 0
is equal to n
,
in the seperate cases.
For the first case,
we can reduce loop (n + 1) times
to just loop n times ∙ loop
since that was the definition.
Hence we are interested in what endPt helix (loop n times ∙ loop) 0
is.
Recalling our intuition behind endPt
,
this amounts to following the point 0
up the helix
along the path
loop n times ∙ loop
.
This should just be going to endPt helix (loop n times) 0
then adding 1
.
You can also check what agda
reduces the expression to by writing it in the hole and
then doing Cc Cn
.
It should look something like sucℤ (transp (λ i → helix (loop pos n times i)) i0 (pos 0))
.
Clearly it has reduced the definition a bit too far,
but the important idea is there, that it is + 1
of whatever data we have already.
Lastly we can just take sucℤ
on both sides of an equality we have from the induction hypothesis.
Solution
For one of the cases we detail the thought process going on above, and for the last case we extract only the important part of the proof.
windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase (pos zero) = refl
windingNumberRewindBase (pos (suc n)) =
windingNumber base (rewind base (pos (suc n)))
≡⟨ refl ⟩
windingNumber base (loop (pos n) times ∙ loop)
≡⟨ refl ⟩
endPt helix (loop (pos n) times ∙ loop) (pos zero)
≡⟨ refl ⟩
sucℤ (endPt helix (loop (pos n) times) (pos zero))
≡⟨ cong sucℤ (windingNumberRewindBase (pos n)) ⟩
sucℤ (pos n)
≡⟨ refl ⟩
pos (suc n) ∎
windingNumberRewindBase (negsuc zero) = refl
windingNumberRewindBase (negsuc (suc n)) = cong predℤ (windingNumberRewindBase (negsuc n))
You might wonder if it is possible to make the above map work across all of S¹
,
and the answer is yes.
This is not really necessary for our goal,
so feel free to skip to the next part if you are not interested.
Try stating and proving the generalization of the above;
which we call windingNumberRewind
.
The Statement
windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind = {!!}
Hint 0
We defined rewind
by casing on points in the circle
and rewind
is the first function being applied,
so it would make sense to case on points in the circle.
In the case when the point is base
we can just give
the map we wanted to generalize in the first place.
Solution to Hint 0
windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind =
outOfS¹D (λ x → (n : helix x) → windingNumber x (rewind x n) ≡ n)
windingNumberRewindBase {!!}
Hint 1
Checking the last hole we see that we need to give a dependent path from
windingNumberRewindBase
to itself.
According to the definition of a dependent path,
this is just a path in the last fiber from pathToFun
of windingNumberRewindBase
to windingNumberRewindBase
(the fiber is (n : ℤ) → windingNumber base (rewind base n) ≡ n
).
Now this might seem very complicated :
even after applying functional extensionality (this is equality of two functions)
this would be “finding a path between paths in ℤ
”.
Try repeating that last bit in your head a couple of times.
Hint 2
We put a lot of effort into showing that ℤ
is a set.
Solution
windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind =  must case on x / use recursor / outOfS¹ since that is def of rewind
outOfS¹D (λ x → (n : helix x) → windingNumber x (rewind x n) ≡ n)
windingNumberRewindBase (
pathToFun
(λ i → (n : helix (loop i)) → windingNumber (loop i) (rewind (loop i) n) ≡ n)
windingNumberRewindBase
≡⟨ funExt (λ x → isSetℤ _ _ _ _ ) ⟩
windingNumberRewindBase ∎)
Part 2  rewind
is a left inverse
Try to show that rewind
is a left inverse.
The Statement
Just like we struggled to only define windingNumber base
without access to the entire circle,
we make sure to include all the data we have access to.
Note that this was not the case before.
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = {!!}
Hint 0
Remembering that windingNumber x p
is externally equal to endPt helix p 0
,
and that endPt
is defined by path induction  using J
(this is not exactly true for endPt
from the library for cubical
reasons),
the obvious thing to do here is to do path induction.
Solution for Hint 0
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p) {!!}
Hint 1
It suffices to show that rewind x (windingNumber x refl) ≡ refl
,
which by reducing the left side is the same as showing
loop_times (endPt helix refl 0) ≡ refl
.
Solution to Hint 1
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))
≡⟨ {!!} ⟩
refl ∎)
Hint 2
We know what endPt
does to refl
, which is given by the result endPtRefl
.
If you need to recall what endPtRefl
proves you can type it into the hole
and do Cc C.
for the goal and the type of endPtRefl
.
Solution to Hint 2
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))
≡⟨ cong loop_times (cong (λ g → g (pos zero)) (endPtRefl {x = base} helix)) ⟩
loop (pos zero) times
≡⟨ {!!} ⟩
refl ∎)
Solution
The last step is simply remembering how loop_times
computes.
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))  reduce both definitions
≡⟨ cong loop_times (cong (λ g → g (pos zero)) (endPtRefl {x = base} helix)) ⟩
loop (pos zero) times
≡⟨ refl ⟩
refl ∎)
Part 3  The Loop Space is ℤ
We can conclude our main goal now, by collecting all of the components we have made above. We leave you the pleasure.
Solution
As usual we construct an isomorphism,
but we can choose to do this over the entire circle
or just between loopSpace S¹ base
and ℤ
.
We do the former and have the latter as a corollary,
but you could just do the latter directly as well.
pathFibration≡helix : (x : S¹) → (base ≡ x) ≡ helix x
pathFibration≡helix x =
isoToPath (iso (windingNumber x) (rewind x) (windingNumberRewind x) (rewindWindingNumber x))
loopSpaceS¹≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpaceS¹≡ℤ = pathFibration≡helix base
What now?
We have mentioned already that we aren’t exactly working with the fundamental group, but the loop space. In the final quest of this arc we discuss the definition of the fundamental group and show that the loop space in this case is the fundamental group already.