Maths - Category Theory - Equality

Category theory usually only takes equality upto isomorphism.

Here it might be interesting to work out if we can use pullbacks to represent definitional equality.

see these pages:


pullback diagram

To explain this, imagine we have a set with three elements: 1,2 and 3.

To find the equalities take all 9 combinations as tuples (that is, take product with itself).

The ones where the left and right parts of the tuple are equal are the ones where this diagram commutes. That is <1,1> , <2,2> and <3,3>.

pullback diagram

Can this thinking be extended to isomorphism instead of equality?

And can this be extended to Leibniz equality?

That is, can we include proofs in this framework?

leibniz equality diagram

Discussed more on these pages:

metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.