CatDat

CatDat provides a growing collection of categorical structures such as categories and functors, each with detailed descriptions and properties. Built by and for those who love category theory.

https://catdat.app

Features

• Four types of categorical structures: Supports categories, functors, morphisms, and symmetric monoidal categories.
• 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 and unsatisfied properties.
• Comparison feature: Compare multiple categorical structures to identify their differences and similarities.
• Intuitive user interface: Usable on both mobile and desktop. Supports light/dark mode.

How to contribute

This project is a community effort. Whether you're a mathematician spotting missing data or a developer improving the interface, your contributions are welcome. See our contribution guidelines for details.

Documentation

• The database of CatDat
• Deployment
• Status page

Local setup

You need to have Git, Node.js and pnpm installed.

1. Fork ScriptRaccoon/CatDat on GitHub.
2. Clone your fork with git clone https://github.com/{your_username}/CatDat.git.
3. Change into the directory with cd CatDat.
4. Install dependencies with pnpm install.
5. Create the local database with pnpm db:setup.
6. Update the local database with pnpm db:update.
7. Start the local development server with pnpm dev.

Tech stack

Built with modern web technologies:

• Language: TypeScript
• Framework: SvelteKit 3
• Database: SQLite
• Deployment: Netlify
• Math rendering: KaTeX
• End-to-end testing: Playwright

Admin application

The repository CatDatAdmin contains the admin functionality for CatDat.

Similar projects

CatDat draws inspiration from and complements other resources in category theory:

• Catabase: A similar project that appears to be abandoned. It is more ambitious in terms of available data types but less complete for basic categories. The UI is not very intuitive, and it lacks an integrated deduction system between properties. See the nForum announcement.
• SmallCategories: A database that systematically enumerates isomorphism classes of small finite categories. Each entry represents one finite category by its multiplication table and provides a visualization and selected properties of that category. The database is currently complete for categories with at most 8 morphisms.
• nLab: A wiki for (higher) category theory. CatDat refers to nLab pages for detailed information on its entries.
• Clowder Project: A new online reference for category theory. Unlike CatDat, which is data-based, Clowder follows a textbook-based approach.
• Database of Ring Theory: This database focuses on ring theory and module theory rather than category theory, but is very similar in nature and was a major inspiration for CatDat.
• pi-Base: This is a database of examples and counterexamples in topology. Just like CatDat, it uses three types of entries (objects, properties, and theorems) and automatically derives properties from the theorems.

MathBases lists many other databases for other kinds of mathematical structures.

Financial support

If you find this project useful, you can support its development:

Cost transparency. The project currently only incurs domain costs of about $15 per year. There are no costs for hosting or the database. The project has no external funding.