diff --git a/.markdown-preview.html b/.markdown-preview.html deleted file mode 100644 index b9fc048..0000000 --- a/.markdown-preview.html +++ /dev/null @@ -1,41 +0,0 @@ - - - - - - Markdown preview - - - - - - -
-

Markdown preview

-
- - diff --git a/HoTTGame.agda-lib b/HoTTGameLib.agda-lib similarity index 100% rename from HoTTGame.agda-lib rename to HoTTGameLib.agda-lib diff --git a/Plan.html b/Plan.html deleted file mode 100644 index 2cacc26..0000000 --- a/Plan.html +++ /dev/null @@ -1,377 +0,0 @@ - - - - - - - -‎ - - - - - - -
-
-

Table of Contents

-
- -
-
- -
-

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
    • -
  • [?] Work towards showing an interesting result in HoTT
    • -
  • 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

-
-
    -
  • emacs usage
    • -
  • agda usage -
    • -
  • 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 -
        -
      1. fibers contractable
        2. -
      2. quasi-inverse
        3. -
      3. zig-zag
        4. -
      • -
    • (side Q) types are infinity groupoids
      • -
    • extra paths (univalence, fun ext, HITs)
      • -
    • -
  • HoTT -
      -
    • basics -
        -
      1. meta interval, identity type vs path type -
          -
        • mention identity type for compatability with other sources, but just use path type
          • -
        2. -
      2. path type on other types
        3. -
      3. dependent path type PathP vs path over
        4. -
      4. univalence
        5. -
      5. the (non)-issue of J in (Cu)TT
        6. -
      6. isContr, isProp, isSet
        7. -
      7. drawing pictures
        8. -
      • -
    • Structures, using univalence to transport -
        -
      1. transporting results between isomorphic structures
        2. -
      • -
    • HITs, examples -
        -
      1. the constructed interval
        2. -
      2. booleans and covers
        3. -
      3. Sn
        4. -
      4. S1 with 2 cw structures equiv
        5. -
      • -
    • Homotopy n-types -
        -
      1. homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT -
          -
        • in particular sigma types
          • -
        2. -
      • -
    • -
-
-
- -
-

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
      • -
    • -
-
-
-
-
-
-

Author: JLH KL

-

Created: 2021-07-19 Mon 18:31

