Skip to main content

All Questions

20 votes
1 answer
313 views

Examples of formalisation of abelian categories

The question I would be interested to hear about examples of formalisation of the theory of abelian categories in theorem provers, and in particular formalisations of things like the zig-zag lemma and ...
Kevin Buzzard's user avatar
20 votes
0 answers
275 views

Can we automatically get around set-theoretic difficulties?

One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
Wojowu's user avatar
  • 1,058