nLab CatDat

This page records the project

  • CatDatA comprehensive database of categories and their properties, catdat.app.

It has been initiated by Martin Brandenburg and welcomes contributions by the community.

Features

  • Types of Categorical Structures: Supports categories, functors, and morphisms.
  • Structure Detail Pages: Each categorical structure has a dedicated page with its definition, satisfied and unsatisfied properties, and related structures.
  • Property Detail Pages: Explore the definition of a property and view categorical structures that satisfy it and those that don’t.
  • Proofs and References: Each property and implication includes a proof or reference, forming a data-driven knowledge base for category theory.
  • Deduction System: Automatically infers properties of categorical structures from existing ones using a database of implications.
  • Automatic Dualization: Automatically dualizes implications and property assignments.
  • Searchable Database: Find categorical structures based on satisfied properties and unsatisfied properties.
  • Comparison Feature: Compare multiple categorical structures to identify their differences and similarities.

Example pages

category: reference

Last revised on August 12, 2026 at 20:54:10. See the history of this page for a list of all contributions to it.