module Cat.Instances.Slice where

Slice categoriesπŸ”—

When working in there is an evident notion of family indexed by a set: a family of sets is equivalently a functor where we have equipped the set 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 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 then, would consist of an object and a morphism where is considered as the β€œtotal space” object and assigns gives the β€œtag” of each object. By analysing how pulls back along maps we recover a notion of β€œfibres”: the collection with index can be recovered as the pullback

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 and object we have a category of objects indexed by , the slice category An object of β€œthe slice over ” is given by an object to serve as the domain, and a map

  record /-Obj (c : C.Ob) : Type (o βŠ” β„“) where
    constructor cut
    field
      {domain} : C.Ob
      map      : C.Hom domain c

A map between and is given by a map such that the triangle below commutes. Since we’re thinking of and as families indexed by , commutativity of the triangle says that the map β€œrespects reindexing”, or less obliquely β€œpreserves fibres”.

  record /-Hom (a b : /-Obj c) : Type β„“ where
    no-eta-equality
    private
      module a = /-Obj a
      module b = /-Obj b
    field
      map      : C.Hom a.domain b.domain
      commutes : b.map C.∘ map ≑ a.map

The slice category is given by the /-Obj and /-Homs.

Slice : (C : Precategory o β„“) β†’ ⌞ 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 = hlevel 2
  precat .id .map      = C.id
  precat .id .commutes = C.idr _

For composition in the slice over note that if the triangle (the commutativity condition for and the rhombus (the commutativity condition for both commute, then so does the larger triangle (the commutativity for

  precat ._∘_ {x} {y} {z} f g = fog where
    module f = /-Hom f
    module g = /-Hom g
    fog : /-Hom _ _
    fog .map = f.map C.∘ g.map
    fog .commutes =
      z .map C.∘ f.map C.∘ g.map β‰‘βŸ¨ C.pulll f.commutes βŸ©β‰‘
      y .map C.∘ g.map           β‰‘βŸ¨ g.commutes βŸ©β‰‘
      x .map                     ∎
  precat .idr f = ext (C.idr _)
  precat .idl f = ext (C.idl _)
  precat .assoc f g h = ext (C.assoc _ _ _)

There is an evident projection functor from to that only remembers the domains.

  Forget/ : Functor (Slice C c) C
  Forget/ .Fβ‚€ o = o .domain
  Forget/ .F₁ f = f .map
  Forget/ .F-id = refl
  Forget/ .F-∘ _ _ = refl

Furthermore, this forgetful functor is easily seen to be faithful and conservative: if is a morphism in whose underlying map has an inverse in then clearly also makes the triangle commute, so that is invertible in

  Forget/-is-faithful : is-faithful Forget/
  Forget/-is-faithful p = ext p

  Forget/-is-conservative : is-conservative Forget/
  Forget/-is-conservative {f = f} i =
    C/c.make-invertible f⁻¹ (ext i.invl) (ext i.invr)
    where
      module i = C.is-invertible i
      f⁻¹ : /-Hom _ _
      f⁻¹ .map = i.inv
      f⁻¹ .commutes = C.rswizzle (sym (f .commutes)) i.invl

Finite limitsπŸ”—

We discuss the construction of finite limits in the slice of First, every slice category has a terminal object, given by the identity map

module _ {o β„“} {C : Precategory o β„“} {c : ⌞ 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 C.id)
  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 .Terminal.top  = _
  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 and is exactly the product in the slice over

Suppose we have a pullback diagram like the one below, i.e., a limit of the diagram in the category We’ll show that it’s also a limit of the (discrete) diagram consisting of and but now in the slice category

For starters, we have to define a map 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 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 and extend directly to maps from into and over In the nontrivial case, we have to show that 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 Given a family the data of maps and over is given precisely by evidence that 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 which we can calculate satisfies

so that it is indeed a map over as required. Reading out the rest of universal property, we see that is the unique map which satisfies and exactly as required for the pairing of a product in

    is-pullback→is-fibre-product
      : 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.map                   β‰‘βŸ¨ p.commutes βŸ©β‰‘
        Q .map                             ∎

While products and terminal objects in do not correspond to those in pullbacks (and equalisers) are precisely equivalent. A square is a pullback in precisely if its image in forgetting the maps to 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 may be tested in but we do have to take some care when extending the β€œuniversal” morphism back down to the slice category (see the calculation marked {- * -}).

  pullback-above→pullback-below
    : 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))

  pullback-below→pullback-above
    : 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-terminal-object
    (Slice-pullbacks pb)

Slices of SetsπŸ”—

Having tackled some properties of slice categories in general, we now turn to characterising the slice as the category of families of indexed by , by formalising the aforementioned equivalence Let us trace our route before we depart, and write down an outline of the proof.

  • A functor is sent to the first projection functorially. Since is the total space of we refer to this as the Total-space functor.

  • We define a procedure that, given a morphism over recovers a natural transformation 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 the assignment sending an index to the fibre of over it, gives a functor and that over 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))
  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 over is a function

which preserves the first projection, i.e.Β we have This means that it corresponds to a dependent function and, since the morphisms in 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 β†’ ext Ξ» _ _ β†’ transport-refl _) where

    from : /-Hom (Total-space .Fβ‚€ F) (Total-space .Fβ‚€ G) β†’ F => G
    from mp = nt where
      eta : βˆ€ i β†’ F Κ» i β†’ G Κ» i
      eta i j = subst (G Κ»_) (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 to the total space of its family of fibres gets us all the way back around to 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 isomorphic to in it’s actually identical to

  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 is given by an identification and a proof that over 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

Therefore, if we have an isomorphism over and its component in corresponds to an identification then the commutativity of is exactly the data we need to extend this to an identification

  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 is the category of families of indexed by , it stands to reason that we should be able to consider any object as a family over where each fibre of the family is isomorphic to Type-theoretically, this would correspond to taking a closed type and trivially regarding it as living in a context by ignoring the context entirely.

From the perspective of slice categories, the constant families functor, sends an object to the projection morphism

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 then the fibre of over given by the pullback

is isomorphic to The extra generality makes it a bit harder to see the constancy, but if were a point the fibre over would correspondingly be isomorphic to

  constant-family-fibre
    : (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)

The constant families functor is a right adjoint to the projection This can be understood in terms of base change: if has a terminal object then the slice is equivalent to and the unique map induces a pullback functor that is just the constant families functor. On the other hand, the β€œdependent sum” functor sends a map to the unique composite it simply Forget/s the map. Thus the following adjunction is a special case of the adjunction between dependent sum and base change.

  Forget⊣constant-family : Forget/ ⊣ constant-family
  Forget⊣constant-family .unit .η X .map = ⟨ id , X .map ⟩
  Forget⊣constant-family .unit .Ξ· X .commutes = Ο€β‚‚βˆ˜βŸ¨βŸ©
  Forget⊣constant-family .unit .is-natural _ _ f = ext (uniqueβ‚‚
    (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ id-comm-sym)
    (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ f .commutes)
    (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚βˆ˜βŸ¨βŸ©)
    (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©))
  Forget⊣constant-family .counit .Ξ· x = π₁
  Forget⊣constant-family .counit .is-natural _ _ f = Ο€β‚βˆ˜βŸ¨βŸ©
  Forget⊣constant-family .zig = Ο€β‚βˆ˜βŸ¨βŸ©
  Forget⊣constant-family .zag = ext (uniqueβ‚‚
    (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚βˆ˜βŸ¨βŸ©)
    (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©)
    refl
    (idr _))