module Cat.Diagram.Limit.Base where

Limits🔗

Idea🔗

To motivate limits, note how all the above examples have roughly the same structure. They all consist of some object, a bunch of maps out of said object, some commutativity conditions, and a universal property that states that we can construct unique maps into the object under certain conditions.

Our first step towards making this vague intuition precise is to construct a mathematical widget that picks out a collection of objects, arrows, and commutativity conditions in a category. This is required to describe the collection of maps out of our special objects, and the equations they satisfy. Luckily, we already have such a widget: functors!

To see how this works, let’s take a very simple example: a functor out of the single object category with one morphism into some category $\mathcal{C}$. If we look at the image of such a functor, we can see that it picks out a single object; the single morphism must be taken to the identity morphism due to functoriality. We can scale this example up to functors from discrete category with $n$ elements; if we look at the image of such a functor, we shall see that it selects out $n$ objects of $\mathcal{C}$.

We can perform the same trick with non-discrete categories; for instance, a functor out of the parallel arrows category selects a pair of parallel arrows in $\mathcal{C}$, a functor out of the isomorphism category selects an isomorphism in $\mathcal{C}$, and so on. We call such functors diagrams to suggest that we should think of them as picking out some shape in $\mathcal{C}$.

We can use this newfound insight to describe the shape that each of our examples is defined over. Products are defined over a diagram that consists of a pair of objects; these diagrams correspond to functors out of the category with 2 objects and only identity morphisms. Equalisers are defined over a diagram that consists of a pair of parallel morphisms; such diagrams are given by functors out of the aforementioned parallel arrows category. Pullbacks defined over a diagram of the shape, $\bullet \to \bullet \leftarrow \bullet$; again, these diagrams are given by functors out of the category with that exact shape. Terminal objects may seem to break this trend, but we can think of them as being defined over the empty diagram, the unique functor from the category with no objects.

We now move our attention to the maps out of our special object into the objects of the diagram. Note that these maps need to commute with any morphisms in the diagram, as is the case with pullbacks and equalisers. This is where our definition diverges from many other introductory sources. The typical approach is to define a bespoke widget called a cone that encodes the required morphisms and commuting conditions, and then proceeding from there.

However, this approach is somewhat unsatisfying. Why did we have to invent a new object just to bundle up the data we needed? Furthermore, cones are somewhat disconnected from the rest of category theory, which makes it more difficult to integrate results about limits into the larger body of work. It would be great if we could encode the data we needed using existing objects!

Luckily, we can! If we take a step back, we can notice that we are trying to construct a map into a functor. What are maps into functors? Natural transformations! Concretely, let $D : \mathcal{J} \to \mathcal{C}$ be some diagram. We can encode the same data as a cone in a natural transformation $\eta : {!x} \circ \mathord{!} \to D$, where $!x : \top \to \mathcal{C}$ denotes the constant functor that maps object to $x$ and every morphism to $id$, and $! : \mathcal{J} \to \top$ denotes the unique functor into the terminal category. The components of such a natural transformation yield maps from $x \to D(j)$ for every $j : \mathcal{J}$, and naturality ensures that these maps must commute with the rest of the diagram. We can describe this situation diagrammatically like so:

All that remains is the universal property. If we translate this into our existing machinery, that means that $!x$ must be the universal functor equipped with a natural transformation $\eta$; that is, for any other $K : \{*\} \to \mathcal{C}$ equipped with $\tau : K \circ \mathord{!} \to D$, we have a unique natural transformation $\sigma : K \to {!x}$ that factors $\tau$. This is a bit of a mouthful, so let’s look at a diagram instead.

We might be tempted to stop here and call it a day, but we can go one step further. It turns out that these universal functors have a name: they are right Kan extensions. This allows for an extremely concise definition of limits: $x : \mathcal{C}$ is the limit of a diagram $D : \mathcal{J} \to \mathcal{C}$ when the constant functor $!x : \{*\} \to \mathcal{C}$ is a right Kan extension of $! : \mathcal{J} \to \{*\}$ along $D$.

