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

The comma category is the universal way of completing a cospan of functors $A \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 \downarrow G$ are given by triples $(x, y, f)$ where $x : \mathcal{A}$, $y : \mathcal{B}$, and $f : F(x) \to G(y)$.

  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 $(x_a, y_a, f_a) \to (x_b, y_b, f_b)$ is given by a pair of maps $\alpha : x_a \to x_b$ and $\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
    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 $\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 .↓Obj.map) λ x y f → f .↓Hom.sq