class Category.Struct {O : Sort u} (Mor : O → O → Sort v) : Sort (max (max 1 u) v)

The basic data of a Category, without the corresponding laws.

This can be useful, allowing us to first define the data of a category, giving us a composition operator, before then proving that it behaves correctly.

• id : {x : O} → Mor x x

  We require a particular morphism for any object, acting as the identity.

• comp : {a b c : O} → Mor a b → Mor b c → Mor a c

  We choose to compose arrows from left to right, binding to the right.

def «term_≫_» : Lean.TrailingParserDescr

We define ≫ as a convenient notation for composition of morphisms.

Equations

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

class Category {O : Sort u} (Mor : O → O → Sort v) extends Category.Struct Mor : Sort (max (max 1 u) v)

• id : {x : O} → Mor x x
• comp : {a b c : O} → Mor a b → Mor b c → Mor a c
• pre_id : ∀ {x x_1 : O} {f : Mor x x_1}, Category.Struct.id ≫ f = f
• post_id : ∀ {x x_1 : O} {f : Mor x x_1}, f ≫ Category.Struct.id = f
• comp_assoc : ∀ {a b c d : O} {f : Mor a b} {g : Mor b c} {h : Mor c d}, (f ≫ g) ≫ h = f ≫ g ≫ h