open import Cat.Instances.Shape.Terminal
open import Cat.Instances.Shape.Join
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Discrete
open import Cat.Instances.Functor
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Functor.Base
open import Cat.Univalent
open import Cat.Prelude

open import Data.Sum

import Cat.Reasoning

module Cat.Instances.Slice where

Slice categories🔗

When working in Sets\sets, there is an evident notion of family indexed by a set: a family of sets (Fi)i∈I(F_i)_{i \in I} is equivalently a functor [Disc(I),Sets][\id{Disc}(I), \sets], where we have equipped the set II with the discrete category structure. This works essentially because of the discrete category-global sections adjunction, but in general this can not be applied to other categories, like Groups\id{Groups}. How, then, should we work with “indexed families” in general categories?

The answer is to consider, rather than families themselves, the projections from their total spaces as the primitive objects. A family indexed by II, then, would consist of an object AA and a morphism t:A→It : A \to I, where AA is considered as the “total space” object and tt assigns gives the “tag” of each object. By analysing how tt pulls back along maps B→IB \to I, we recover a notion of “fibres”: the collection with index ii can be recovered as the pullback t∗it^*i.

Note that, since the discussion in the preceding paragraph made no mention of the category of sets, it applies in any category! More generally, for any category C\ca{C} and object c:Cc : \ca{C}, we have a category of objects indexed by cc, the slice category C/c\ca{C}/c. An object of “the slice over cc” is given by an object d:Cd : \ca{C} to serve as the domain, and a map f:d→cf : d \to c.

  record /-Obj (c : C.Ob) : Type (o ⊔ ℓ) where
    constructor cut
      {domain} : C.Ob
      map      : C.Hom domain c

A map between f:a→cf : a \to c and g:b→cg : b \to c is given by a map h:a→bh : a \to b such that the triangle below commutes. Since we’re thinking of ff and gg as families indexed by cc, commutativity of the triangle says that the map hh “respects reindexing,” or less obliquely “preserves fibres.”

  record /-Hom (a b : /-Obj c) : Type ℓ where
      module a = /-Obj a
      module b = /-Obj b
      map      : C.Hom a.domain b.domain
      commutes : C.∘ map ≡

The slice category C/c\ca{C}/c is given by the /-Obj and /-Homs.

Slice : (C : Precategory o ℓ) → Precategory.Ob C → Precategory _ _
Slice C c = precat where
  import Cat.Reasoning C as C
  open Precategory
  open /-Hom
  open /-Obj

  precat : Precategory _ _
  precat .Ob = /-Obj {C = C} c
  precat .Hom = /-Hom
  precat .Hom-set x y = /-Hom-is-set
  precat .id .map      =
  precat .id .commutes = C.idr _

For composition in the slice over cc, note that if the triangle (the commutativity condition for ff) and the rhombus (the commutativity condition for gg) both commute, then so does the larger triangle (the commutativity for g∘fg \circ f).

  precat ._∘_ {x} {y} {z} f g = fog where
    module f = /-Hom f
    module g = /-Hom g
    fog : /-Hom _ _
    fog .map = C.∘
    fog .commutes =
      z .map C.∘ C.∘ ≡⟨ C.pulll f.commutes ⟩≡
      y .map C.∘           ≡⟨ g.commutes ⟩≡
      x .map                     ∎
  precat .idr f = /-Hom-path (C.idr _)
  precat .idl f = /-Hom-path (C.idl _)
  precat .assoc f g h = /-Hom-path (C.assoc _ _ _)


We discuss some limits in the slice of C\ca{C} over cc. First, every slice category has a terminal object, given by the identity map id:c→c\id{id} : c \to c.