-
- - diff --git a/Plan.md b/Plan.md deleted file mode 100644 index 618c840..0000000 --- a/Plan.md +++ /dev/null @@ -1,107 +0,0 @@ - -# Table of Contents - -- [Planning The HoTT Game](#org3bb90ed) - - [Aims of the HoTT Game](#orga8d795d) - - [Barriers](#org122a1d0) - - [Format](#org3ea389f) - - [Content](#org70d2231) - - [Debriefs](#org37fbeb9) - - - - - -# 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 -- [?] Work towards showing an interesting result in HoTT -- 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 - -- emacs usage -- agda usage - - basic commands (all covered in ) - - 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 - 1. fibers contractable - 2. quasi-inverse - 3. zig-zag - - (side Q) types are infinity groupoids - - extra paths (univalence, fun ext, HITs) -- HoTT - - basics - 1. meta interval, identity type vs path type - - mention identity type for compatability with other sources, but just use path type - 2. path type on other types - 3. dependent path type PathP vs path over - 4. univalence - 5. the (non)-issue of J in (Cu)TT - 6. isContr, isProp, isSet - 7. drawing pictures - - Structures, using univalence to transport - 1. transporting results between isomorphic structures - - HITs, examples - 1. the constructed interval - 2. booleans and covers - 3. Sn - 4. S1 with 2 cw structures equiv - - Homotopy n-types - 1. 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 - diff --git a/Plan.org b/Plan.org index db5fa59..7f1435a 100644 --- a/Plan.org +++ b/Plan.org @@ -27,52 +27,52 @@ - 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__~ + + 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 + + meta (judgemental/definitional) equality vs internal (propositional) equality - function extensionality - - type formation + + 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 - a) fibers contractable - b) quasi-inverse - c) zig-zag - - (side Q) types are infinity groupoids - - extra paths (univalence, fun ext, HITs) + + (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 - a) meta interval, identity type vs path type - - mention identity type for compatability with other sources, but just use path type - b) path type on other types - c) dependent path type PathP vs path over - d) univalence - e) the (non)-issue of J in (Cu)TT - f) isContr, isProp, isSet - g) drawing pictures - - Structures, using univalence to transport - a) transporting results between isomorphic structures - - HITs, examples - a) the constructed interval - b) booleans and covers - c) S^n - d) S^1 with 2 cw structures equiv - - Homotopy n-types - a) homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT - * in particular sigma types + + 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 + + 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 diff --git a/README.md b/README.md new file mode 100644 index 0000000..b01edbc --- /dev/null +++ b/README.md @@ -0,0 +1,56 @@ +The HoTT Game +============= + +The Homotopy Type Theory (HoTT) Game is a project aimed at +introducing mathematicians with no experience +in proof verification interested in HoTT and able to use Agda for HoTT. +This guide 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) is a bit nicer 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 up `Trinitarianism/AsProps/Quest0.agda` in Emacs +and do `Ctrl-c Ctrl-l`. +Some text should be highlighted, and any `?` should turn into `{ }`. + +## How the game works + +Our Game is currently under development. Please contact the devs. +Currently you can try `Trinitarianism/AsProps/Quest0.agda`, +making use of the accompanying solutions Agda file. + +## Emacs and Agda usage +We have a file with a list of basic Emacs commands and +you _should_ be able to learn how to use Agda as you go along. + +## Feedback +If you have any feedback please contact the devs. diff --git a/Trinitarianism/AsCats.agda b/Trinitarianism/AsCats.agda index 9ce79bb..92f7ac6 100644 --- a/Trinitarianism/AsCats.agda +++ b/Trinitarianism/AsCats.agda @@ -1,4 +1,4 @@ -module TheHoTTGame.Trinitarianism.AsCats where +module Trinitarianism.AsCats where {- Here are some things that we could like to have in a category diff --git a/Trinitarianism/AsProps/Quest0.agda b/Trinitarianism/AsProps/Quest0.agda index 2853084..d0ecb38 100644 --- a/Trinitarianism/AsProps/Quest0.agda +++ b/Trinitarianism/AsProps/Quest0.agda @@ -1,5 +1,5 @@ -module TheHoTTGame.Trinitarianism.AsProps.Quest0 where -open import TheHoTTGame.Trinitarianism.AsProps.Quest0Preamble +module Trinitarianism.AsProps.Quest0 where +open import Trinitarianism.AsProps.Quest0Preamble {- Here are some things that we could like to have in a logical framework diff --git a/Trinitarianism/AsProps/Quest0Preamble.agda b/Trinitarianism/AsProps/Quest0Preamble.agda index c2fb7b2..6a0a871 100644 --- a/Trinitarianism/AsProps/Quest0Preamble.agda +++ b/Trinitarianism/AsProps/Quest0Preamble.agda @@ -1,5 +1,5 @@ -module TheHoTTGame.Trinitarianism.AsProps.Quest0Preamble where +module Trinitarianism.AsProps.Quest0Preamble where open import Cubical.Core.Everything hiding (_∨_) public open import Cubical.Data.Nat public diff --git a/Trinitarianism/AsProps/Quest0Solutions.agda b/Trinitarianism/AsProps/Quest0Solutions.agda index 573bff9..9771bb0 100644 --- a/Trinitarianism/AsProps/Quest0Solutions.agda +++ b/Trinitarianism/AsProps/Quest0Solutions.agda @@ -1,5 +1,5 @@ -module TheHoTTGame.Trinitarianism.AsProps.Quest0Solutions where -open import TheHoTTGame.Trinitarianism.AsProps.Quest0Preamble +module Trinitarianism.AsProps.Quest0Solutions where +open import Trinitarianism.AsProps.Quest0Preamble data ⊤ : Prop where trivial : ⊤ diff --git a/Trinitarianism/AsProps/Quest1.agda b/Trinitarianism/AsProps/Quest1.agda index e69de29..dc3632b 100644 --- a/Trinitarianism/AsProps/Quest1.agda +++ b/Trinitarianism/AsProps/Quest1.agda @@ -0,0 +1,13 @@ +{- +Two things being equal is also a proposition + +-} + + + + +-- FalseToTrue : ⊥ → ⊤ +-- FalseToTrue = λ x → trivial + +-- FalseToTrue' : ⊥ → ⊤ +-- FalseToTrue' () diff --git a/Trinitarianism/AsProps/Trash/Qust0.agda b/Trinitarianism/AsProps/Trash/Qust0.agda deleted file mode 100644 index 636bf99..0000000 --- a/Trinitarianism/AsProps/Trash/Qust0.agda +++ /dev/null @@ -1,31 +0,0 @@ -{- This says that ⊥ is the proposition where there are no proofs of it. -} - -{- -Given two propositions P and Q, we can form a new proposition 'P implies Q' -written P → Q -To introduce a proof of P → Q we assume a proof x of P and give a proof y of Q - -Here is an example demonstrating → in action --} --- TrueToTrue : ⊤ → ⊤ --- TrueToTrue = ? - -{- - * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document, - and now you can fill the holes - * press C-c C-r and agda will try to help you, - * you should see λ x → { } - * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward) - * to check what agda wants in the hole use C-c C-, - * the Goal area should look like - Goal: ⊤ - ———————————————————————————————————————————————————————————— - x : ⊤ - - * this means you have a proof x : ⊤ and you need to give a proof of ⊤ - * you can now give it a proof of ⊤ and press C-c C-SPC to fill the hole - - There is more than one proof (see answers) - are they the same? --} - --- solutions: diff --git a/Trinitarianism/AsProps2.agda b/Trinitarianism/AsProps2.agda deleted file mode 100644 index dc3632b..0000000 --- a/Trinitarianism/AsProps2.agda +++ /dev/null @@ -1,13 +0,0 @@ -{- -Two things being equal is also a proposition - --} - - - - --- FalseToTrue : ⊥ → ⊤ --- FalseToTrue = λ x → trivial - --- FalseToTrue' : ⊥ → ⊤ --- FalseToTrue' () diff --git a/_build/2.6.2/agda/Trinitarianism/AsCats.agdai b/_build/2.6.2/agda/Trinitarianism/AsCats.agdai new file mode 100644 index 0000000..ab957bf Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/AsCats.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/AsProps/Quest0Preamble.agdai b/_build/2.6.2/agda/Trinitarianism/AsProps/Quest0Preamble.agdai new file mode 100644 index 0000000..913d317 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/AsProps/Quest0Preamble.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/AsProps/Quest0Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/AsProps/Quest0Solutions.agdai new file mode 100644 index 0000000..795a1ce Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/AsProps/Quest0Solutions.agdai differ