open import Cat.Diagram.Limit.Finite
open import Cat.Functor.Properties
open import Cat.Instances.Discrete
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Functor.Base
open import Cat.Prelude

open import Data.Sum

import Cat.Reasoning

module Cat.Instances.Slice where

private variable
  o ℓ o' ℓ' : Level
open Functor
open _=>_

module _ {o ℓ} {C : Precategory o ℓ} where
  private
    module C = Cat.Reasoning C
    variable a b c : C.Ob

Slice categories🔗

When working in $\mathbf{Sets}$, there is an evident notion of family indexed by a set: a family of sets $(F_i)_{i \in I}$ is equivalently a functor $[\mathrm{Disc}(I), \mathbf{Sets}]$, where we have equipped the set $I$ 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 $\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 $I$, then, would consist of an object $A$ and a morphism $t : A \to I$, where $A$ is considered as the “total space” object and $t$ assigns gives the “tag” of each object. By analysing how $t$ pulls back along maps $B \to I$, we recover a notion of “fibres”: the collection with index $i$ can be recovered as the pullback $t^*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 $\mathcal{C}$ and object $c : \mathcal{C}$, we have a category of objects indexed by $c$, the slice category $\mathcal{C}/c$. An object of “the slice over $c$” is given by an object $d : \mathcal{C}$ to serve as the domain, and a map $f : d \to c$.

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

A map between $f : a \to c$ and $g : b \to c$ is given by a map $h : a \to b$ such that the triangle below commutes. Since we’re thinking of $f$ and $g$ as families indexed by $c$, commutativity of the triangle says that the map $h$ “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

  /-Obj-path : ∀ {c} {x y : /-Obj c}
             → (p : x ./-Obj.domain ≡ y ./-Obj.domain)
             → PathP (λ i → C.Hom (p i) c) (x ./-Obj.map) (y ./-Obj.map)
             → x ≡ y
  /-Obj-path p q i ./-Obj.domain = p i
  /-Obj-path p q i ./-Obj.map = 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 ./-Hom.map) (y ./-Hom.map)
              → 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 =
      is-prop→pathp
        (λ i → C.Hom-set (p i ./-Obj.domain) _
                         (q i ./-Obj.map C.∘ r i) (p i ./-Obj.map))
        (x .commutes) (y .commutes) i

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

  Extensional-/-Hom
    : ∀ {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

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

  abstract
    /-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  eqv (hlevel )

The slice category $\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      = C.id
  precat .id .commutes = C.idr _

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

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

Finite limits🔗

We discuss the construction of finite limits in the slice of $\mathcal{C}/c$. First, every slice category has a terminal object, given by the identity map $\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 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'

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
  private variable
    a b : C.Ob
    f g π₁ π₂ : C.Hom a b
  open /-Hom
  open /-Obj

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

For starters, we have to define a map $a \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\pi_1$, i.e. following the top face then the right face, for definiteness.

  module
    _ {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))
    where
    private module pb = is-pullback pb

    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 $\pi_1$ and $\pi_2$ extend directly to maps from $f\pi_1$ into $f$ and $g$ over $c$. In the nontrivial case, we have to show that $g\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 $\mathcal{C}/c$. Given a family $Q : Q \to c$, the data of maps $p : p \to f$ and $q : p \to g$ over $c$ is given precisely by evidence that $fq = 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 \to a \times_c b$, which we can calculate satisfies

$$f\pi_1l = fp = Q\text{,}$$

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

    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                             ∎

    is-pullback→is-fibre-product .π₁∘factor = ext pb.p₁∘universal
    is-pullback→is-fibre-product .π₂∘factor = ext pb.p₂∘universal
    is-pullback→is-fibre-product .unique other p q =
      ext (pb.unique (ap map p) (ap map q))

  Pullback→Fibre-product
    : ∀ {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 $\mathcal{C}/X$ do not correspond to those in $\mathcal{C}$, pullbacks (and equalisers) are precisely equivalent. A square is a pullback in $\mathcal{C}/X$ precisely if its image in $\mathcal{C}$, forgetting the maps to $X$, 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 $\mathcal{C}/X$ may be tested in $\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 {- * -}).

module _ {o ℓ} {C : Precategory o ℓ} {X : Precategory.Ob C}
         {P A B c} {p1 f p2 g}
  where
  open Cat.Reasoning C
  open is-pullback
  open /-Obj
  open /-Hom

  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.

module _ {o ℓ} {C : Precategory o ℓ} where
  open Cat.Reasoning C
  open Pullback
  open /-Obj
  open /-Hom

  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)

  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🔗

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

Having tackled some properties of slice categories in general, we now turn to characterising the slice $\mathcal{C}/x$ as the category of families of $\mathcal{C}$-objects indexed by $x$, by formalising the aforementioned equivalence $\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 \to \mathbf{Sets}$ is sent to the first projection $\pi_1 : (\Sigma F) \to I$, functorially. Since $\Sigma F$ is the total space of $F$, we refer to this as the Total-space functor.

• We define a procedure that, given a morphism $\Sigma F \to \Sigma G$ over $I$, recovers a natural transformation $F \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 \to I$, the assignment $i \mapsto p^{-1}(i)$, sending an index to the fibre of $p$ over it, gives a functor $P$; and that $\int P \cong p$ over $I$, 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 : \Sigma F \to \Sigma G$ over $I$ is a function

$$h : (\Sigma F) \to (\Sigma G)$$

which preserves the first projection, i.e. we have $\pi_1(h(i, x)) = i$. This means that it corresponds to a dependent function $h : F(i) \to G(i)$, and, since the morphisms in $I$-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 _ ∎

    linv : is-left-inverse (F₁ Total-space) from
    linv x = ext λ y → Σ-path (sym (happly (x .commutes) _))
      ( sym (transport-∙ (ap (∣_∣ ⊙ G .F₀) (happly (x .commutes) y))
                    (sym (ap (∣_∣ ⊙ G .F₀) (happly (x .commutes) y))) _)
      ·· ap₂ transport (∙-invr (ap (∣_∣ ⊙ G .F₀) (happly (x .commutes) y))) refl
      ·· transport-refl _)

All that remains is showing that sending a map $p$ to the total space of its family of fibres gets us all the way back around to $p$. 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 $\Sigma (x \mapsto p^{-1}(x))$ isomorphic to $p$ in $\mathbf{Sets}/I$, it’s actually identical to $p$!

  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) \equiv (Y, g) : \mathcal{C}/x$ is given by an identification $p' : X \equiv Y$ and a proof that $f = g$ over $p$. 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 \circ f = g$.

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

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

Therefore, if we have an isomorphism $i : f \cong g$ over $x$, and its component in $\mathcal{C}$ corresponds to an identification $X \equiv Y$, then the commutativity of $i$ is exactly the data we need to extend this to an identification $(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 _))

open /-Obj
open /-Hom

Constant families🔗

If $\mathcal{C}/B$ is the category of families of $\mathcal{C}$-objects indexed by $B$, it stands to reason that we should be able to consider any object $A : \mathcal{C}$ as a family over $B$, where each fibre of the family is isomorphic to $A$. 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, $\Delta : \mathcal{C} \to \mathcal{C}/B$, sends an object $A : \mathcal{C}$ to the projection morphism $\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 \to B$, then the fibre of $\Delta_B(A)$ over $h$, given by the pullback

is isomorphic to $A \times Y$. The extra generality makes it a bit harder to see the constancy, but if $h$ were a point $h : \top \to B$, the fibre over $h$ would correspondingly be isomorphic to $A \times \top \cong A$.

  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)