Maths in Lean: category theory #

The category typeclass is defined in category_theory/category/basic.lean. It depends on the type of the objects, so for example we might write category (Type u) if we're talking about a category whose objects are types (in universe u).

Functors (which are a structure, not a typeclass) are defined in category_theory/functor/basic.lean, along with identity functors and functor composition.

Natural transformations, and their compositions, are defined in category_theory/natural_transformation.lean.

The category of functors and natural transformations between fixed categories C and D is defined in category_theory/functor/category.lean.

Cartesian products of categories, functors, and natural transformations appear in category_theory/products/basic.lean. (Product in the sense of limits will appear elsewhere soon!)

The category of types, and the hom pairing functor, are defined in category_theory/types.lean.

Notation #

Categories #

We use the ⟶ (\hom) arrow to denote sets of morphisms, as in X ⟶ Y. This leaves the actual category implicit; it is inferred from the type of X and Y by typeclass inference.

We use 𝟙 (\b1) to denote identity morphisms, as in 𝟙 X.

We use ≫ (\gg) to denote composition of morphisms, as in f ≫ g, which means "f followed by g". You may prefer write composition in the usual convention, using ⊚ (\oo or \circledcirc), as in f ⊚ g which means "g followed by f". To do so you'll need to add this notation locally, via

local notation f ` ⊚ `:80 g:80 := category.comp g f

Isomorphisms #

We use ≅ for isomorphisms.

Functors #

We use ⥤ (\func) to denote functors, as in C ⥤ D for the type of functors from C to D. (Unfortunately ⇒ is reserved in logic.relator, so we can't use that here.)

We use F.obj X to denote the action of a functor on an object. We use F.map f to denote the action of a functor on a morphism`.

Functor composition can be written as F ⋙ G.

Natural transformations #

We use τ.app X for the components of a natural transformation.

Otherwise, we mostly use the notation for morphisms in any category:

We use F ⟶ G (\hom or -->) to denote the type of natural transformations, between functors F and G. We use F ≅ G (\iso) to denote the type of natural isomorphisms.

For vertical composition of natural transformations we just use ≫. For horizontal composition, use hcomp.