118 lines
4.0 KiB
Org Mode
118 lines
4.0 KiB
Org Mode
#+OPTIONS: num:nil
|
||
#+AUTHOR: JLH
|
||
#+AUTHOR: KL
|
||
|
||
* 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
|
||
# 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 + 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!
|
||
|
||
** Fundamental group of S1
|
||
+ def of S¹
|
||
+ a bunch of stuff about ℤ
|
||
+ isoToPath to make ℤ ≡ ℤ
|
||
+ subst
|
||
+ funExt
|
||
+ set-truncation
|
||
+ paths as equality
|