open import Cat.Instances.Shape.Terminal open import Cat.Instances.Functor open import Cat.Prelude module Cat.Instances.Comma where
Comma categoriesπ
The comma category of two functors and with common codomain, written , is the directed, bicategorical analogue of a pullback square. It consists of maps in which all have their domain in the image of , and codomain in the image of .
The comma category is the universal way of completing a cospan of functors to a square, like the one below, which commutes up to a natural transformation . Note the similarity with a pullback square.
The objects in are given by triples where , , and .
record βObj : Type (h β ao β bo) where no-eta-equality field {x} : Ob A {y} : Ob B map : Hom C (Fβ F x) (Fβ G y)
A morphism from is given by a pair of maps and , such that the square below commutes. Note that this is exactly the data of one component of a naturality square.
record βHom (a b : βObj) : Type (h β bh β ah) where no-eta-equality private module a = βObj a module b = βObj b field {Ξ±} : Hom A a.x b.x {Ξ²} : Hom B a.y b.y sq : b.map C.β Fβ F Ξ± β‘ Fβ G Ξ² C.β a.map
We omit routine characterisations of equality in βHom from the page: βHom-path and βHom-set.
Identities and compositions are given componentwise:
βid : β {a} β βHom a a βid .βHom.Ξ± = A.id βid .βHom.Ξ² = B.id βid .βHom.sq = ap (_ C.β_) (F-id F) Β·Β· C.id-comm Β·Β· ap (C._β _) (sym (F-id G)) ββ : β {a b c} β βHom b c β βHom a b β βHom a c ββ {a} {b} {c} g f = composite where open βHom module a = βObj a module b = βObj b module c = βObj c module f = βHom f module g = βHom g composite : βHom a c composite .Ξ± = g.Ξ± A.β f.Ξ± composite .Ξ² = g.Ξ² B.β f.Ξ² composite .sq = c.map C.β Fβ F (g.Ξ± A.β f.Ξ±) β‘β¨ ap (_ C.β_) (F-β F _ _) β©β‘ c.map C.β Fβ F g.Ξ± C.β Fβ F f.Ξ± β‘β¨ C.extendl g.sq β©β‘ Fβ G g.Ξ² C.β b.map C.β Fβ F f.Ξ± β‘β¨ ap (_ C.β_) f.sq β©β‘ Fβ G g.Ξ² C.β Fβ G f.Ξ² C.β a.map β‘β¨ C.pulll (sym (F-β G _ _)) β©β‘ Fβ G (g.Ξ² B.β f.Ξ²) C.β a.map β
This assembles into a precategory.
_β_ : Precategory _ _ _β_ .Ob = βObj _β_ .Hom = βHom _β_ .Hom-set = βHom-set _β_ .id = βid _β_ ._β_ = ββ _β_ .idr f = βHom-path (A.idr _) (B.idr _) _β_ .idl f = βHom-path (A.idl _) (B.idl _) _β_ .assoc f g h = βHom-path (A.assoc _ _ _) (B.assoc _ _ _)
We also have the projection functors onto the factors, and the natural transformation witnessing βdirected commutativityβ of the square.
Dom : Functor _β_ A Dom .Fβ = βObj.x Dom .Fβ = βHom.Ξ± Dom .F-id = refl Dom .F-β _ _ = refl Cod : Functor _β_ B Cod .Fβ = βObj.y Cod .Fβ = βHom.Ξ² Cod .F-id = refl Cod .F-β _ _ = refl ΞΈ : (F Fβ Dom) => (G Fβ Cod) ΞΈ = NT (Ξ» x β x .βObj.map) Ξ» x y f β f .βHom.sq