germax26/TheHoTTGame
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
c35e360247
TheHoTTGame/Plan.org
jlh 2735e5623b Edits to windows installation guide
2021-08-11 17:16:07 +01:00

3.2 KiB
Raw Blame History

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

  • 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

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