module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} (Diagram : Functor J C) where
  private
    module C = Precategory C
    open _=>_
    open Functor

  cone→counit : ∀ {x : C.Ob} → (Const x => Diagram) → const! x F∘ !F => Diagram
  unquoteDef cone→counit = define-coherence cone→counit

  counit→cone : ∀ {K : Functor ⊤Cat C} → K F∘ !F => Diagram → (Const (K .F₀ tt) => Diagram)
  counit→cone {K = K} eta .η = eta .η
  counit→cone {K = K} eta .is-natural x y f =
    ap (_ C.∘_) (sym (K .F-id)) ∙ eta .is-natural x y f

  is-limit : (x : C.Ob) → Const x => Diagram → Type _
  is-limit x cone = is-ran !F Diagram (const! x) (cone→counit cone)

In a “bundled” form, we may define the type of limits for a diagram $D$ as the type of right extensions of $D$ along the terminating functor $\mathord{!} : \mathcal{J} \to \{*\}$.

  Limit : Type _
  Limit = Ran !F Diagram

Concretely🔗

The definition above is very concise, and it has the benefit of being abstract: We can re-use definitions and theorems originally stated for right Kan extensions to limits. However, it has the downside of being abstract: it’s good for working with limits in general, but working with a specific limit is penalised, as the data we want to get at is “buried”.

The definition above is also hard to instantiate, since you have to.. bury the data, and some of it is really quite deep! What we do is provide an auxiliary record, make-is-limit, which computes right extensions to the point.

We solve this by defining a concretised version of is-limit, called make-is-limit, which exposes the following data. First, we have morphisms from the apex to every value in the diagram, a family called $\psi$. Moreover, if $f : x \to y$ is a morphism in the “shape” category $\mathcal{J}$, then $F(f)\psi_x = \psi_y$, i.e., the $\psi$ maps fit into triangles

    field
      ψ        : (j : J.Ob) → C.Hom apex (F₀ j)
      commutes : ∀ {x y} (f : J.Hom x y) → F₁ f C.∘ ψ x ≡ ψ y

The rest of the data says that $\psi$ is the universal family of maps with this property: If $\eta_j : x \to Fj$ is another family of maps with the same commutativity property, then each $\eta_j$ factors through the apex by a single, unique universal morphism:

      universal
        : ∀ {x : C.Ob}
        → (eta : ∀ j → C.Hom x (F₀ j))
        → (∀ {x y} (f : J.Hom x y) → F₁ f C.∘ eta x ≡ eta y)
        → C.Hom x apex

      factors
        : ∀ {j : J.Ob} {x : C.Ob}
        → (eta : ∀ j → C.Hom x (F₀ j))
        → (p : ∀ {x y} (f : J.Hom x y) → F₁ f C.∘ eta x ≡ eta y)
        → ψ j C.∘ universal eta p ≡ eta j

      unique
        : ∀ {x : C.Ob}
        → (eta : ∀ j → C.Hom x (F₀ j))
        → (p : ∀ {x y} (f : J.Hom x y) → F₁ f C.∘ eta x ≡ eta y)
        → (other : C.Hom x apex)
        → (∀ j → ψ j C.∘ other ≡ eta j)
        → other ≡ universal eta p

