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.
Instances
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))
Instances For
class
Category
{O : Sort u}
(Mor : O → O → Sort v)
extends Category.Struct Mor :
Sort (max (max 1 u) v)