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
    constructor ↓obj
    field
      {x} : Ob A
      {y} : Ob B
      map : Hom C (F .F₀ x) (G .F₀ 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
    constructor ↓hom
    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₁ α ≡ G .F₁ β 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 .F-id) ·· C.id-comm ·· ap (C._∘ _) (sym (G .F-id))

  ↓∘ : ∀ {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 ⟩
      G .F₁ g.β C.∘ b.map C.∘ F .F₁ f.α  ≡⟨ ap (_ C.∘_) f.sq ⟩
      G .F₁ g.β C.∘ G .F₁ f.β C.∘ a.map  ≡⟨ C.pulll (sym (G .F-∘ _ _)) ⟩
      G .F₁ (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