We'll start working on this bit:
- Introduction [motivating examples]
- Mathematical objects; no entity without identi(ty/fications)
- Geometry and algebra united via symmetry (Erlangen Program)
- Impossibility results: ruler+compass, root extraction
- Mathematical objects and constructions
- types, Σ, Π, =, U, ℕ, Fin, ×, →
- constructions, pair, λ, idp, 0, successor, etc.
- equivalences, h-levels, truncation, propositions, sets
- logic, ∧, ∨, ∃, ∀, →
- Groups
- structure of identity types
- automorphism 1-group = fundamental group (hint at higher groups)
- homomorphisms induced by functions (early)
- more examples: symmetric groups, integers, cyclic groups & modular arithmetic
- group actions, orbits and fixed points
- subgroups
- Cayley's theorem