Skip to main content

Functor

structure Functor[O1, M1, O2, M2] {
    src_cat: Category[O1, M1]
    dst_cat: Category[O2, M2]
    obj_map: O1 -> O2
    mor_map: M1 -> M2
} constraint {
    is_functor(src_cat, dst_cat, obj_map, mor_map)
}

A functor between two categories.

GitHub

dst_cat​

Functor.dst_cat: Functor[O1, M1, O2, M2] -> Category[O2, M2]

The target category.

mor_map​

Functor.mor_map: (Functor[O1, M1, O2, M2], M1) -> M2

The action on morphisms.

obj_map​

Functor.obj_map: (Functor[O1, M1, O2, M2], O1) -> O2

The action on objects.

src_cat​

Functor.src_cat: Functor[O1, M1, O2, M2] -> Category[O1, M1]

The source category.