Category Archives: Type theory
Induction on equality
In type theory, equality has a definition, and basic facts about it such as symmetry and transitivity can be proved from more fundamental principles. Continue reading
Induction, and inductive types.
Induction in Lean isn’t just something which you do on natural numbers. Continue reading
Thoughts on the Pythagorean theorem
Pythagoras’ theorem says that a square is equal to two squares. What does equality mean here? Continue reading
Division by zero in type theory: a FAQ
How can a theorem prover use the convention that 1/0=0 and still be consistent? Continue reading
Equality, specifications, and implementations
There are lots of kinds of equalities in Lean. Here’s some basic things that a mathematician needs to know to understand what’s going on Continue reading
Teaching dependent type theory to 4 year olds via mathematics
What is the number before 0? Who cares! How do children model numbers? An experiment with type theory. Continue reading
Mathematics in type theory.
An explanation of how to set up mathematics using universes, types, and terms Continue reading
The Sphere Eversion Project
Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading
The invisible map
Is a subgroup of a group a group? Is 3 a topology on 2? Is a natural number a real number? Decisions like this have consequences. Continue reading
Xena 