module Cat.Diagram.Limit.Cone where

Limits via conesπŸ”—

As noted in the main page on limits, most introductory material defines limits via a mathematical widget called a cone.

module _ {J : Precategory o₁ h₁} {C : Precategory oβ‚‚ hβ‚‚} (F : Functor J C) where
  private
    import Cat.Reasoning J as J
    import Cat.Reasoning C as C
    module F = Functor F

  record Cone : Type (o₁ βŠ” oβ‚‚ βŠ” h₁ βŠ” hβ‚‚) where
    no-eta-equality

A Cone over is given by an object (the apex) together with a family of maps ψ β€” one for each object in the indexing category J β€” such that β€œeverything in sight commutes”.

    field
      apex     : C.Ob
      ψ        : (x : J.Ob) β†’ C.Hom apex (F.β‚€ x)

For every map in the indexing category, we require that the diagram below commutes. This encompasses β€œeverything” since the only non-trivial composites that can be formed with the data at hand are of the form

      commutes : βˆ€ {x y} (f : J.Hom x y) β†’ F.₁ f C.∘ ψ x ≑ ψ y

These non-trivial composites consist of following the left leg of the diagram below, followed by the bottom leg. For it to commute, that path has to be the same as following the right leg.

Since paths in Hom-spaces are propositions, to test equality of cones, it suffices for the apices to be equal, and for their to assign equal morphisms for every object in the shape category.

  Cone-path : {x y : Cone}
        β†’ (p : Cone.apex x ≑ Cone.apex y)
        β†’ (βˆ€ o β†’ PathP (Ξ» i β†’ C.Hom (p i) (F.β‚€ o)) (Cone.ψ x o) (Cone.ψ y o))
        β†’ x ≑ y
  Cone-path p q i .Cone.apex = p i
  Cone-path p q i .Cone.ψ o = q o i
  Cone-path {x = x} {y} p q i .Cone.commutes {x = a} {y = b} f =
    is-propβ†’pathp (Ξ» i β†’ C.Hom-set _ _ (F.₁ f C.∘ q a i) (q b i))
      (x .commutes f) (y .commutes f) i
    where open Cone

Cone mapsπŸ”—

  record Cone-hom (x y : Cone) : Type (o₁ βŠ” hβ‚‚) where
    no-eta-equality
    constructor cone-hom

A Cone homomorphism is – like the introduction says – a map hom in the ambient category between the apices, such that β€œeverything in sight commutes”. Specifically, for any choice of object in the index category, the composition of hom with the domain cone’s ψ (at that object) must be equal to the codomain’s ψ.

    field
      hom      : C.Hom (Cone.apex x) (Cone.apex y)
      commutes : βˆ€ o β†’ Cone.ψ y o C.∘ hom ≑ Cone.ψ x o

Since cone homomorphisms are morphisms in the underlying category with extra properties, we can lift the laws from the underlying category to the category of Cones. The definition of compose is the enlightening part, since we have to prove that two cone homomorphisms again preserve all the commutativities.

  Cones : Precategory _ _
  Cones = cat where
    open Precategory

    compose : {x y z : _} β†’ Cone-hom y z β†’ Cone-hom x y β†’ Cone-hom x z
    compose {x} {y} {z} F G = r where
      open Cone-hom
      r : Cone-hom x z
      r .hom = hom F C.∘ hom G
      r .commutes o =
        Cone.ψ z o C.∘ hom F C.∘ hom G β‰‘βŸ¨ C.pulll (commutes F o) βŸ©β‰‘
        Cone.ψ y o C.∘ hom G           β‰‘βŸ¨ commutes G o βŸ©β‰‘
        Cone.ψ x o                     ∎

    cat : Precategory _ _
    cat .Ob = Cone
    cat .Hom = Cone-hom
    cat .id = record { hom = C.id ; commutes = Ξ» _ β†’ C.idr _ }
    cat ._∘_ = compose
    cat .idr f = Cone-hom-path (C.idr _)
    cat .idl f = Cone-hom-path (C.idl _)
    cat .assoc f g h = Cone-hom-path (C.assoc _ _ _)

Terminal cones as limitsπŸ”—

Note that cones over some diagram contain the exact same data as natural transformations from a constant functor to To obtain a limit, all we need is a way of stating that a given cone is universal. In particular, the terminal object in the category of cones over a diagram (if it exists!) is the limit of

The proof here is just shuffling data around: this is not totally surprising, as both constructions contain the same data, just organized differently.

  Cone→cone : (K : Cone) → Const (Cone.apex K) => F
  Coneβ†’cone K .Ξ· = K .Cone.ψ
  Coneβ†’cone K .is-natural x y f = C.idr _ βˆ™ sym (K .Cone.commutes f)

  is-terminal-cone→is-limit
    : βˆ€ {K : Cone}
    β†’ is-terminal Cones K
    → is-limit F (Cone.apex K) (Cone→cone K)
  is-terminal-cone→is-limit {K = K} term = isl where
    open Cone-hom
    open is-ran
    open Cone

    isl : is-ran _ F _ (Cone→cone K)
    isl .Οƒ {M = M} Ξ± = nt where
      Ξ±' : Cone
      Ξ±' .apex = M .Functor.Fβ‚€ tt
      α' .ψ x = α .η x
      Ξ±' .commutes f = sym (Ξ± .is-natural _ _ f) βˆ™ C.elimr (M .Functor.F-id)

      nt : M => !Const (K .apex)
      nt .Ξ· x = term Ξ±' .centre .hom
      nt .is-natural tt tt tt = C.elimr (M .Functor.F-id) βˆ™ C.introl refl
    isl .Οƒ-comm = ext Ξ» x β†’ term _ .centre .commutes _
    isl .Οƒ-uniq {Οƒ' = Οƒ'} x = ext Ξ» _ β†’ ap hom $ term _ .paths Ξ» where
      .hom        β†’ Οƒ' .Ξ· _
      .commutes _ β†’ sym (x Ξ·β‚š _)

The inverse direction of this equivalence also consists of packing and unpacking data.

  is-limit→is-terminal-cone
    : βˆ€ {x} {eps : Const x => F}
    β†’ (L : is-limit F x eps)
    β†’ is-terminal Cones (record { commutes = is-limit.commutes L })
  is-limit→is-terminal-cone {x = x} L K = term where
    module L = is-limit L
    module K = Cone K
    open Cone-hom

    term : is-contr (Cone-hom K _)
    term .centre .hom =
      L.universal K.ψ K.commutes
    term .centre .commutes _ =
      L.factors K.ψ K.commutes
    term .paths f =
      Cone-hom-path (sym (L.unique K.ψ K.commutes (f .hom) (f .commutes)))