Formulation of category theory in Agda

smash product in Agda

This is a formalization of dialectica spaces.

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

Categorical Abstract Machine: Theory, Formalisation, Extensions

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

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

Code for Category theory applied to functional programming

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

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

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

A categorical semantics library in Agda.

Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in 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