Skip to main content
2 of 7
add another formalization
Jason Gross
  • 695
  • 1
  • 8
  • 17

Formalizations of category theory in proof assistants

What are the existing formalizations of category theory in proof assistants?

The ones I know about are:

I also know about the following papers about formalizing category theory in proof assistants:

I'm primarily interested in public-domain code implementing category theory in a proof assistant, though I'm also interested in papers about formalizations of category theory in proof assistants.

Jason Gross
  • 695
  • 1
  • 8
  • 17