open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Prelude

import Cat.Reasoning

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.

private variable
oβ oβ hβ hβ : Level

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

  private unquoteDecl eqv = declare-record-iso eqv (quote Cone-hom)

Cone-hom-path : β {x y} {f g : Cone-hom x y} β Cone-hom.hom f β‘ Cone-hom.hom g β f β‘ g
Cone-hom-path p i .Cone-hom.hom = p i
Cone-hom-path {x = x} {y} {f} {g} p i .Cone-hom.commutes o j =
is-setβsquarep (Ξ» i j β C.Hom-set _ _)
(Ξ» j β Cone.Ο y o C.β p j) (f .Cone-hom.commutes o) (g .Cone-hom.commutes o) refl i j


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 _ _ _)

    cat .Hom-set x y = Isoβis-hlevel! 2 eqv

open _=>_


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)))

  open Ran

Terminal-coneβLimit : Terminal Cones β Limit F
Terminal-coneβLimit x .Ext     = _
Terminal-coneβLimit x .eps     = _
Terminal-coneβLimit x .has-ran = is-terminal-coneβis-limit (x .Terminal.hasβ€)

LimitβTerminal-cone : Limit F β Terminal Cones
LimitβTerminal-cone x .Terminal.top  = _
LimitβTerminal-cone x .Terminal.hasβ€ = is-limitβis-terminal-cone
(Limit.has-limit x)