TheHoTTGame/Plan.org

• Planning The HoTT Game
  • Aims of the HoTT Game
  • Barriers
  • Format
  • Content
  • Debriefs
  • Mixolydian Bosses
  • SuperUltraMegaHyperLydianBosses
  • Top 100 (set theoretic) misconceptions about type theory

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

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