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 F:Aβ†’CF : \mathcal{A} \to \mathcal{C} and G:Bβ†’CG : \mathcal{B} \to \mathcal{C} with common codomain, written F↓GF \downarrow G, is the directed, bicategorical analogue of a pullback square. It consists of maps in C\mathcal{C} which all have their domain in the image of FF, and codomain in the image of GG.

The comma category is the universal way of completing a cospan of functors Aβ†’C←BA \to C {\leftarrow}B to a square, like the one below, which commutes up to a natural transformation ΞΈ\theta. Note the similarity with a pullback square.

The objects in F↓GF \downarrow G are given by triples (x,y,f)(x, y, f) where x:Ax : \mathcal{A}, y:By : \mathcal{B}, and f:F(x)β†’G(y)f : F(x) \to G(y).

  record ↓Obj : Type (h βŠ” ao βŠ” bo) where
      {x} : Ob A
      {y} : Ob B
      map : Hom C (Fβ‚€ F x) (Fβ‚€ G y)

A morphism from (xa,ya,fa)→(xb,yb,fb)(x_a, y_a, f_a) \to (x_b, y_b, f_b) is given by a pair of maps α:xa→xb\alpha : x_a \to x_b and β:ya→yb\beta : y_a \to y_b, 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
      module a = ↓Obj a
      module b = ↓Obj b

      {Ξ±} : Hom A a.x b.x
      {Ξ²} : Hom B a.y b.y
      sq : C.∘ F₁ F Ξ± ≑ F₁ G Ξ² C.∘

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.Ξ± =
  ↓id .↓Hom.Ξ² =
  ↓id .↓Hom.sq = ap (_ C.∘_) (F-id F) Β·Β· Β·Β· 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.∘ F₁ F (g.Ξ± A.∘ f.Ξ±)    β‰‘βŸ¨ ap (_ C.∘_) (F-∘ F _ _) βŸ©β‰‘ C.∘ F₁ F g.Ξ± C.∘ F₁ F f.Ξ± β‰‘βŸ¨ C.extendl g.sq βŸ©β‰‘
      F₁ G g.Ξ² C.∘ C.∘ F₁ F f.Ξ± β‰‘βŸ¨ ap (_ C.∘_) f.sq βŸ©β‰‘
      F₁ G g.Ξ² C.∘ F₁ G f.Ξ² C.∘ β‰‘βŸ¨ C.pulll (sym (F-∘ G _ _)) βŸ©β‰‘
      F₁ G (g.Ξ² B.∘ f.Ξ²) C.∘    ∎

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 ΞΈ\theta 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 .↓ Ξ» x y f β†’ f .↓Hom.sq