Kitcat is an experimental library for Cubical Agda centered on general purpose programming, whose underpinnings lie in a theory of virtual categorical structures formalized in univalent foundations, which guides the overall design and implementation of the library. This is an active research project intended as a vehicle for exploring applied univalent mathematics while pinning down useful abstractions intended to be useful to Agda hackers of all stripes.

WIP — The API is not yet stable. Expect breaking changes.

Kitcat is not a formalization library in the style of agda-categories or 1lab. Its focus is on providing an opinionated foundation for programming with categorical abstractions, with an emphasis on usability.

The library aims to provide ergonomic interfaces for both programming and formalization: functors, natural transformations, limits, adjunctions, monads — built on a modular virtual category theory framework intended to serve as a cohesive API throughout. Quality of life features and metaprogramming facilities are planned where they make sense.

Research branches may appear in alternative tags. Thin-cloning recommended.

The library explores a presentation of univalent type theory and higher category theory formalization drawing on Capriotti–Kraus's prior work formalizing Univalent higher categories and ∞-categorical models of HoTT, Petrakis's univalent typoids, and Sterling's virtual bicategory theory and reflexive graph lenses.

The core abstraction is the virtual graph: a graph with 2-cells satisfying a propositional contractibility condition on composites, which generalizes but is trivially satisfied by the native ∞-groupoid structure of types. Research is ongoing, but early results seem promising that this provides a suitable setting for synthetic higher category theory.

• 1lab — Formalised mathematics as explorable reference
• agda-unimath — Systematic univalent foundations at scale
• agda-categories — Mature category theory for the Agda ecosystem