module Cat.Instances.Slice where

Slice categories🔗

When working in Sets\mathbf{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][\mathrm{Disc}(I), \mathbf{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\mathrm{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\mathcal{C} and object c:Cc : \mathcal{C}, we have a category of objects indexed by cc, the slice category C/c\mathcal{C}/c. An object of “the slice over cc” is given by an object d:Cd : \mathcal{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 ≡
  /-Obj-path : ∀ {c} {x y : /-Obj c}
             → (p : x ./-Obj.domain ≡ y ./-Obj.domain)
             → PathP (λ i → C.Hom (p i) c) (x ./ (y ./
             → x ≡ y
  /-Obj-path p q i ./-Obj.domain = p i
  /-Obj-path p q i ./ = q i

  /-Hom-pathp : ∀ {c a a' b b'} (p : a ≡ a') (q : b ≡ b')
                {x : /-Hom {c = c} a b} {y : /-Hom a' b'}
              → PathP (λ i → C.Hom (p i ./-Obj.domain) (q i ./-Obj.domain))
                        (x ./ (y ./
              → PathP (λ i → /-Hom (p i) (q i)) x y
  /-Hom-pathp p q {x} {y} r = path where
    open /-Hom

    path : PathP (λ i → /-Hom (p i) (q i))  x y
    path i .map = r i
    path i .commutes =
        (λ i → C.Hom-set (p i ./-Obj.domain) _
                         (q i ./ C.∘ r i) (p i ./
        (x .commutes) (y .commutes) i

  /-Hom-path : ∀ {c a b} {x y : /-Hom {c = c} a b}
             → x ./ ≡ y ./
             → x ≡ y
  /-Hom-path = /-Hom-pathp refl refl

    : ∀ {c a b ℓ} ⦃ sa : Extensional (C.Hom (/-Obj.domain a) (/-Obj.domain b)) ℓ ⦄
    → Extensional (/-Hom {c = c} a b) ℓ
  Extensional-/-Hom ⦃ sa ⦄ = injection→extensional! (/-Hom-pathp refl refl) sa

    extensionality-/-hom : ∀ {c a b} → Extensionality (/-Hom {c = c} a b)
    extensionality-/-hom = record { lemma = quote Extensional-/-Hom }

  private unquoteDecl eqv = declare-record-iso eqv (quote /-Hom)

    /-Hom-is-set : ∀ {c a b} → is-set (/-Hom {c = c} a b)
    /-Hom-is-set {a = a} {b} = hl where abstract
      open C.HLevel-instance

      hl : is-set (/-Hom a b)
      hl = Iso→is-hlevel 2 eqv (hlevel 2)

The slice category C/c\mathcal{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 = ext (C.idr _)
  precat .idl f = ext (C.idl _)
  precat .assoc f g h = ext (C.assoc _ _ _)

Finite limits🔗

We discuss the construction of finite limits in the slice of C/c\mathcal{C}/c. First, every slice category has a terminal object, given by the identity map id⁡:c→c\operatorname{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 =
    ext (sym (other .commutes) ∙ C.idl _)

  Slice-terminal-object : Terminal (Slice C c)
  Slice-terminal-object  = _
  Slice-terminal-object .Terminal.has⊤ = Slice-terminal-object'

Products in a slice category are slightly more complicated — but if you’ve ever heard a pullback referred to as a “fibre(d) product”, you already know what we’re up to! Indeed, in defining pullback diagrams, we noted that the pullback of f:X→Zf : X \to Z and g:Y→Zg : Y \to Z is exactly the product f×gf \times g 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\mathcal{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\mathcal{C}/c.

For starters, we have to define a map a×cb→ca \times_c b \to c, to serve as the actual object in the slice. It seems like there are two choices, depending on how you trace out the square. But the square commutes, which by definition means that we don’t really have a choice. We choose fπ1f\pi_1, i.e. following the top face then the right face, for definiteness.

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

Let us turn to the projection maps. Again by commutativity of the square, the pullback projection maps π1\pi_1 and π2\pi_2 extend directly to maps from fπ1f\pi_1 into ff and gg over cc. In the nontrivial case, we have to show that gπ2=fπ1g\pi_2 = f\pi_1, which is exactly what commutativity of the square gets us.

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

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

    open is-product

Now we turn to showing that these projections are universal, in the slice C/c\mathcal{C}/c. Given a family Q:Q→cQ : Q \to c, the data of maps p:p→fp : p \to f and q:p→gq : p \to g over cc is given precisely by evidence that fq=gpfq = gp, meaning that they fit neatly around our pullback diagram, as shown in the square below.

And, as indicated in the diagram, since this square is a pullback, we can obtain the dashed map l:Q→a×cbl : Q \to a \times_c b, which we can calculate satisfies

fπ1l=fp=Q, f\pi_1l = fp = Q\text{,}

so that it is indeed a map Q→f×gQ \to f \times g over cc, as required. Reading out the rest of (a×cb)(a \times_c b)’s universal property, we see that ll is the unique map which satisfies π1l=p\pi_1l = p and π2l=q\pi_2l = q, exactly as required for the pairing ⟨p,q⟩\langle p, q \rangle of a product in C/c.\mathcal{C}/c.

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

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

While products and terminal objects in C/X\mathcal{C}/X do not correspond to those in C\mathcal{C}, pullbacks (and equalisers) are precisely equivalent. A square is a pullback in C/X\mathcal{C}/X precisely if its image in C\mathcal{C}, forgetting the maps to XX, is a pullback.

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\mathcal{C}/X may be tested in C\mathcal{C}, but we do have to take some care when extending the “universal” morphism back down to the slice category (see the calculation marked {- * -}).

    : 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 pb = pb' where
    pb' : is-pullback (Slice _ _) _ _ _ _
    pb' .square           = ext (pb .square)
    pb' .universal p .map = pb .universal (ap map p)
    pb' .universal {P'} {p₁' = p₁'} p .commutes =
      (c .map ∘ pb .universal (ap map p))           ≡˘⟨ pulll (p1 .commutes) ⟩≡˘
      (P .map ∘ p1 .map ∘ pb .universal (ap map p)) ≡⟨ ap (_ ∘_) (pb .p₁∘universal) ⟩≡
      (P .map ∘ p₁' .map)                           ≡⟨ p₁' .commutes ⟩≡
      P' .map                                       ∎ {- * -}
    pb' .p₁∘universal = ext (pb .p₁∘universal)
    pb' .p₂∘universal = ext (pb .p₂∘universal)
    pb' .unique p q   = ext (pb .unique (ap map p) (ap map q))

    : 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 pb = pb' where
    pb' : is-pullback _ _ _ _ _
    pb' .square = ap map (pb .square)
    pb' .universal p = pb .universal
      {p₁' = record { commutes = refl }}
      {p₂' = record { commutes = sym (pulll (g .commutes))
                              ·· sym (ap (_ ∘_) p)
                              ·· pulll (f .commutes) }}
      (ext p) .map
    pb' .p₁∘universal = ap map $ pb .p₁∘universal
    pb' .p₂∘universal = ap map $ pb .p₂∘universal
    pb' .unique p q   = ap map $ pb .unique
      {lim' = record { commutes = sym (pulll (p1 .commutes)) ∙ ap (_ ∘_) p }}
      (ext p) (ext q)

It follows that any slice of a category with pullbacks is finitely complete. Note that we could have obtained the products abstractly, since any category with pullbacks and a terminal object has products, but expanding on the definition in components helps clarify both their construction and the role of pullbacks.

  Slice-pullbacks : ∀ {b} → has-pullbacks C → has-pullbacks (Slice C b)
  Slice-products  : ∀ {b} → has-pullbacks C → has-products (Slice C b)
  Slice-lex : ∀ {b} → has-pullbacks C → Finitely-complete (Slice C b)
This is one of the rare moments when the sea of theory has already risen to meet our prose — put another way, the proofs of the statements above are just putting things together. We leave them in this <details> block for the curious reader.
  Slice-pullbacks pullbacks {A = A} f g = pb where
    pb : Pullback (Slice C _) _ _
    pb .apex = cut (A .map ∘ pullbacks _ _ .p₁)
    pb .p₁ = record { commutes = refl }
    pb .p₂ = record { commutes =
         sym (pushl (sym (f .commutes))
      ·· ap₂ _∘_ refl (pullbacks _ _ .square)
      ·· pulll (g .commutes)) }
    pb .has-is-pb = pullback-above→pullback-below $
      pullbacks (f .map) (g .map) .has-is-pb

  Slice-products pullbacks f g = Pullback→Fibre-product (pullbacks _ _)

  Slice-lex pb = with-pullbacks (Slice C _)
    (Slice-pullbacks pb)

Slices of Sets🔗

Having tackled some properties of slice categories in general, we now turn to characterising the slice C/x\mathcal{C}/x as the category of families of C\mathcal{C}-objects indexed by xx, by formalising the aforementioned equivalence Sets/I≅[I,Sets]\mathbf{Sets}/I \cong [I, \mathbf{Sets}]. Let us trace our route before we depart, and write down an outline of the proof.

  • A functor F:I→SetsF : I \to \mathbf{Sets} is sent to the first projection π1:(ΣF)→I\pi_1 : (\Sigma F) \to I, functorially. Since ΣF\Sigma F is the total space of FF, we refer to this as the Total-space functor.

  • We define a procedure that, given a morphism ΣF→ΣG\Sigma F \to \Sigma G over II, recovers a natural transformation F⇒GF \Rightarrow G; We then calculate that this procedure is an inverse to the action on morphisms of Total-space, so that it is fully faithful.

  • Finally, we show that, given p:X→Ip : X \to I, the assignment i↦p−1(i)i \mapsto p^{-1}(i), sending an index to the fibre of pp over it, gives a functor PP; and that ∫P≅p\int P \cong p over II, so that Total-space is a split essential surjection, hence an equivalence of categories.

Let’s begin. The Total-space functor gets out of our way very fast:

  Total-space : Functor Cat[ Disc' I , Sets ℓ ] (Slice (Sets ℓ) I)
  Total-space .F₀ F .domain = el (Σ _ (∣_∣ ⊙ F₀ F)) hlevel!
  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    = trivial!
  Total-space .F-∘ _ _ = trivial!

Since the construction of the functor itself is straightforward, we turn to showing it is fully faithful. The content of a morphism h:ΣF→ΣGh : \Sigma F \to \Sigma G over II is a function

h:(ΣF)→(ΣG) h : (\Sigma F) \to (\Sigma G)

which preserves the first projection, i.e. we have π1(h(i,x))=i\pi_1(h(i, x)) = i. This means that it corresponds to a dependent function h:F(i)→G(i)h : F(i) \to G(i), and, since the morphisms in II-qua-category are trivial, this dependent function is automatically a natural transformation.

  Total-space-is-ff : is-fully-faithful Total-space
  Total-space-is-ff {F} {G} = is-iso→is-equiv $
    iso from linv (λ x → Nat-path λ x → funext (λ _ → transport-refl _)) where

    from : /-Hom (Total-space .F₀ F) (Total-space .F₀ G) → F => G
    from mp = nt where
      eta : ∀ i → ⌞ F .F₀ i ⌟ → ⌞ G .F₀ i ⌟
      eta i j =
        subst (∣_∣ ⊙ G .F₀) (happly (mp .commutes) _) (mp .map (i , j) .snd)

      nt : F => G
      nt .η = eta
      nt .is-natural _ _ = J (λ _ p → eta _ ⊙ F .F₁ p ≡ G .F₁ p ⊙ eta _) $
        eta _ ⊙ F .F₁ refl ≡⟨ ap (eta _ ⊙_) (F .F-id) ⟩≡
        eta _              ≡˘⟨ ap (_⊙ eta _) (G .F-id) ⟩≡˘
        G .F₁ refl ⊙ eta _ ∎

All that remains is showing that sending a map pp to the total space of its family of fibres gets us all the way back around to pp. Fortunately, our proof that universes are object classifiers grappled with many of the same concerns, so we have a reusable equivalence Total-equiv which slots right in. By univalence, we can finish in style: not only is Σ(x↦p−1(x))\Sigma (x \mapsto p^{-1}(x)) isomorphic to pp in Sets/I\mathbf{Sets}/I, it’s actually identical to pp!

  Total-space-is-eso : is-split-eso Total-space
  Total-space-is-eso fam = functor , path→iso path where
    functor : Functor _ _
    functor .F₀ i    = el! (fibre (fam .map) i)
    functor .F₁ p    = subst (fibre (fam .map)) p
    functor .F-id    = funext transport-refl
    functor .F-∘ f g = funext (subst-∙ (fibre (fam .map)) _ _)

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

Slices preserve univalence🔗

In passing, we can put together the following result: any slice of a univalent category is univalent again. That’s because an identification p:(X,f)≡(Y,g):C/xp : (X, f) \equiv (Y, g) : \mathcal{C}/x is given by an identification p′:X≡Yp' : X \equiv Y and a proof that f=gf = g over pp. We already have a characterisation of dependent identifications in a space of morphisms, in terms of composition with the induced isomorphisms, so that this latter condition reduces to showing p∘f=gp \circ f = g.

Therefore, if we have an isomorphism i:f≅gi : f \cong g over xx, and its component in C\mathcal{C} corresponds to an identification X≡YX \equiv Y, then the commutativity of ii is exactly the data we need to extend this to an identification (X,f)≡(Y,g)(X, f) \equiv (Y, g).

  slice-is-category : is-category (Slice C o)
  slice-is-category .to-path x = /-Obj-path (isc .to-path $
    C.make-iso (x .to .map) (x .from .map)
      (ap map (C/o._≅_.invl x)) (ap map (C/o._≅_.invr x)))
    (Univalent.Hom-pathp-refll-iso isc (x .from .commutes))
  slice-is-category .to-path-over x = C/o.≅-pathp refl _ $
    /-Hom-pathp _ _ (Univalent.Hom-pathp-reflr-iso isc (C.idr _))

Constant families🔗

If C/B\mathcal{C}/B is the category of families of C\mathcal{C}-objects indexed by BB, it stands to reason that we should be able to consider any object A:CA : \mathcal{C} as a family over BB, where each fibre of the family is isomorphic to AA. Type-theoretically, this would correspond to taking a closed type and trivially regarding it as living in a context Γ\Gamma by ignoring the context entirely.

From the perspective of slice categories, the constant families functor, Δ:C→C/B\Delta : \mathcal{C} \to \mathcal{C}/B, sends an object A:CA : \mathcal{C} to the projection morphism π2:A×B→B\pi_2 : A \times B \to B.

module _ {o ℓ} {C : Precategory o ℓ} {B} (prod : has-products C) where
  open Binary-products C prod
  open Cat.Reasoning C

  constant-family : Functor C (Slice C B)
  constant-family .F₀ A = cut (π₂ {a = A})
  constant-family .F₁ f .map      = ⟨ f ∘ π₁ , π₂ ⟩
  constant-family .F₁ f .commutes = π₂∘⟨⟩
  constant-family .F-id    = ext (sym (⟨⟩-unique _ id-comm (idr _)))
  constant-family .F-∘ f g = ext $ sym $
      ⟨⟩-unique _ (pulll π₁∘⟨⟩ ∙ extendr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ π₂∘⟨⟩)

We can observe that this really is a constant families functor by performing the following little calculation: If we have a map h:Y→Bh : Y \to B, then the fibre of ΔB(A)\Delta_B(A) over hh, given by the pullback

is isomorphic to A×YA \times Y. The extra generality makes it a bit harder to see the constancy, but if hh were a point h:⊤→Bh : \top \to B, the fibre over hh would correspondingly be isomorphic to A×⊤≅AA \times \top \cong A.

    : (pb : has-pullbacks C)
    → ∀ {A Y} (h : Hom Y B)
    → pb (constant-family .F₀ A .map) h .Pullback.apex ≅ (A ⊗₀ Y)
  constant-family-fibre pb {A} h = make-iso
    ⟨ π₁ ∘ p₁ , p₂ ⟩ (universal {p₁' = ⟨ π₁ , h ∘ π₂ ⟩} {p₂' = π₂} π₂∘⟨⟩)
    (⟨⟩∘ _ ∙ sym (Product.unique (prod _ _) _
      (idr _ ∙ sym (pullr p₁∘universal ∙ π₁∘⟨⟩))
      (idr _ ∙ sym p₂∘universal)))
    (Pullback.unique₂ (pb _ _) {p = π₂∘⟨⟩ ∙ square}
      (pulll p₁∘universal ∙ ⟨⟩∘ _ ∙ ap₂ ⟨_,_⟩ π₁∘⟨⟩ (pullr π₂∘⟨⟩ ∙ sym square))
      (pulll p₂∘universal ∙ π₂∘⟨⟩)
      (idr _ ∙ Product.unique (prod _ _) _ refl refl)
      (idr _))
    where open Pullback (pb (constant-family .F₀ A .map) h)