Tag Archives: equality

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

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

Counting binary relations: an apology

OK so this is really just another equality post. And an apology to the Imperial 1st years for teaching them badly. Let’s start with two questions. Q1) How many binary relations are there on a set with 2 elements? Q2) … Continue reading

Posted in Uncategorized | Tagged , , | 5 Comments

Equality part 3: canonical isomorphism.

I hadn’t planned on writing a third equality post, but my talk at Big Proof 2019 (see slides here) ended up having a huge section about “mathematician’s equality”, and I realised I had more to say about it. Here are … Continue reading

Posted in Uncategorized | Tagged , | 14 Comments

Equality part 2: syntactic equality

Syntactic equality is yet another kind of equality. I am beginning to learn why it matters. Continue reading

Posted in Learning Lean, tactics | Tagged , | Leave a comment

Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until … Continue reading

Posted in Learning Lean | Tagged , | 2 Comments