module _ {o ℓ} {C : Precategory o ℓ} {c : Precategory.Ob C} where
  import Cat.Reasoning C as C
  import Cat.Reasoning (Slice C c) as C/c
  open /-Hom
  open /-Obj

  Slice-terminal-object : is-terminal (Slice C c) (cut
  Slice-terminal-object obj .centre .map = obj .map
  Slice-terminal-object obj .centre .commutes = C.idl _
  Slice-terminal-object obj .paths other =
    /-Hom-path (sym (other .commutes) ∙ C.idl _)

Products in a slice category are slightly more complicated, but recall that another word for pullback is “fibred product.” Indeed, in the pullback page we noted that the pullback of X→ZX \to Z and Y→ZY \to Z is exactly the product of those maps in the slice over ZZ.

Suppose we have a pullback diagram like the one below, i.e., a limit of the diagram a→fc←gba \xrightarrow{f} c \xleftarrow{g} b, in the category C\ca{C}. We’ll show that it’s also a limit of the (discrete) diagram consisting of ff and gg, but now in the slice category C/c\ca{C}/c.

For starters, note that we have seemingly “two” distinct choices for maps a×cb→ca \times_c b \to c, but since the square above commutes, either one will do. For definiteness, we go with the composite f∘π1f \circ \pi_1.

    _ {f g : /-Obj c} {Pb : C.Ob} {π₁ : C.Hom Pb (f .domain)}
                                  {π₂ : C.Hom Pb (g .domain)}
      (pb : is-pullback C {X = f .domain} {Z = c} {Y = g .domain} {P = Pb}
        π₁ (map {_} {_} {C} {c} f) π₂ (map {_} {_} {C} {c} g))
    private module pb = is-pullback pb

    is-pullback→product-over : C/c.Ob
    is-pullback→product-over = cut (f .map C.∘ π₁)

Now, by commutativity of the square, the maps π1\pi_1 and π2\pi_2 in the diagram above extend to maps (f∘π1)→f(f \circ \pi_1) \to f and (f∘π1)→g(f \circ \pi_1) \to g in C/c\ca{C}/c. Indeed, note that by scribbling a red line across the diagonal of the diagram, we get the two needed triangles as the induced subdivisions.

    is-pullback→π₁ : C/c.Hom is-pullback→product-over f
    is-pullback→π₁ .map      = π₁
    is-pullback→π₁ .commutes i = f .map C.∘ π₁

    is-pullback→π₂ : C/c.Hom is-pullback→product-over g
    is-pullback→π₂ .map        = π₂
    is-pullback→π₂ .commutes i = pb.square (~ i)

    open is-product

Unfolding what it means for a diagram to be a universal cone over the discrete diagram consisting of ff and gg in the category C/c\ca{C}/c, we see that it is exactly the data of the pullback of ff and gg in C\ca{C}, as below:

      : is-product (Slice C c) is-pullback→π₁ is-pullback→π₂
    is-pullback→is-fibre-product .⟨_,_⟩ {Q} /f /g = factor
        module f = /-Hom /f
        module g = /-Hom /g

        factor : C/c.Hom Q _
        factor .map = pb.limiting (f.commutes ∙ sym g.commutes)
        factor .commutes =
          (f .map C.∘ π₁) C.∘ pb.limiting _ ≡⟨ C.pullr pb.p₁∘limiting ⟩≡
          f .map C.∘                  ≡⟨ f.commutes ⟩≡
          Q .map                            ∎

    is-pullback→is-fibre-product .π₁∘factor = /-Hom-path pb.p₁∘limiting
    is-pullback→is-fibre-product .π₂∘factor = /-Hom-path pb.p₂∘limiting
    is-pullback→is-fibre-product .unique other p q =
      /-Hom-path (pb.unique (ap map p) (ap map q))

    : ∀ {f g : /-Obj c}
    → Pullback C (f .map) (g .map) → Product (Slice C c) f g
  Pullback→Fibre-product pb .Product.apex = _
  Pullback→Fibre-product pb .Product.π₁ = _
  Pullback→Fibre-product pb .Product.π₂ = _
  Pullback→Fibre-product pb .Product.has-is-product =
    is-pullback→is-fibre-product (pb .Pullback.has-is-pb)

While products and terminal objects in C/X\ca{C}/X do not correspond to those in C\ca{C}, pullbacks (and equalisers) are precisely equivalent. A square is a pullback in C/X\ca{C}/X iff. the square consisting of their underlying objects and maps is a square in C\ca{C}.

The “if” direction (what is pullback-above→pullback-below) in the code is essentially an immediate consequence of the fact that equality of morphisms in C/X\ca{C}/X may be tested in C\ca{C}, but we do have to take some care when extending the “limiting” morphism back down to the slice category (see the calculation marked {- * -}).

module _ where
  open /-Obj
  open /-Hom

    : ∀ {o ℓ} {C : Precategory o ℓ} {X : Precategory.Ob C}
    → ∀ {P A B c} {p1 f p2 g}
    → is-pullback C (p1 .map) (f .map) (p2 .map) (g .map)
    → is-pullback (Slice C X) {P} {A} {B} {c} p1 f p2 g
  pullback-above→pullback-below {C = C} {P = P} {a} {b} {c} {p1} {f} {p2} {g} pb
    = pb′ where
      open is-pullback
      open Cat.Reasoning C

      pb′ : is-pullback (Slice _ _) _ _ _ _
      pb′ .square = /-Hom-path (pb .square)
      pb′ .limiting p .map = pb .limiting (ap map p)
      pb′ .limiting {P'} {p₁' = p₁'} p .commutes =
        (c .map ∘ pb .limiting (ap map p))           ≡˘⟨ (pulll (p1 .commutes)) ⟩≡˘
        (P .map ∘ p1 .map ∘ pb .limiting (ap map p)) ≡⟨ ap (_ ∘_) (pb .p₁∘limiting) ⟩≡
        (P .map ∘ p₁' .map)                          ≡⟨ p₁' .commutes ⟩≡
        P' .map                                      ∎ {- * -}
      pb′ .p₁∘limiting = /-Hom-path (pb .p₁∘limiting)
      pb′ .p₂∘limiting = /-Hom-path (pb .p₂∘limiting)
      pb′ .unique p q = /-Hom-path (pb .unique (ap map p) (ap map q))

    : ∀ {o ℓ} {C : Precategory o ℓ} {X : Precategory.Ob C}
    → ∀ {P A B c} {p1 f p2 g}
    → is-pullback (Slice C X) {P} {A} {B} {c} p1 f p2 g
    → is-pullback C (p1 .map) (f .map) (p2 .map) (g .map)
  pullback-below→pullback-above {C = C} {P = P} {p1 = p1} {f} {p2} {g} pb = pb′ where
    open Cat.Reasoning C
    open is-pullback
    pb′ : is-pullback _ _ _ _ _
    pb′ .square = ap map (pb .square)
    pb′ .limiting {P′ = P'} {p₁'} {p₂'} p =
      pb .limiting {P′ = cut (P .map ∘ p₁')}
        {p₁' = record { map = p₁' ; commutes = refl }}
        {p₂' = record { map = p₂' ; commutes = sym (pulll (g .commutes))
                                             ∙ sym (ap (_ ∘_) p)
                                             ∙ pulll (f .commutes)
        (/-Hom-path p)
    pb′ .p₁∘limiting = ap map $ pb .p₁∘limiting
    pb′ .p₂∘limiting = ap map $ pb .p₂∘limiting
    pb′ .unique p q = ap map $ pb .unique
      {lim' = record { map = _ ; commutes = sym (pulll (p1 .commutes)) ∙ ap (_ ∘_) p }}
      (/-Hom-path p) (/-Hom-path q)

Slices of Sets🔗

We now prove the correspondence between slices of Sets\sets and functor categories into Sets\sets, i.e. the corresponding between indexing and slicing mentioned in the first paragraph.

module _ {I : Set ℓ} where
  open /-Obj
  open /-Hom

We shall prove that the functor Total-space, defined below, is an equivalence of categories, i.e. that it is fully faithful and essentially surjective. But first, we must define the functor! Like its name implies, it maps the functor F:I→SetsF : I → \sets to the first projection map fst:∑F→I\id{fst} : \sum F \to I.

  Total-space : Functor Cat[ Disc′ I , Sets ℓ ] (Slice (Sets ℓ) I)
  Total-space .F₀ F .domain = Σ (∣_∣ ⊙ F₀ F)
                            , Σ-is-hlevel 2 (I .is-tr) (is-tr ⊙ F₀ F)
  Total-space .F₀ F .map = fst

  Total-space .F₁ nt .map (i , x) = i , nt .η _ x
  Total-space .F₁ nt .commutes    = refl

  Total-space .F-id    = /-Hom-path refl
  Total-space .F-∘ _ _ = /-Hom-path refl

To prove that the Total-space functor is fully faithful, we will exhibit a quasi-inverse to its action on morphisms. Given a fibre-preserving map between fst:∑F→I\id{fst} : \sum F \to I and fst:∑G→I\id{fst} : \sum G \to I, we recover a natural transformation between FF and GG. The hardest part is showing naturality, where we use path induction.

  Total-space-is-ff : is-fully-faithful Total-space
  Total-space-is-ff {f1} {f2} = is-iso→is-equiv
    (iso from linv (λ x → Nat-path (λ x → funext (λ _ → transport-refl _))))
      from : /-Hom (Total-space .F₀ f1) (Total-space .F₀ f2) → f1 => f2
      from mp = nt where
        eta : ∀ i → ∣ F₀ f1 i ∣ → ∣ F₀ f2 i ∣
        eta i j =
          subst (∣_∣ ⊙ F₀ f2) (happly (mp .commutes) _) (mp .map (i , j) .snd)

        nt : f1 => f2
        nt .η = eta
        nt .is-natural _ _ f =
          J (λ _ p → eta _ ⊙ F₁ f1 p ≡ F₁ f2 p ⊙ eta _)
            (ap (eta _ ⊙_) (F-id f1) ∙ sym (ap (_⊙ eta _) (F-id f2)))

For essential surjectivity, given a map f:X→If : X \to I, we recover a family of sets (f∗i)i∈I(f^*i)_{i \in I} by taking the fibre of ff over each point, which cleanly extends to a functor. To show that the Total-space of this functor is isomorphic to the map we started with, we use one of the auxilliary lemmas used in the construction of an object classifier: Total-equiv. This is cleaner than exhibiting an isomorphism directly, though it does involve an appeal to univalence.

  Total-space-is-eso : is-split-eso Total-space
  Total-space-is-eso fam = functor , path→iso _ path
      functor : Functor _ _
      functor .F₀ i = fibre (fam .map) i
                    , Σ-is-hlevel 2 (fam .domain .is-tr)
                                    λ _ → is-prop→is-set (I .is-tr _ _)
      functor .F₁ p = subst (fibre (fam .map)) p
      functor .F-id = funext transport-refl
      functor .F-∘ f g = funext (subst-∙ (fibre (fam .map)) _ _)

      path : F₀ Total-space functor ≡ fam
      path = /-Obj-path (n-ua (Total-equiv _  e⁻¹)) (ua→ λ a → sym (a .snd .snd))

Slices preserve univalence🔗

An important property of slice categories is that they preserve univalence. This can be seen intuitively: If C\ca{C} is a univalent category, then let a,b,ca, b, c be some objects, with the pairs (a,f)(a, f) and (b,g)(b, g) objects in the slice C/c\ca{C}/c. An isomorphism h:(a,f)≅(b,g)h : (a, f) \cong (b, g) induces an identification a≡ba \equiv b, which extends to an identification (a,f)≡(b,g)(a, f) \equiv (b, g) since h∘g=fh \circ g = f.

module _ {C : Precategory o ℓ} {o : Precategory.Ob C} (isc : is-category C) where
    module C   = Cat.Reasoning C
    module C/o = Cat.Reasoning (Slice C o)
    module Cu  = Cat.Univalent C

    open /-Obj
    open /-Hom
    open C/o._≅_
    open C._≅_

  slice-is-category : is-category (Slice C o)
  slice-is-category A .centre = A , C/
  slice-is-category A .paths (B , isom) = Σ-pathp A≡B eql where
    Ad≡Bd : A .domain ≡ B .domain
    Ad≡Bd = Cu.iso→path isc
      (C.make-iso (isom .to .map) (isom .from .map)
        (ap map (C/o._≅_.invl isom)) (ap map (C/o._≅_.invr isom)))

    Af≡Bf : PathP (λ i → C.Hom (Ad≡Bd i) o) (A .map) (B .map)
    Af≡Bf = Cu.Hom-pathp-refll-iso isc (isom .from .commutes)

    A≡B = /-Obj-path Ad≡Bd Af≡Bf

    eql : PathP (λ i → A C/o.≅ A≡B i) C/ isom
    eql = C/o.≅-pathp refl A≡B
      (/-Hom-pathp _ _ (Cu.Hom-pathp-reflr-iso isc (C.idr _)))

Arbitrary limits in slices🔗

Suppose we have some really weird diagram F:J→C/cF : \ca{J} \to \ca{C}/c, 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 it.

The observation that will let us compute a limit for this diagram is inspecting the computation of products in slice categories, above. To compute the product of (a,f)(a, f) and (b,g)(b, g), we had to pass to a pullback of a→fc←ba \xto{f} c \xot{b} in C\ca{C} — which we had assumed exists. But! Take a look at what that diagram looks like:

We “exploded” a diagram of shape ∙∙\bullet \quad \bullet to one of shape ∙→∙←∙\bullet \to \bullet \ot \bullet. This process can be described in a way easier to generalise: We “exploded” our diagram F:{∗,∗}→C/cF : \{*,*\} \to \ca{C}/c 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.

Generically, if we have a diagram F:J→C/cF : J \to \ca{C}/c, we can “explode” this into a diagram F′:(J⋆{∗})→CF' : (J \star \{*\}) \to \ca{C}, compute the limit in C\ca{C}, 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) =
    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 = lim where
    module lim = Terminal lims
    module limob = Cone

    nadir : Cone F
    nadir .apex .domain = limob.apex
    nadir .apex .map = limob.ψ (inr tt)
    nadir .ψ x .map = limob.ψ (inl x)
    nadir .ψ x .commutes = limob.commutes (lift tt)
    nadir .commutes f = /-Hom-path (limob.commutes (lift f))

    lim : Limit F
    lim .top = nadir
    lim .has⊤ other = contr ch cont where
      other′ : Cone F′
      other′ .apex = other .apex .domain
      other′ .ψ (inl x) = other .ψ x .map
      other′ .ψ (inr tt) = other .apex .map
      other′ .commutes {inl x} {inl y} (lift f) = ap map (other .commutes f)
      other′ .commutes {inl x} {inr y} (lift f) = other .ψ x .commutes
      other′ .commutes {inr x} {inr y} (lift f) = C.idl _

      module cont = is-contr (lim.has⊤ other′)
      ch : Cone-hom F other nadir
      ch .hom .map = cont.centre .hom
      ch .hom .commutes = cont.centre .commutes (inr tt)
      ch .commutes o = /-Hom-path (cont.centre .commutes (inl o))

      cont : ∀ c → ch ≡ c
      cont c = Cone-hom-path _ (/-Hom-path (ap hom uniq)) where
        c′ : Cone-hom F′ other′
        c′ .hom = c .hom .map
        c′ .commutes (inl x) = ap map (c .commutes x)
        c′ .commutes (inr tt) = c .hom .commutes

        uniq = cont.paths c′

In particular, if a category C\ca{C} is complete, then so are its slices:

  : ∀ {ℓ o ℓ′} {C : Precategory o ℓ} {c : Precategory.Ob 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 _)