Update README.md

This commit is contained in:
jlh 2021-09-22 09:52:41 +01:00 committed by GitHub
parent 3c7d924b86
commit df5d7c381b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -43,26 +43,29 @@ Try opening `Trinitarianism/Quest0.agda` in Emacs
and do `Ctrl-c Ctrl-l`.
Some text should be highlighted, and any `?` should turn into `{ }`.
## How the game works
## Where to start?
Our Game is currently under development.
As of now you can try the _quests_ in the `Trinitarianism` folder.
Each quest consists of three files, for example :
- `Trinitarianism/Quest0.md` is the guide for the quest.
In there, you will find details of the tasks
you must finish in order to complete the quest.
For now, it is recommended that
you view these online within github.
- `Trinitarianism/Quest0.agda` is the agda file in which
you do the quest.
- `Trinitarianism/Quest0Solutions.agda` contains
solutions to the tasks in the quest.
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 ``.
## Emacs and Agda usage
We have a file with a list of [basic Emacs commands](
## 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
),
but you _should_ be able to learn how to use Agda as you go along.
## Feedback
If you have any feedback please contact the devs.
).