#+TITLE: 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
#+DESCRIPTION: listing topics we have pursued, NO ordering
+ emacs usage
  - `data` and `record`
  - 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
  - constructing types in universes
  - universes
  - recursors / pattern matching
  - side quest: 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
  - types are infinity groupoids
  - positive and negative constructions of Pi/Sigma types
+ HoTT
  - basics
    a) meta interval, identity type vs 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
  - 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