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
  module _ (A-grpd : is-pregroupoid A) (B-grpd : is-pregroupoid B) where
    open ↓Hom
    open is-invertible
    open Inverses

    ↓-is-pregroupoid : is-pregroupoid _↓_
    ↓-is-pregroupoid f .inv .α = A-grpd (f .α) .inv
    ↓-is-pregroupoid f .inv .β = B-grpd (f .β) .inv
    ↓-is-pregroupoid f .inv .sq = C.rswizzle
      (sym (C.lswizzle (f .sq) (G.annihilate (B-grpd (f .β) .invr))) ∙ C.assoc _ _ _)
      (F.annihilate (A-grpd (f .α) .invl))
    ↓-is-pregroupoid f .inverses .invl = ↓Hom-path (A-grpd (f .α) .invl) (B-grpd (f .β) .invl)
    ↓-is-pregroupoid f .inverses .invr = ↓Hom-path (A-grpd (f .α) .invr) (B-grpd (f .β) .invr)

module _ {A : Precategory ao ah} {B : Precategory bo bh} where
  private module A = Precategory A

  infix 5 _↙_ _↘_
  _↙_ : A.Ob → Functor B A → Precategory _ _
  X ↙ T = const! X ↓ T

  _↘_ : Functor B A → A.Ob → Precategory _ _
  S ↘ X = S ↓ const! X

module ↙-compose
    {oc ℓc od ℓd oe ℓe}
    {𝒞 : Precategory oc ℓc} {𝒟 : Precategory od ℓd} {ℰ : Precategory oe ℓe}
    (F : Functor 𝒞 𝒟) (G : Functor 𝒟 ℰ)
  where
  private
    module 𝒟 = Precategory 𝒟
    module ℰ = Precategory ℰ
    module F = Functor F
    module G = Cat.Functor.Reasoning G
  open ↓Obj
  open ↓Hom

  _↙>_ : ∀ {d} (g : Ob (d ↙ G)) → Ob (g .y ↙ F) → Ob (d ↙ G F∘ F)
  g ↙> f = ↓obj (G.₁ (f .map) ℰ.∘ g .map)

  ↙-compose : ∀ {d} (g : Ob (d ↙ G)) → Functor (g .y ↙ F) (d ↙ G F∘ F)
  ↙-compose g .F₀ f = g ↙> f
  ↙-compose g .F₁ {f} {f'} h = ↓hom {β = h .β} $
    (G.₁ (f' .map) ℰ.∘ g .map) ℰ.∘ ℰ.id          ≡⟨ ℰ.idr _ ⟩≡
    G.₁ (f' .map) ℰ.∘ g .map                     ≡⟨ G.pushl (sym (𝒟.idr _) ∙ h .sq) ⟩≡
    G.₁ (F.₁ (h .β)) ℰ.∘ G.₁ (f .map) ℰ.∘ g .map ∎
  ↙-compose g .F-id = ↓Hom-path _ _ refl refl
  ↙-compose g .F-∘ _ _ = ↓Hom-path _ _ refl refl

  ↙>-id : ∀ {c} {f : Ob (c ↙ G F∘ F)} → ↓obj (f .map) ↙> ↓obj 𝒟.id ≡ f
  ↙>-id = ↓Obj-path _ _ refl refl (G.eliml refl)

-- Outside the main module to make instance search work.
module _ where
  open ↓Hom
  open ↓Obj
  open Precategory
  open Functor


  instance
    Extensional-↓Hom
      : ∀ {ℓr}
      → {F : Functor A C} {G : Functor B C}
      → {f g : ↓Obj F G}
      → ⦃ sab : Extensional (A .Hom (f .x) (g .x) × B .Hom (f .y) (g .y)) ℓr ⦄
      → Extensional (↓Hom F G f g) ℓr
    Extensional-↓Hom {A = A} {B = B} {F = F} {G = G} {f = f} {g = g} ⦃ sab ⦄ =
      injection→extensional! (λ p → ↓Hom-path F G (ap fst p) (ap snd p)) sab

    -- Overlapping instances for ↙ and ↘; these resolve issues where
    -- Agda cannot determine the source category A for 'Const'. We can
    -- also optimize the instance a bit to avoid a silly obligation that
    -- 'tt ≡ tt'.
    Extensional-↙Hom
      : ∀ {ℓr}
      → {X : A .Ob} {T : Functor B A}
      → {f g : ↓Obj (const! X) T}
      → ⦃ sb : Extensional (B .Hom (f .y) (g .y)) ℓr ⦄
      → Extensional (↓Hom (const! X) T f g) ℓr
    Extensional-↙Hom {B = B} {X = X} {T = T} {f = f} {g = g} ⦃ sb ⦄ =
      injection→extensional! {f = λ sq → sq .β} (λ p → ↓Hom-path (const! X) T refl p) sb
    {-# OVERLAPS Extensional-↙Hom #-}

    Extensional-↘Hom
      : ∀ {ℓr}
      → {T : Functor A B} {X : B .Ob}
      → {f g : ↓Obj T (const! X)}
      → ⦃ sa : Extensional (A .Hom (f .x) (g .x)) ℓr ⦄
      → Extensional (↓Hom T (const! X) f g) ℓr
    Extensional-↘Hom {A = A} {T = T} {X = X} {f = f} {g = g} ⦃ sa ⦄ =
      injection→extensional! {f = λ sq → sq .α} (λ p → ↓Hom-path T (const! X) p refl) sa
    {-# OVERLAPS Extensional-↘Hom #-}


    -- Extensionality cannot handle PathP, but we /can/ make a bit of progress
    -- by deleting 'tt ≡ tt' obligations when using ↙ and ↘.
    Extensional-↙Obj
      : ∀ {ℓr}
      → {X : A .Ob} {T : Functor B A}
      → ⦃ sb : Extensional (Σ[ Y ∈ B .Ob ] (A .Hom X (T .F₀ Y))) ℓr ⦄
      → Extensional (↓Obj (const! X) T) ℓr
    Extensional-↙Obj {A = A} {B = B} {X = X} {T = T} ⦃ sb ⦄ =
      iso→extensional isom sb
        where
          -- Easier to just do this by hand.
          isom : Iso (↓Obj (const! X) T) (Σ[ Y ∈ B .Ob ] (A .Hom X (T .F₀ Y)))
          isom .fst α = ↓Obj.y α , ↓Obj.map α
          isom .snd .is-iso.inv (Y , f) = ↓obj f
          isom .snd .is-iso.rinv _ = refl
          isom .snd .is-iso.linv _ = ↓Obj-path (const! X) T refl refl refl

    Extensional-↘Obj
      : ∀ {ℓr}
      → {T : Functor A B} {Y : B .Ob}
      → ⦃ sb : Extensional (Σ[ X ∈ A .Ob ] (B .Hom (T .F₀ X) Y)) ℓr ⦄
      → Extensional (↓Obj T (const! Y)) ℓr
    Extensional-↘Obj {A = A} {B = B} {T = T} {Y = Y} ⦃ sb ⦄ =
      iso→extensional isom sb
        where
          -- Easier to just do this by hand.
          isom : Iso (↓Obj T (const! Y)) (Σ[ X ∈ A .Ob ] (B .Hom (T .F₀ X) Y))
          isom .fst α = ↓Obj.x α , ↓Obj.map α
          isom .snd .is-iso.inv (Y , f) = ↓obj f
          isom .snd .is-iso.rinv _ = refl
          isom .snd .is-iso.linv _ = ↓Obj-path T (const! Y) refl refl refl