# 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