All Questions
1 question
43
votes
36
answers
6k
views
Formalizations of category theory in proof assistants
What are the existing formalizations of category theory in proof assistants?
I'm primarily interested in public-domain code implementing category theory in a proof assistant (Coq, Agda, Isabelle/HOL, ...