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


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


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 \to Z$ and $g : Y \to Z$ is exactly the product $f \times g$ in the slice over $Z$.

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)  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π

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$


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}