If we have this data, then we can make a value of is-limit. It might seem like naturality, required for a right Kan extension, is missing from make-is-limit, but it can be derived from the other data we have been given:

  to-is-limit : ∀ {D : Functor J C} {apex}
              → (mk : make-is-limit D apex)
              → is-limit D apex (to-cone mk)
  to-is-limit {Diagram} {apex} mklim = lim where
    open make-is-limit mklim
    open is-ran
    open Functor
    open _=>_

    lim : is-limit Diagram apex (to-cone mklim)
    lim .σ {M = M} α .η _ =
      universal (α .η) (λ f → sym (α .is-natural _ _ f) ∙ C.elimr (M .F-id))
    lim .σ {M = M} α .is-natural _ _ _ =
      lim .σ α .η _ C.∘ M .F₁ tt ≡⟨ C.elimr (M .F-id) ⟩
      lim .σ α .η _              ≡˘⟨ C.idl _ ⟩
      C.id C.∘ lim .σ α .η _     ∎
    lim .σ-comm {β = β} = Nat-path λ j →
      factors (β .η) _
    lim .σ-uniq {β = β} {σ' = σ'} p = Nat-path λ _ →
      sym $ unique (β .η) _ (σ' .η tt) (λ j → sym (p ηₚ j))

To use the data of is-limit, we provide a function for unmaking a limit:

  unmake-limit
    : ∀ {D : Functor J C} {F : Functor ⊤Cat C} {eps}
    → is-ran !F D F eps
    → make-is-limit D (Functor.F₀ F tt)

We also provide a similar interface for the bundled form of limits.

module Limit
  {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Functor J C} (L : Limit D)
  where

The “apex” object of the limit is the single value in the image of the extension functor.

  apex : C.Ob
  apex = Ext.₀ tt

Furthermore, we can show that the apex is the limit, in the sense of is-limit, of the diagram. You’d think this is immediate, but unfortunately, proof assistants: is-limit asks for the constant functor functor $\{*\} \to \mathcal{C}$ with value apex to be a Kan extension, but Limit, being an instance of Ran, packages an arbitrary functor $\{*\} \to \mathcal{C}$.

Since Agda does not compare functors for $\eta$-equality, we have to shuffle our data around manually. Fortunately, this isn’t a very long computation.

  cone : Const apex => D
  cone .η x = eps .η x
  cone .is-natural x y f = ap (_ C.∘_) (sym $ Ext .F-id) ∙ eps .is-natural x y f

  has-limit : is-limit D apex cone
  has-limit .is-ran.σ α .η = σ α .η
  has-limit .is-ran.σ α .is-natural x y f =
    σ α .is-natural tt tt tt ∙ ap (C._∘ _) (Ext .F-id)
  has-limit .is-ran.σ-comm =
    Nat-path (λ _ → σ-comm ηₚ _)
  has-limit .is-ran.σ-uniq {M = M} {σ' = σ'} p =
    Nat-path (λ _ → σ-uniq {σ' = nt} (Nat-path (λ j → p ηₚ j)) ηₚ _) where
      nt : M => Ext
      nt .η = σ' .η
      nt .is-natural x y f = σ' .is-natural x y f ∙ ap (C._∘ _) (sym $ Ext .F-id)

  open is-limit has-limit public

Uniqueness🔗

Above, there has been mention of the limit. The limit of a diagram, if it exists, is unique up to isomorphism. This follows directly from uniqueness of Kan extensions.

We show a slightly more general result first: if there exist a pair of maps $f$, $g$ between the apexes of the 2 limits, and these maps commute with the 2 limits, then $f$ and $g$ are inverses.

  limits→inversesp
    : ∀ {f : C.Hom x y} {g : C.Hom y x}
    → (∀ {j : J.Ob} → Ly.ψ j C.∘ f ≡ Lx.ψ j)
    → (∀ {j : J.Ob} → Lx.ψ j C.∘ g ≡ Ly.ψ j)
    → C.Inverses f g
  limits→inversesp {f = f} {g = g} f-factor g-factor =
    inversesⁿ→inverses
      {α = hom→⊤-natural-trans f}
      {β = hom→⊤-natural-trans g}
      (Ran-unique.σ-inversesp Ly Lx
        (Nat-path λ j → f-factor {j})
        (Nat-path λ j → g-factor {j}))
      tt

Furthermore, any morphism between apexes that commutes with the limit must be invertible.

  limits→invertiblep
    : ∀ {f : C.Hom x y}
    → (∀ {j : J.Ob} → Ly.ψ j C.∘ f ≡ Lx.ψ j)
    → C.is-invertible f
  limits→invertiblep {f = f} f-factor =
    is-invertibleⁿ→is-invertible
      {α = hom→⊤-natural-trans f}
      (Ran-unique.σ-is-invertiblep
        Ly
        Lx
        (Nat-path λ j → f-factor {j}))
      tt

This implies that the universal maps must also be inverses.

  limits→inverses
    : C.Inverses (Ly.universal Lx.ψ Lx.commutes) (Lx.universal Ly.ψ Ly.commutes)
  limits→inverses =
    limits→inversesp (Ly.factors Lx.ψ Lx.commutes) (Lx.factors Ly.ψ Ly.commutes)

  limits→invertible
    : C.is-invertible (Ly.universal Lx.ψ Lx.commutes)
  limits→invertible = limits→invertiblep (Ly.factors Lx.ψ Lx.commutes)

Finally, we can bundle this data up to show that the apexes are isomorphic.

  limits-unique : x C.≅ y
  limits-unique = isoⁿ→iso (Ran-unique.unique Lx Ly) tt

Furthermore, if the universal map is invertible, then that means that its domain is also a limit of the diagram.

  is-invertible→is-limitp
    : ∀ {K' : Functor ⊤Cat C} {eps : K' F∘ !F => D}
    → (eta : ∀ j → C.Hom (K' .F₀ tt) (D.₀ j))
    → (p : ∀ {x y} (f : J.Hom x y) → D.₁ f C.∘ eta x ≡ eta y)
    → (∀ {j} → eta j ≡ eps .η j)
    → C.is-invertible (Ly.universal eta p)
    → is-ran !F D K' eps
  is-invertible→is-limitp {K' = K'} eta p q invert =
    generalize-limitp
      (is-invertible→is-ran Ly $ invertible→invertibleⁿ _ (λ _ → invert))
      q

Another useful fact is that if $L$ is a limit of some diagram $Dia$, and $Dia$ is naturally isomorphic to some other diagram $Dia'$, then the apex of $L$ is also a limit of $Dia'$.

  natural-iso-diagram→is-limitp
    : ∀ {D' : Functor J C} {eps : K F∘ !F => D'}
    → (isos : D ≅ⁿ D')
    → (∀ {j} → Isoⁿ.to isos .η j C.∘ Ly.ψ j ≡ eps .η j)
    → is-ran !F D' K eps
  natural-iso-diagram→is-limitp {D' = D'} isos p =
    generalize-limitp
      (natural-iso-of→is-ran Ly isos)
      p

Since limits are unique “up to isomorphism”, if $C$ is a univalent category, then Limit itself is a proposition! This is an instance of the more general uniqueness of Kan extensions.

  Limit-is-prop : is-category C → is-prop (Limit Diagram)
  Limit-is-prop cat = Ran-is-prop cat

Preservation of limits🔗

Suppose you have a limit $L$ of a diagram $\mathrm{Dia}$. We say that $F$ preserves $L$ if $F(L)$ is also a limit of $F \circ \mathrm{Dia}$.

This definition is necessary because $\mathcal{D}$ will not, in general, possess an operation assigning a limit to every diagram — therefore, there might not be a “canonical limit” of $F\circ\mathrm{Dia}$ we could compare $F(L)$ to. However, since limits are described by a universal property (in particular, being terminal), we don’t need such an object! Any limit is as good as any other.

In more concise terms, we say a functor preserves limits if it takes limiting cones “upstairs” to limiting cones “downstairs”.

  preserves-limit : Type _
  preserves-limit =
    ∀ {K : Functor ⊤Cat C} {eps : K F∘ !F => Diagram}
    → (lim : is-ran !F Diagram K eps)
    → preserves-ran F lim

Reflection of limits🔗

Using the terminology from before, we say a functor reflects limits if it takes limiting cones “downstairs” to limiting cones “upstairs”. More concretely, if we have a limit in $\mathcal{D}$ of $F \circ \mathrm{Dia}$ with apex $F(a)$, then $F$ reflects this limit means that $a$ was already the limit of $\mathrm{Dia}$!

  reflects-limit : Type _
  reflects-limit =
    ∀ {K : Functor ⊤Cat C} {eps : K F∘ !F => Diagram}
    → (ran : is-ran !F (F F∘ Diagram) (F F∘ K) (nat-assoc-from (F ▸ eps)))
    → reflects-ran F ran

Continuity🔗

is-continuous
  : ∀ (oshape hshape : Level)
      {C : Precategory o₁ h₁}
      {D : Precategory o₂ h₂}
  → Functor C D → Type _

A continuous functor is one that — for every shape of diagram J, and every diagram diagram of shape J in C — preserves the limit for that diagram.

is-continuous oshape hshape {C = C} F =
  ∀ {J : Precategory oshape hshape} {Diagram : Functor J C}
  → preserves-limit F Diagram

Completeness🔗

A category is complete if it admits limits for diagrams of arbitrary shape. However, in the presence of excluded middle, if a category admits products indexed by its class of morphisms, then it is automatically a poset. Since excluded middle is independent of type theory, we can not prove that any non-thin categories have arbitrary limits.

Instead, categories are complete with respect to a pair of universes: A category is $(o, \ell)$-complete if it has limits for any diagram indexed by a precategory with objects in $\mathrm{Type}\ o$ and morphisms in $\mathrm{Type}\ \ell$.

is-complete : ∀ {oc ℓc} o ℓ → Precategory oc ℓc → Type _
is-complete oj ℓj C = ∀ {J : Precategory oj ℓj} (F : Functor J C) → Limit F

While this condition might sound very strong, and thus that it would be hard to come by, it turns out we can get away with only two fundamental types of limits: products and equalisers. In order to construct the limit for a diagram of shape $\mathcal{J}$, we will require products indexed by $\mathcal{J}$’s type of objects and by its type of morphisms.

  limit-as-equaliser-of-product
    : ∀ {oj ℓj} {J : Precategory oj ℓj}
    → has-products-indexed-by C (Precategory.Ob J)
    → has-products-indexed-by C (Precategory.Mor J)
    → has-equalisers C
    → (F : Functor J C) → Limit F
  limit-as-equaliser-of-product {oj} {ℓj} {J} has-Ob-prod has-Mor-prod has-eq F =
    to-limit (to-is-limit lim) where

Given a diagram $F : \mathcal{J} \to \mathcal{C}$, we start by building the product of all the objects appearing in the diagram.

    Obs : Indexed-product C λ o → F₀ o
    Obs = has-Ob-prod _

Our limit will arise as a subobject of this product-of-objects, namely the equaliser of two carefully chosen morphisms.

As a guiding example, the pullback of $f : A \to C$ and $g : B \to C$ should be the subobject of $A \times B \times C$ consisting of triples $(a, b, c)$ such that $f(a) = c = g(b)$. In full generality, for each arrow $f : A \to C$ in our diagram, we should have that projecting out the $C$th component of our product should give the same result as projecting out the $A$th component and postcomposing with $f$.

This suggests to build another indexed product of all the codomains of arrows in the diagram, taking the first morphism to be the projection of the codomain and the second morphism to be the projection of the domain postcomposed with $f$:

    Cod : Indexed-product C {Idx = J.Mor} λ (a , b , f) → F₀ b
    Cod = has-Mor-prod _

    s t : C.Hom (Obs .ΠF) (Cod .ΠF)
    s = Cod .tuple λ (a , b , f) → F₁ f C.∘ Obs .π a
    t = Cod .tuple λ (a , b , f) → Obs .π b

    eq : Equaliser C s t
    eq = has-eq _ _

    lim : make-is-limit F (eq .apex)

    lim .ψ c = Obs .π c C.∘ eq .equ
    lim .commutes {a} {b} f =
      F₁ f C.∘ Obs .π a C.∘ eq .equ            ≡˘⟨ C.extendl (Cod .commute) ⟩
      Cod .π (a , b , f) C.∘ ⌜ s C.∘ eq .equ ⌝ ≡⟨ ap! (eq .equal) ⟩
      Cod .π (a , b , f) C.∘ t C.∘ eq .equ     ≡⟨ C.pulll (Cod .commute) ⟩
      Obs .π b C.∘ eq .equ                     ∎
    lim .universal {x} e comm = eq .universal comm' where
      e' : C.Hom x (Obs .ΠF)
      e' = Obs .tuple e
      comm' : s C.∘ e' ≡ t C.∘ e'
      comm' = Indexed-product.unique₂ Cod λ i@(a , b , f) →
        Cod .π i C.∘ s C.∘ e'        ≡⟨ C.extendl (Cod .commute) ⟩
        F₁ f C.∘ ⌜ Obs .π a C.∘ e' ⌝ ≡⟨ ap! (Obs .commute) ⟩
        F₁ f C.∘ e a                 ≡⟨ comm f ⟩
        e b                          ≡˘⟨ Obs .commute ⟩
        Obs .π b C.∘ e'              ≡˘⟨ C.pulll (Cod .commute) ⟩
        Cod .π i C.∘ t C.∘ e'        ∎
    lim .factors {j} e comm =
      (Obs .π j C.∘ eq .equ) C.∘ lim .universal e comm ≡⟨ C.pullr (eq .factors) ⟩
      Obs .π j C.∘ Obs .tuple e                        ≡⟨ Obs .commute ⟩
      e j                                              ∎
    lim .unique e comm u' fac = eq .unique $ Obs .unique _
      λ i → C.assoc _ _ _ ∙ fac i

This implies that a category with equalisers and large enough indexed products has all limits.

  products+equalisers→complete
    : ∀ {oj ℓj}
    → has-indexed-products C (oj ⊔ ℓj)
    → has-equalisers C
    → is-complete oj ℓj C
  products+equalisers→complete {oj} {ℓj} has-prod has-eq =
    limit-as-equaliser-of-product
      (λ _ → Lift-Indexed-product C ℓj (has-prod _))
      (λ _ → has-prod _)
      has-eq