md files removed and README.rst added
This commit is contained in:
Jlh18
parent
31d9f67af6
commit
d0dd1d79f1
@ -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.
|
|
||||||
|
|
||||||
117
Plan.org
117
Plan.org
@ -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
|
|
||||||
71
README.md
71
README.md
@ -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
|
|
||||||
).
|
|
||||||
16
README.rst
Normal file
16
README.rst
Normal file
@ -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 <https://agda.readthedocs.io/en/v2.6.0/language/cubical.html>`_
|
||||||
|
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 <https://findtherightpath.readthedocs.io/en/latest/>`_.
|
||||||
Loading…
Reference in New Issue
Block a user