module Cat.Displayed.Instances.Slice {o ℓ} (B : Precategory o ℓ) where

The canonical self-indexing🔗

There is a canonical way of viewing any category B\mathcal{B} as displayed over itself, given fibrewise by taking slice categories. Following (Sterling and Angiuli 2022), we refer to this construction as the canonical-self indexing of B\mathcal{B} and denote it B‾\underline{\mathcal{B}}. Recall that the objects in the slice over yy are pairs consisting of an object xx and a map f:x→yf : x \to y. The core idea is that any morphism lets us view an object xx as being “structure over” an object yy; the collection of all possible such structures, then, is the set of morphisms x→yx \to y, with domain allowed to vary.

Contrary to the maps in the slice category, the maps in the canonical self-indexing have an extra “adjustment” by a morphism f:x→yf : x \to y of the base category. Where maps in the ordinary slice are given by commuting triangles, maps in the canonical self-indexing are given by commuting squares, of the form

where the primed objects and dotted arrows are displayed.

    {x y} (f : Hom x y)
    (px : /-Obj {C = B} x) (py : /-Obj {C = B} y)
    : Type ℓ
  constructor slice-hom
    to      : Hom (px .domain) (py .domain)
    commute : f ∘ px .map ≡ py .map ∘ to

open Slice-hom

The intuitive idea for the canonical self-indexing is possibly best obtained by considering the canonical self-indexing of Setsκ\mathbf{Sets}_\kappa. First, recall that an object f:Sets/Xf : \mathbf{Sets}/X is equivalently a XX-indexed family of sets, with the value of the family at each point x:Xx : X being the fibre f∗(x)f^*(x). A function X→YX \to Y of sets then corresponds to a reindexing, which takes an XX-family of sets to a YY-family of sets (in a functorial way). A morphism X′→Y′X' \to Y' in the canonical self-indexing of Sets\mathbf{Sets} lying over a map f:X→Yf : X \to Y is then a function between the families X′→Y′X' \to Y' which commutes with the reindexing given by ff.

It’s straightforward to piece together the objects of the (ordinary) slice category and our displayed maps Slice-hom into a category displayed over B\mathcal{B}.

Slices : Displayed B (o ⊔ ℓ) ℓ
Slices .Ob[_] = /-Obj {C = B}
Slices .Hom[_] = Slice-hom
Slices .Hom[_]-set = Slice-is-set
Slices .id′ = slice-hom id id-comm-sym
Slices ._∘′_ {x = x} {y = y} {z = z} {f = f} {g = g} px py =
  slice-hom (px .to ∘ py .to) $
    (f ∘ g) ∘ x .map           ≡⟨ pullr (py .commute) ⟩≡
    f ∘ (y .map ∘ py .to)      ≡⟨ extendl (px .commute) ⟩≡
    z .map ∘ (px .to ∘ py .to) ∎
Slices .idr′ {f = f} f′ = Slice-pathp (idr f) (idr (f′ .to))
Slices .idl′ {f = f} f′ = Slice-pathp (idl f) (idl (f′ .to))
Slices .assoc′ {f = f} {g = g} {h = h} f′ g′ h′ =
  Slice-pathp (assoc f g h) (assoc (f′ .to) (g′ .to) (h′ .to))

It’s only slightly more annoying to show that a vertical map in the canonical self-indexing is a map in the ordinary slice category which, since the objects displayed over xx are defined to be those of the slice category B/x\mathcal{B}/x, gives an equivalence of categories between the fibre B‾∗(x)\underline{\mathcal{B}}^*(x) and the slice B/x\mathcal{B}/x.

Fibre→slice : ∀ {x} → Functor (Fibre Slices x) (Slice B x)
Fibre→slice .F₀ x = x
Fibre→slice .F₁ f ./ = f .to
Fibre→slice .F₁ f ./-Hom.commutes = sym (f .commute) ∙ eliml refl
Fibre→slice .F-id = /-Hom-path refl
Fibre→slice .F-∘ f g = /-Hom-path (transport-refl _)

