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:ACF : \ca{A} \to \ca{C} and G:BCG : \ca{B} \to \ca{C} with common codomain, written FGF \downarrow G, is the directed, bicategorical analogue of a pullback square. It consists of maps in C\ca{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 ACBA \to C \ot 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 FGF \downarrow G are given by triples (x,y,f)(x, y, f) where x:Ax : \ca{A}, y:By : \ca{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 α:xaxb\alpha : x_a \to x_b and β:yayb\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