class Category.Struct (O : Type u) : Type (max u (v + 1))

Sorts have an instance of this class when they have a Category structure.

This means that the members of this sort can be considered as objects in some category, to which we can associate some other sort for the morphisms between these objects. We also have, for each object, an identity morphism, and, for any two pairs of objects, ways of composing the morphisms between them.

This does not yet contain any properties about these data: Category O has them instead.

Small categories will have O : Type, and large categories will have a large O. For example: Type : Type 1.

• Mor : O → O → Type v

  Each pair of objects gets its own sort of morphism.

• id : {A : O} → Category.Struct.Mor A A

  Each such sort has a distinguished identity morphism.

• comp : {A B C : O} → Category.Struct.Mor A B → Category.Struct.Mor B C → Category.Struct.Mor A C

  We can compose morphisms to link many objects together.

def «term_≫_» : Lean.TrailingParserDescr

Equations

• «term_≫_» = Lean.ParserDescr.trailingNode `«term_≫_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 80))

class Category (O : Type u) extends Category.Struct O : Type (max u (u_1 + 1))

A category has the structure of a category—objects, morphisms, identities, composition—and laws.

• Mor : O → O → Type u_1
• id : {A : O} → Category.Struct.Mor A A
• comp : {A B C : O} → Category.Struct.Mor A B → Category.Struct.Mor B C → Category.Struct.Mor A C
• pre_id : ∀ {A B : O} (f : Category.Struct.Mor A B), Category.Struct.id ≫ f = f

  The identity does nothing before a morphism.

• post_id : ∀ {A B : O} (f : Category.Struct.Mor A B), f ≫ Category.Struct.id = f

  The identity does nothing after a morphism

• comp_assoc : ∀ {A B C D : O} (f : Category.Struct.Mor A B) (g : Category.Struct.Mor B C) (h : Category.Struct.Mor C D), f ≫ g ≫ h = (f ≫ g) ≫ h

  We can compose morphisms without regard to the grouping.