open import Cat.Diagram.Limit.Base
open import Cat.Instances.Comma
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cat

module Cat.Instances.Comma.Limits where

open make-is-limit
open ↓Obj
open ↓Hom
open _=>_

Limits in comma categories🔗

This short note proves the following fact about limits in comma categories of the form $d\swarrow F\text{:}$ If $\mathcal{C}$ has a limit $L$ for $\mathrm{cod}\circ G$ and $F$ preserves limits the size of $G\text{’s}$ shape $\mathcal{J}\text{,}$ then $L$ can be made into an object of $d\swarrow F\text{,}$ and this object is the limit of $J\text{.}$

module
  _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} {d}
    (F : Functor C D) {lo lℓ} (F-cont : is-continuous lo lℓ F)
    {J : Precategory lo lℓ} {G : Functor J (d ↙ F)}
  where

  private
    module G = Functor G
    module D = Cat D
    module C = Cat C
    module F = Fr F

  Cod-lift-limit : Limit (Cod _ F F∘ G) → Limit G
  Cod-lift-limit limf = to-limit (to-is-limit lim') where
    module limf = Limit limf

    flimf = F-cont limf.has-limit
    module flimf = is-limit flimf

The family of maps $d\to FL$ can be given componentwise, since $FL$ is a limit in $\mathcal{D}\text{:}$ it suffices to give a family of maps $d\to FGj\text{,}$ at each $j:\mathcal{J}\text{.}$ But $G$ sends objects of $\mathcal{J}$ to pairs which include a map $d\to FGj\text{,}$ and it does so in a way compatible with $F\text{,}$ by definition.

    apex : ⌞ d ↙ F ⌟
    apex .x = tt
    apex .y = limf.apex
    apex .map = flimf.universal (λ j → G.₀ j .map) λ f → sym (G.₁ f .sq) ∙ D.elimr refl

Similarly short calculations show that we can define maps in $d\swarrow F$ into $L$ componentwise, and these satisfy the universal property.

    lim' : make-is-limit G apex
    lim' .ψ j .α = tt
    lim' .ψ j .β = limf.ψ j
    lim' .ψ j .sq = sym (flimf.factors _ _ ∙ D.intror refl)
    lim' .commutes f = ext (sym (limf.eps .is-natural _ _ _) ∙ C.elimr limf.Ext.F-id)
    lim' .universal eta p .α = tt
    lim' .universal eta p .β = limf.universal (λ j → eta j .β) λ f → ap β (p f)
    lim' .universal eta p .sq = D.elimr refl ∙ sym (flimf.unique _ _ _ λ j → F.pulll (limf.factors _ _) ∙ sym (eta j .sq) ∙ D.elimr refl)
    lim' .factors eta p = ext (limf.factors _ _)
    lim' .unique eta p other q = ext (limf.unique _ _ _ λ j → ap β (q j))

As an easy corollary, we get: if $\mathcal{C}$ is small-complete and $F$ small-continuous, then $d\swarrow F$ is small-complete as well.

module
  _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
    (F : Functor C D) (c-compl : is-complete ℓ ℓ C) (F-cont : is-continuous ℓ ℓ F)
    where
  private
    module C = Cat C
    module D = Cat D
    module F = Fr F

  comma-is-complete : ∀ {d} → is-complete ℓ ℓ (d ↙ F)
  comma-is-complete G = Cod-lift-limit F F-cont (c-compl (Cod _ F F∘ G))