Kitcat

An experiment with univalent programming and open source mathematics in cubical Agda.

WIP — API is unstable. Expect breaking changes.

Contents

Kitcat is a research library at the intersection of higher category theory, homotopy type theory, and programming language foundations, written in Cubical Agda. It is a testbed for new ideas in these areas, a reference for formalized mathematics and type theory with machine-checked proof as its standard of evidence. In many aspects it is my personal playground and blackboard for exploring the design space of univalent type theory and higher category theory, and I hope it will be useful to downstream researchers and practitioners in these areas as well.

Foundations

The category theory framework is built on a confluence of ideas from:

• Capriotti-Kraus
• Chen
• Petrakis and
• Sterling's virtual bicategory theory & (reflexive graph lenses)
• among other references (see: resources directory)

Acknowledgments

The primary HoTT reference used throughout is Rijke's Introduction to Homotopy Type Theory, which we take as our standard reference for identifiers and structural organization of the theory whenever possible.

While many lemmas are original (I've rewritten the Core library several times in the course of development), Kitcat has adapted or otherwise drawn upon code from the following projects, which are exemplars of open source mathematics and deserve ample credit for their contributions to the foudnational corpus of formalized Homotopy Type Theory and Univalent Foundations. They are excellent, go look at them.

• 1lab (Amélia Liao et al., AGPL-3.0) — Definitions and proofs across Core.Function.Embedding, Core.HLevel, Core.Trait.Trunc, Core.Data.Fin, Core.Path, and Core.Transport.Properties are derived from or influenced by 1lab's formalizations
• TypeTopology (Martín Escardó et al., GPL-3.0) — Core.Function.Partial adapts the lifting monad from Lifting.Construction/Lifting.Monad; Core.Retract follows UF.Retracts; Core.Discrete follows UF.DiscreteAndSeparated; and Core.Function.Embedding adapts UF.LeftCancellable

Related work not otherwise mentioned

• agda-unimath — Univalent foundations at scale, a lovely reference, and one with considerable involvement from the author of the aforementioned Intro to HoTT textbook.
• agda-categories — Category theory library for Agda

LLM policy (updated 2026-07-09)

See llm-policy for my statement on the use of generative LLMs in this project.