An experiment with univalent programming and open source mathematics in cubical Agda.
WIP — API is unstable. Expect breaking changes.
Kitcat will be host to investigations at the intersection of higher catgegory theory, homotopy type theory, rewriting theory, combinatorics, and proof theory. The library is intended to be a testbed for new ideas in these areas, as well as a reference for formalized mathematics and an ergonomic environment for functional programming.
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
Kitcat incorporates and adapts code from the following projects:
- 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, andCore.Transport.Propertiesare derived from or influenced by 1lab's formalizations - TypeTopology (Martín
Escardó et al., GPL-3.0) —
Core.Function.Partialadapts the lifting monad fromLifting.Construction/Lifting.Monad;Core.Set.OmegafollowsUF.SubtypeClassifier;Core.RetractfollowsUF.Retracts;Core.DiscretefollowsUF.DiscreteAndSeparated; andCore.Function.EmbeddingadaptsUF.LeftCancellable - agda-prelude (Ulf Norell,
MIT) —
Core.Function.BaseandCore.Trait.Ordare adapted fromPrelude.Functionand the prelude's ordering conventions - TOTBWF's Segal conditions gist —
Lib.SSet.Base,Lib.SSet.Segal, andLib.CSet.Baseadapt the simplicial set and Segal condition definitions
The primary HoTT reference used throughout is Rijke's Introduction to Homotopy Type Theory.
- 1lab — Formalised mathematics as explorable reference, to whom this library is much indebted
- agda-unimath — Univalent foundations at scale
- agda-categories — Category theory library for Agda