19
votes
32answers
1k 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, ...
5
votes
3answers
655 views

Proof formalization

I read some time ago some papers about proof formalization. Typically, I began whith this one, from Lamport. Are there more recent works in this field ?