# 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

Posted in M1F, M40001, Type theory, undergrad maths | Tagged , | 8 Comments

## Induction, and inductive types.

Induction in Lean isn’t just something which you do on natural numbers. Continue reading

Posted in Learning Lean, Type theory | Tagged , | 9 Comments

## 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

Posted in Learning Lean, M1F, M40001, Type theory, undergrad maths | Tagged , | 12 Comments

## 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

Posted in Algebraic Geometry, General, Type theory | Tagged , , | 6 Comments

## 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

| Tagged , , | 8 Comments

## Mathematics in type theory.

An explanation of how to set up mathematics using universes, types, and terms Continue reading

Posted in Learning Lean, Type theory, undergrad maths | Tagged , , , | 26 Comments

## The Sphere Eversion Project

Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading

Posted in Imperial, Learning Lean, Type theory | | 2 Comments

## 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