Categorica is an experimental proof engine for category theory, inspired by automated theorem provers like Vampire but focused on categorical structures. It provides a kernel for reasoning about categories, functors, and universal constructions using equational logic and saturation techniques.

• Category-theoretic reasoning kernel
  A lightweight core for modeling categories, objects, morphisms, and their equations.

• Equational logic & automated proof search
  Built on equational reasoning with normalization and saturation, aiming toward superposition and e-graph backends.

• Multi-category support
  Work with many categories at once, while keeping category boundaries explicit and safe.

• Universal properties as rules
  Extendable with constructions like products, pullbacks, equalizers, and their ∀∃! axioms.

• Extensible architecture
  Functors and natural transformations are layered as capabilities, enabling both symbolic and concrete interpretations.

• Interactive exploration
  Designed to support user feedback loops: suggest missing constructions, materialize witnesses, or inspect goals interactively.

TBD

TBD

TBD

Categorica is a (early) work in progress. The current kernel supports typed morphisms, category-local constraints, and normalization-based goal checking. The next milestones include unification, superposition, and an e-graph backend for scalable equational reasoning.