Synthetic category theory

Content created by Egbert Rijke, Ivan Kobe and Fredrik Bakke.

Created on 2024-09-01.
Last modified on 2024-09-25.

{-# OPTIONS --guardedness #-}

Idea

Synthetic category theory is an approach to the foundation of mathematics in which the principal objects are ∞-categories. The theory is due to Cisinski et al. [DCCW24], which we will follow here closely. Synthetic category theory differs from wild category theory in the sense that wild categories are defined as structured objects, i.e., their definition follows an “analytic” approach, whereas synthetic categories are defined by the rules for the type of all synthetic categories.

Some core principles of higher category theory include:

  • To express that two things are equal we specify an isomorphism between them.
  • Any valid statement or construction in category theory must respect isomorphisms [Mak98].

Modules in the synthetic category theory namespace

module synthetic-category-theory where

open import synthetic-category-theory.cone-diagrams-synthetic-categories public
open import synthetic-category-theory.cospans-synthetic-categories public
open import synthetic-category-theory.equivalences-synthetic-categories public
open import synthetic-category-theory.invertible-functors-synthetic-categories public
open import synthetic-category-theory.pullbacks-synthetic-categories public
open import synthetic-category-theory.retractions-synthetic-categories public
open import synthetic-category-theory.sections-synthetic-categories public
open import synthetic-category-theory.synthetic-categories public

References

[DCCW24]
Kim Nguyen Denis-Charles Cisinski, Bastiaan Cnossen and Tashi Walde. Formalization of higher categories. 08 2024. URL: https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view.
[Mak98]
M. Makkai. Towards a categorical foundation of mathematics. In Logic Colloquium '95 (Haifa), volume 11 of Lecture Notes Logic, pages 153–190. Springer, Berlin, 1998. doi:10.1007/978-3-662-22108-2\_11.

Recent changes