diff --git a/EmacsCommands.md b/EmacsCommands.md deleted file mode 100644 index 099e8e5..0000000 --- a/EmacsCommands.md +++ /dev/null @@ -1,47 +0,0 @@ -Useful Doom Emacs Commands -===================== - -## Notation - -- `SPC` means space bar -- `C-` means hold down `Ctrl` -- `M-` means hold down `Alt` for non-Macs and `Option` for Macs -- `S-` means hold down `Shift` -- `RET` means enter - -Example `C-c C-l` in Agda files is `Ctrl-c`, let go, `Ctrl-l` - -## General Doom Emacs usage - -The 'ambient mode' is called __evil mode_ and follows -vim-like bindings. -The following commands are for _evil mode_: - -- `SPC h b b` to look for bindings -- `SPC f f` to find files. can use `TAB` for auto-completing paths -- `h j k l` for left down up right -- `SPC b k` to kill 'buffers' -- `i` to go into __insert mode_ (in insert mode you can insert text) - and `ESC` or `C-g` to go back to _evil mode_. -- `C-_` to undo - -For beta users, to get the latest patch - -- do `SPC g g` for "git status" -- then `F` for pull (whilst in "git status") - - -## Agda usage - -To insert text in the `agda` file use `i` to enter _insert mode_. - -- `C-c C-l` loads the file -- `C-c C-,` checks goal of the hole your cursor is in. -- `C-c C-SPC` fills hole your cursor is in. -- `C-c C-r` refines the hole your cursor is in. -- `C-c C-c` does cases on terms in the hole your cursor is in. -- `C-c C-d` used for checking types of terms -- `C-c C-n` used for 'reducing' terms to their 'simplest form' -- `C-c C-.` does `C-c C-,` and `C-c C-d` -- `M-SPC c d` looks up the definition of the thing you are hovering over. - diff --git a/Plan.org b/Plan.org deleted file mode 100644 index b37660a..0000000 --- a/Plan.org +++ /dev/null @@ -1,117 +0,0 @@ -#+OPTIONS: num:nil -#+AUTHOR: JLH -#+AUTHOR: KL - -* Planning The HoTT Game - -** Aims of the HoTT Game - - To get mathematicians with no experience in proof verification interested in HoTT and able to use Agda for HoTT - - Big-ass-boss: Loop space of S^1 = Z - - Try to balance hiding cubical implementations whilst exploiting their advantages - -** Barriers - - HOLD Installation of emacs - - TODO Usage of emacs - - TODO General type theoretic foundations - - TODO Cubical type theory - -** Format - - [?] Everything done in .agda files - - Partially written code with spaces for participants to fill in + answer files - - Levels set out with mini-bosses like in Nat Num Game, but with an overall boss - - [?] Side quests - - References to Harper lectures and HoTT book - -** Content -# listing topics we have pursued, NO ordering - -- emacs usage -- agda usage - + basic commands (all covered in https://agda.readthedocs.io/en/v2.6.0.1/getting-started/quick-guide.html) - + recommend doom emacs - + implicit/explicit arguments - + holes and inferred types - + =_+_= vs =plus__= -- type theory basics - + meta (judgemental/definitional) equality vs internal (propositional) equality - - function extensionality - + type formation - - inductive types - + (side Q) positive and negative constructions of Pi/Sigma types - + =data= and =record= - + universes - + recursors / pattern matching - + (side Q) some natural number exercises as early evidence of being able to 'do maths'? - + different notions of equivalence - - fibers contractable - - quasi-inverse - - zig-zag - + (side Q) types are infinity groupoids - + extra paths (univalence, fun ext, HITs) -- HoTT - + basics - - meta interval, identity type vs path type - + mention identity type for compatability with other sources, but just use path type - - path type on other types - - dependent path type PathP vs path over - - univalence - - the (non)-issue of J in (Cu)TT - - =isContr, isProp, isSet= - - drawing pictures - + Structures, using univalence to transport - - transporting results between isomorphic structures - + HITs, examples - - the constructed interval - - booleans and covers - - =S^n= - - =S^1= with 2 cw structures equiv - + Homotopy n-types - - homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT - + in particular sigma types - -** Debriefs -- 2021 July 15; Homotopy n-types - + watched (Harper) lecture 15 on Sets being closed under type formations ->- motivates showing in Agda Sets closed under Sigma. - + Harper does product case, claiming sigma case follows analogously, - + attempt proof in Cubical Agda but highly non-obvious how to use that fibers are Sets. - + difficulty is that PathP not in one fiber, but PathOver is, AND PathOver <-> PathP NON-obvious - + Easy to generalize situation to n-types being closed under Sigma (7.1.8 in HoTT book), we showed this assuming PathPIsoPath - -** Mixolydian Bosses - -+ universe classifies bundles - -** SuperUltraMegaHyperLydianBosses -+ natural number object unique and `_+_` unique on any nat num obj - + nat num obj unique - + `_+_` unique on a model of nat num obj - - axiomatize addition on naturals - - naturals is a set - - fun extensionality - - contractability - - propositions - - propositions closed under sigma types - + univalence - -** Top 100 (set theoretic) misconceptions about type theory -+ Propositions -+ Proof relevance -+ Propositions are _inside the theory_ -+ Membership not the same as : - + typing is unique (doesn't make sense to intersect two types) - + -+ Though set theory had fewer axioms type theory's assumptions are - more intuitive (hence intionistic type theory). - There is no fiddling about with membership to construct things - e.g. cartesian product -+ 'we cannot use LEM' ~ not assuming law of excluded middle _globally_ means - type theory theorems are stronger! - -** Fundamental group of S1 -+ def of S¹ -+ a bunch of stuff about ℤ -+ isoToPath to make ℤ ≡ ℤ -+ subst -+ funExt -+ set-truncation -+ paths as equality diff --git a/README.md b/README.md deleted file mode 100644 index 16a01c2..0000000 --- a/README.md +++ /dev/null @@ -1,71 +0,0 @@ -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. - -## Installing Agda and the Cubical Agda library - -Our Game is in Agda, which can be installed following instructions -[on their site]( -https://agda.readthedocs.io/en/latest/getting-started/installation.html). -It is recommended that you use Agda in the text editor -[emacs]( -https://www.gnu.org/software/emacs/tour/index.html), -in particular -[Doom Emacs](https://github.com/hlissner/doom-emacs), -if you can't be bothered to do a bunch of configuration. - -Once you have Emacs and Agda, get the [Cubical Library]( -https://github.com/agda/cubical) (version 0.3) -and make sure Agda knows where your cubical library is -by following instructions on the [library management page]( -https://agda.readthedocs.io/en/latest/tools/package-system.html?highlight=library%20management). -In short: locate (or create) your `libraries` file and add a line -``` -the-directory/cubical.agda-lib -``` -to it, where `the-directory` is the location of `cubical.agda-lib` on your computer. - -Get the HoTT Game by [cloning this repository]( -https://git-scm.com/book/en/v2/Git-Basics-Getting-a-Git-Repository) -into a folder and then making sure that Agda knows where the HoTT Game is -by adding a line -``` -the-directory/HoTTGameLib.agda -``` -to your `libraries` file as above. - -Try opening `Trinitarianism/Quest0.agda` in Emacs -and do `Ctrl-c Ctrl-l`. -Some text should be highlighted, and any `?` should turn into `{ }`. - -## Where to start? - -You can start with `0Trinitarianism` 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 `1FundamentalGroup` where we show that the -fundamental group of `S¹` is `ℤ`. - -## How to start? - -To start with `1FundamentalGroup` (for example), -find the GitHub page [`1FundamentalGroup/Quest0Part0.md`]( -https://github.com/thehottgame/TheHoTTGame/blob/main/1FundamentalGroup/Quest0Part0.md -) -and follow the instructions there, -then trying the following files in the same directory. -Open up the corresponding `.agda` file in `emacs` to -follow along with the instructions in the quests. - -## Emacs issues - -If you can't figure out `emacs` or forget some command, then -try consulting our guide for [basic Emacs commands]( -https://github.com/thehottgame/TheHoTTGame/blob/main/EmacsCommands.md -). diff --git a/README.rst b/README.rst new file mode 100644 index 0000000..275324c --- /dev/null +++ b/README.rst @@ -0,0 +1,16 @@ +.. _theHoTTGame: + +************* +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. + +For instructions on how to get started with the HoTT Game, +visit +`this page `_.