# Tag Archives: induction

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