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

Markdown preview

+
+ + diff --git a/.projectile b/.projectile new file mode 100644 index 0000000..e69de29 diff --git a/HoTTGame.agda-lib b/HoTTGame.agda-lib new file mode 100644 index 0000000..7702b7c --- /dev/null +++ b/HoTTGame.agda-lib @@ -0,0 +1,4 @@ +name: HoTTGameLib +include: . +depend: cubical-0.3 +flags: --cubical --no-import-sorts diff --git a/Plan.html b/Plan.html new file mode 100644 index 0000000..2cacc26 --- /dev/null +++ b/Plan.html @@ -0,0 +1,377 @@ + + + + + + + +‎ + + + + + + +
+
+

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 index a51c354..251d3bd 100644 --- a/Plan.md +++ b/Plan.md @@ -1,72 +1,119 @@ -# 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 +# Table of Contents -## Barriers -- HOLD Installation of emacs -- TODO Usage of emacs -- TODO General type theoretic foundations -- TODO Cubical type theory +1. [Aims of the HoTT Game](#org45da28b) + 1. [To get mathematicians with no experience in proof verification interested in HoTT and able to use Agda for HoTT](#org6c86aa4) + 2. [Work towards showing an interesting result in HoTT](#org5c370bf) + 3. [Try to balance hiding cubical implementations whilst exploiting their advantages](#org2cc236e) +2. [Barriers](#org483c28e) + 1. [Installation of emacs](#orgfaee064) + 2. [Usage of emacs](#org4ec8663) + 3. [General type theoretic foundations](#orgd6212c3) + 4. [Cubical type theory](#orgdb053bf) -## 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 https://agda.readthedocs.io/en/v2.6.0.1/getting-started/quick-guide.html) - - recommend doom emacs? -> basic doom usage and command differences with nude agda. - - implicit/explicit arguments - - holes and inferred types - - `_+_` and `plus__` -- type theory basics - - meta (judgemental/definitional) equality vs internal (propositional) equality - - function extensionality - - type formation - - 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 - - inductive types - - (side Q) positive and negative constructions of Pi/Sigma types - - `data` and `record` -- 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, univalence and transport - a) transporting results between isomorphic structures - - HITs, examples - a) the constructed interval - b) booleans and covers - c) S^n - d) - - Homotopy n-types - a) homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT - * in particular sigma types + + +# 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 + + + +- emacs usage +- agda usage + - basic commands (all covered in ) + - recommend doom emacs + - implicit/explicit arguments + - holes and inferred types + - \`\_+\_\` and \`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 + +- 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 -# 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 498bc5a..f36a5a8 100644 --- a/Plan.org +++ b/Plan.org @@ -1,32 +1,36 @@ -# Planning The HoTT Game +#+OPTIONS: num:nil +#+AUTHOR: JLH +#+AUTHOR: KL -## 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 +* Planning The HoTT Game -## Barriers -- HOLD Installation of emacs -- TODO Usage of emacs -- TODO General type theoretic foundations -- TODO Cubical type theory +** 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 -## 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 +** Barriers + - HOLD Installation of emacs + - TODO Usage of emacs + - TODO General type theoretic foundations + - TODO Cubical type theory -# Content - +** 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? -> basic doom usage and command differences with nude agda. + - recommend doom emacs - implicit/explicit arguments - holes and inferred types - - `_+_` and `plus__` + - src_elisp{(_+_)} and src_elisp{(plus__)} - type theory basics - meta (judgemental/definitional) equality vs internal (propositional) equality - function extensionality @@ -64,7 +68,7 @@ a) homotopy levels being closed under type constructions, in particular Set and ETT inside HoTT * in particular sigma types -# Debriefs +** 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,