Fibre→slice-is-ff : ∀ {x} → is-fully-faithful (Fibre→slice {x = x})
Fibre→slice-is-ff {_} {x} {y} = is-iso→is-equiv isom where
  isom : is-iso (Fibre→slice .F₁)
  isom .is-iso.inv hom =
    slice-hom (hom ./ (eliml refl ∙ sym (hom ./-Hom.commutes))
  isom .is-iso.rinv x = /-Hom-path refl
  isom .is-iso.linv x = Slice-pathp refl refl

Fibre→slice-is-equiv : ∀ {x} → is-equivalence (Fibre→slice {x})
Fibre→slice-is-equiv = is-precat-iso→is-equivalence $
  record { has-is-ff = Fibre→slice-is-ff
         ; has-is-iso = id-equiv

Cartesian Maps🔗

A map f′:x′→y′f' : x' \to y' over f:x→yf : x \to y in the codomain fibration is cartesian if and only if it forms a pullback square as below:

This follows by a series of relatively straightforward computations, so we do not comment too heavily on the proof.

  : ∀ {x y x′ y′} {f : Hom x y} {f′ : Slice-hom f x′ y′}
  → is-cartesian Slices f f′
  → is-pullback B (x′ .map) f (f′ .to) (y′ .map)
cartesian→pullback {x} {y} {x′} {y′} {f} {f′} cart = pb where
  pb : is-pullback B (x′ .map) f (f′ .to) (y′ .map)
  pb .is-pullback.square = f′ .commute
  pb .is-pullback.universal p =
    cart .universal _ (slice-hom _ (idr _ ∙ p)) .to
  pb .is-pullback.p₁∘universal =
    sym (cart .universal _ _ .commute) ∙ idr _
  pb .is-pullback.p₂∘universal =
    ap (cart .commutes _ _)
  pb .is-pullback.unique p q =
    ap (cart .unique (slice-hom _ (idr _ ∙ sym p)) (Slice-pathp refl q))

  : ∀ {x y x′ y′} {f : Hom x y} {f′ : Slice-hom f x′ y′}
  → is-pullback B (x′ .map) f (f′ .to) (y′ .map)
  → is-cartesian Slices f f′
pullback→cartesian {x} {y} {x′} {y′} {f} {f′} pb = cart where
  module pb = is-pullback pb

  cart : is-cartesian Slices f f′
  cart .universal m h′ .to = pb.universal (assoc _ _ _ ∙ h′ .commute)
  cart .universal m h′ .commute = sym pb.p₁∘universal
  cart .commutes m h′ = Slice-pathp refl pb.p₂∘universal
  cart .unique m′ x = Slice-pathp refl $
    pb.unique (sym (m′ .commute)) (ap to x)

As a fibration🔗

If (and only if) B\mathcal{B} has all pullbacks, then its self-indexing is a Cartesian fibration. This is almost by definition, and is in fact where the “Cartesian” in “Cartesian fibration” (recall that another term for “pullback square” is “cartesian square”). Since the total space ∫B‾\int \underline{\mathcal{B}} is equivalently the arrow category of B\mathcal{B}, with the projection functor π:∫B‾→B\pi : \int \underline{\mathcal{B}} \to \mathcal{B} corresponding under this equivalence to the codomain functor, we refer to caB‾\underline{ca{B}} regarded as a Cartesian fibration as the codomain fibration.

  : (∀ {x y z} (f : Hom x y) (g : Hom z y) → Pullback B f g)
  → Cartesian-fibration Slices
Codomain-fibration pullbacks .has-lift f y′ = lift-f where
  module pb = Pullback (pullbacks f (y′ .map))

  lift-f : Cartesian-lift Slices f y′
  lift-f .x′ = cut pb.p₁
  lift-f .lifting .to = pb.p₂
  lift-f .lifting .commute = pb.square
  lift-f .cartesian = pullback→cartesian pb.has-is-pb

Since the proof that Slices is a cartesian fibration is given by essentially rearranging the data of pullbacks in B\mathcal{B}, we also have the converse implication: If B‾\underline{\mathcal{B}} is a Cartesian fibration, then B\mathcal{B} has all pullbacks.

  : ∀ {x y z} (f : Hom x y) (g : Hom z y)
  → Cartesian-fibration Slices
  → Pullback B f g
Codomain-fibration→pullbacks f g lifts = pb where
  open Pullback
  open is-pullback
  module the-lift = Cartesian-lift (lifts .has-lift f (cut g))

  pb : Pullback B f g
  pb .apex = the-lift.x′ .domain
  pb .p₁ = the-lift.x′ .map
  pb .p₂ = the-lift.lifting .to
  pb .has-is-pb .square = the-lift.lifting .commute
  pb .has-is-pb .universal {p₁' = p₁'} {p₂'} p =
    the-lift.cartesian .universal {u′ = cut id}
      p₁' (slice-hom p₂' (pullr (idr _) ∙ p)) .to
  pb .has-is-pb .p₁∘universal =
    sym (the-lift.universal _ _ .commute) ∙ idr _
  pb .has-is-pb .p₂∘universal = ap to (the-lift.cartesian .commutes _ _)
  pb .has-is-pb .unique p q = ap to $ the-lift.cartesian .unique
    (slice-hom _ (idr _ ∙ sym p)) (Slice-pathp refl q)

Since the fibres of the codomain fibration are given by slice categories, then the interpretation of Cartesian fibrations as “displayed categories whose fibres vary functorially” leads us to reinterpret the above results as, essentially, giving the pullback functors between slice categories.

As an Opfibration🔗

The canonical self-indexing is always an opfibration, where opreindexing is given by postcomposition. If we think about slices as families, then opreindexing along X→YX \to Y extends a family over XX to a family over YY by adding in empty fibres for all elements of YY that do not lie in the image of ff.

Codomain-opfibration : Cocartesian-fibration Slices
Codomain-opfibration .Cocartesian-fibration.has-lift f x′ = lift-f where

  lift-f : Cocartesian-lift Slices f x′
  lift-f .Cocartesian-lift.y′ = cut (f ∘ x′ .map)
  lift-f .Cocartesian-lift.lifting = slice-hom id (sym (idr _))
  lift-f .Cocartesian-lift.cocartesian .is-cocartesian.universal m h′ =
    slice-hom (h′ .to) (assoc _ _ _ ∙ h′ .commute)
  lift-f .Cocartesian-lift.cocartesian .is-cocartesian.commutes m h′ =
    Slice-pathp refl (idr _)
  lift-f .Cocartesian-lift.cocartesian .is-cocartesian.unique m′ p =
    Slice-pathp refl (sym (idr _) ∙ ap to p)