TO DO.md

We'll start working on this bit:

1. 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
2. More modular arithmetic?
3. Cycle decomposition
   • Random permutations
4. More geometries: Affine, Projective, Similarity, etc.

Done:

1. Mathematical objects and constructions
   • types, Σ, Π, =, U, ℕ, Fin, ×, →
   • constructions, pair, λ, idp, 0, successor, etc.
   • equivalences, h-levels, truncation, propositions, sets
   • logic, ∧, ∨, ∃, ∀, →
2. Group theory
   • 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