| ← Ch. 4: Tactics | Table of contents | Ch. 6: Groups → |
Before committing to Group’s definition in the next chapter, this short
chapter answers three questions a careful mathematician should already be
asking. Why does this book use plain structure instead of Lean’s class
mechanism, which is what Mathlib actually uses? What exactly is Type,
and does Group (α : Type) really quantify over all types, including
Group itself? And when two proofs both establish a = b, in what sense
are they “the same”? Skipping these would leave exactly the kind of
unstated assumption a demanding reader is trained to notice and question,
so they are addressed here, before Chapter 6 proceeds.
Learning objectives. By the end of this chapter, explain why this book
delays class in favor of structure, state the STLC typing rules and
why Type itself needs a universe hierarchy, and distinguish definitional
from propositional equality (and predict, correctly, when rfl alone
will and will not close a goal).
Sections
structureversusclass: why this book delays type classes- Universes:
Type,Type 1, and whyGroupisn’t aGroup - Typing rules and safety
- Definitional versus propositional equality
- Exercises
- Checkpoint project: a
Monoidfrom scratch
| ← Ch. 4: Tactics | Table of contents | Ch. 6: Groups → |