The agda-unimath library

Categories parametrized by morphism equality, in Agda

A formalization of category theory in cubical Agda

Category theory formalized in cubical agda

Bicategories of automata, completeness of F-automata in monoidal categories, adjoints between (semi)bicategories; https://arxiv.org/pdf/2303.03867, https://arxiv.org/pdf/2303.03865, https://arxiv.org/abs/2305.00272

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda

A categorical semantics library in Agda.

Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.

Mechanized classifications of 2-groups

Agda formalization for the POPL 2026 paper "Di- is for Directed: First-Order Directed Type Theory via Dinaturality".

Code for Category theory applied to functional programming

Categorical semantics of counterpart-based quantified (linear) temporal logics in Agda using agda-categories

Espèces généralisées de structures sur les groupoïdes

Formal proofs related to coslice colimits and 2-coherent left adjoints

Categorical Abstract Machine: Theory, Formalisation, Extensions

Homotopy Type Theory and categorical algebra experiments in the style of UniMath

Mirror of https://git8.cs.fau.de/software/initial-algebras-unchained

2022 AMS MRC on Applied Category Theory.

WIP: Reedy fibrant diagrams in models of type theory

Formalization of topics in mathematics and computer science