A comprehensive and searchable database of categorical structures and their properties

CatDat provides a growing collection of categorical structures such as categories, functors, and morphisms. Built by and for those who love category theory.

Structures

Browse a comprehensive collection of categorical structures, including categories and functors, each with detailed descriptions, proofs of their properties, and related structures.

Properties

Browse properties of categorical structures, including category properties and functor properties, each with relevant results, structures satisfying or not satisfying the property, and related properties.

Deduction System

Implications between properties of categorical structures, including category implications and functor implications, power a deduction system that automatically infers satisfied and unsatisfied properties.

Search by properties

Search for categorical structures such as categories or functors satisfying specific properties while not satisfying others. Inconsistent property combinations are detected.

Compare structures

Compare categorical structures such as categories or functors to identify similarities and differences in their properties.