open import Cat.Instances.Shape.Terminal
open import Cat.Instances.Shape.Join
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Instances.Slice
open import Cat.Prelude

open import Data.Sum

import Cat.Reasoning

open Functor

module Cat.Instances.Slice.Limit where


# Arbitrary limits in slicesπ

Suppose we have some really weird diagram in a slice category, like the one below. Well, alright, itβs not that weird, but itβs not a pullback or a terminal object, so we donβt a priori know how to compute its limit in the slice.

The observation that will let us compute a limit for this diagram is inspecting the computation of products in a slice. To compute the product of and we had to pass to a pullback of in β which we had assumed exists. But! Take a look at what that diagram looks like:

We βexplodedβ a diagram of shape to one of shape This process can be described in a way easier to generalise: We βexplodedβ our diagram to one indexed by a category which contains contains an extra point, and has a unique map between each object of β the join of these categories.

module
_ {o β o' β'} {C : Precategory o β} {J : Precategory o' β'} {o : β C β}
(F : Functor J (Slice C o))
where

open Terminal
open /-Obj
open /-Hom

private
module C   = Cat.Reasoning C
module J   = Cat.Reasoning J
module C/o = Cat.Reasoning (Slice C o)
module F = Functor F


Generically, if we have a diagram we can βexplodeβ this into a diagram compute the limit in then pass back to the slice category.

    F' : Functor (J β β€Cat) C
F' .Fβ (inl x) = F.β x .domain
F' .Fβ (inr x) = o
F' .Fβ {inl x} {inl y} (lift f) = F.β f .map
F' .Fβ {inl x} {inr y} _ = F.β x .map
F' .Fβ {inr x} {inr y} (lift h) = C.id
F' .F-id {inl x} = ap map F.F-id
F' .F-id {inr x} = refl
F' .F-β {inl x} {inl y} {inl z} (lift f) (lift g) = ap map (F.F-β f g)
F' .F-β {inl x} {inl y} {inr z} (lift f) (lift g) = sym (F.Fβ g .commutes)
F' .F-β {inl x} {inr y} {inr z} (lift f) (lift g) = C.introl refl
F' .F-β {inr x} {inr y} {inr z} (lift f) (lift g) = C.introl refl

limit-aboveβlimit-in-slice : Limit F' β Limit F
limit-aboveβlimit-in-slice lims = to-limit (to-is-limit lim) where
module lims = Limit lims
open make-is-limit

apex : C/o.Ob
apex = cut (lims.Ο (inr tt))

nadir : (j : J.Ob) β /-Hom apex (F .Fβ j)
nadir j .map = lims.Ο (inl j)
nadir j .commutes = lims.commutes (lift tt)

module Cone
{x : C/o.Ob}
(eps : (j : J.Ob) β C/o.Hom x (F .Fβ j))
(p : β {i j : J.Ob} β (f : J.Hom i j) β F .Fβ f C/o.β eps i β‘ eps j)
where

Ο : (j : J.Ob β β€) β C.Hom (x .domain) (F' .Fβ j)
Ο (inl j) = eps j .map
Ο (inr _) = x .map

Ο-commutes
: β {i j : J.Ob β β€}
β (f : βHom J β€Cat i j)
β F' .Fβ f C.β Ο i β‘ Ο j
Ο-commutes {inl i} {inl j} (lift f) = ap map (p f)
Ο-commutes {inl i} {inr j} (lift f) = eps i .commutes
Ο-commutes {inr i} {inr x} (lift f) = C.idl _

Ο-factor
: β (other : /-Hom x apex)
β (β j β nadir j C/o.β other β‘ eps j)
β (j : J.Ob β β€)
β lims.Ο j C.β other .map β‘ Ο j
Ο-factor other q (inl j) = ap map (q j)
Ο-factor other q (inr tt) = other .commutes

lim : make-is-limit F apex
lim .commutes f = ext (lims.commutes (lift f))
lim .universal {x} eps p .map =
lims.universal (Cone.Ο eps p) (Cone.Ο-commutes eps p)
lim .universal eps p .commutes =
lims.factors _ _
lim .factors eps p = ext (lims.factors _ _)
lim .unique eps p other q = ext \$
lims.unique _ _ (other .map) (Cone.Ο-factor eps p other q)


In particular, if a category is complete, then so are its slices:

is-completeβslice-is-complete
: β {β o o' β'} {C : Precategory o β} {c : β C β}
β is-complete o' β' C
β is-complete o' β' (Slice C c)
is-completeβslice-is-complete lims F = limit-aboveβlimit-in-slice F (lims _)