Documentation

CKMath.Category.Definition

class Category.Struct {O : Sort u} (Mor : OOSort 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 bMor b cMor 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
    Instances For
      class Category {O : Sort u} (Mor : OOSort v) extends Category.Struct Mor :
      Sort (max (max 1 u) v)
      • id : {x : O} → Mor x x
      • comp : {a b c : O} → Mor a bMor b cMor 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
      Instances