module Cat.Displayed.Instances.DisplayedFamilies
  {o β„“ o' β„“'} {B : Precategory o β„“} (E : Displayed B o' β„“')
  where

The displayed family fibrationπŸ”—

The family fibration is a critical part of the theory of fibrations, as it acts as a stepping off point for generalizing structure found in 1-categories to structures in fibrations. However, it is deeply entangled in the meta-theory, as it uses the fact that the type of objects of a precategory is, well, a type.

If we wish to generalize some 1-categorical phenomena, we will need a version of the family fibration that represents families internal to a fibration, where objects should be B\mathcal{B}-indexed families of E\mathcal{E} objects. To construct such a fibration, we recall that every family P:Xβ†’TypeP : X \to \mathrm{Type} is equivalent to the total space of its fibres (see here for more details). It’s quite rare for B\mathcal{B} to have something that looks like a universe, but it does have enough structure to talk about fibres! We can consider a morphism B(a,x)\mathcal{B}(a, x) to be a sort of β€œgeneralized family” over xx, where aa is playing the role of the total space. Objects aβ€²:Eaa' : \mathcal{E}_{a} over aa then encode an xx-indexed family of E\mathcal{E} objects.

This is all quite abstract, so let’s look at an example. Consider some category E\mathcal{E} fibred over Sets\mathbf{Sets}. There is already a natural notion of an II-indexed family of E\mathcal{E}-objects here; namely, a map P:Iβ†’SetP : I \to \mathrm{Set} and a map X:(i:I)β†’EP(i)X : (i : I) \to \mathcal{E}_{P(i)}. To see that we obtain the definition from before, note that we can turn this family of sets into a map fst:Ξ£(i:I)P(i)β†’I\mathrm{fst} : \Sigma (i : I) P(i) \to I by taking the total space of PP. Furthermore, Ξ£(i:I)P(i)\Sigma (i : I) P(i) is a set, so we can consider the space of objects EΞ£(i:I)P(i)\mathcal{E}_{\Sigma (i : I) P(i)}. We can embed each X(i):EP(i)X(i) : E_{P(i)} into EΞ£(i:I)P(i)\mathcal{E}_{\Sigma (i : I) P(i)} by reindexing along the second projection Ξ£(i:I)P(i)β†’P(i)\Sigma (i : I) P(i) \to P(i)

To show the reverse direction, suppose we have some function f:Aβ†’If : A \to I, along with an object EA\mathcal{E}_{A}. We can obtain a family of sets fβˆ’1:Iβ†’Setf^{-1} : I \to \mathrm{Set} by taking the fibres of ff. Furthermore, note that for each i:Ii : I, we have a map fβˆ’1(i)β†’Af^{-1}(i) \to A from the fibre of ff at AA to AA; reindexing along this map yields an object Efβˆ’1(i)\mathcal{E}_{f^{-1}(i)} as desired.

Now that we are armed with the intuition, on with the construction! Recall that the object objects over x:Bx : \mathcal{B} shall be triples (a:B)Γ—B(a,x)Γ—Ea(a : \mathcal{B}) \times \mathcal{B}(a, x) \times \mathcal{E}_{a}, and morphisms f:(a,f,aβ€²)β†’(b,g,bβ€²)f : (a, f, a') \to (b, g, b') over u:xβ†’yu : x \to y are given by triples (k:B(a,b))Γ—(u∘f=g∘k)Γ—Ek(aβ€²,bβ€²)(k : \mathcal{B}(a, b)) \times (u \circ f = g \circ k) \times \mathcal{E}_{k}(a', b'). The first portion of this data can be obtained by using the codomain fibration over B\mathcal{B}. The remaining data involving E\mathcal{E} is then added by composing the codomain fibration with the base change of E\mathcal{E} along the functor Dom:∫Bβ†’β†’B\mathrm{Dom} : \int B^{\to} \to B that takes the domain of a morphism in the arrow category (which is the total category of the codomain fibration).

Dom : Functor (∫ (Slices B)) B
Dom .Fβ‚€ f = f .snd .domain
Dom .F₁ sq = sq .preserves .to
Dom .F-id = refl
Dom .F-∘ _ _ = refl

Disp-family : Displayed B (o βŠ” β„“ βŠ” o') (β„“ βŠ” β„“')
Disp-family = Slices B D∘ Change-of-base Dom E

private
  module Disp-family = Displayed Disp-family

Now, that was quite a bit of abstract nonsense, so let’s verify that the nonsense actually makes sense by characterizing the objects and morphisms of our category. As expected, objects consist of the triples described above.

fam-over : βˆ€ {x} β†’ (a : Ob) β†’ Hom a x β†’ Ob[ a ] β†’ Disp-family.Ob[ x ]
fam-over a f a' .fst .domain = a
fam-over a f a' .fst .map = f
fam-over a f a' .snd = a'

module Fam-over {x} (P : Disp-family.Ob[ x ]) where

  tot : Ob
  tot = P .fst .domain

  fam : Hom tot x
  fam = P .fst .map

  tot' : Ob[ tot ]
  tot' = P .snd

open Fam-over

We glossed over the morphisms above, so let’s go more into detail here. A morphism between displayed families P,QP, Q is given by a map between B\mathcal{B}-valued total spaces; this map must commute with the family structure on PP and QQ. Finally, we have a map between the E\mathcal{E}-valued total spaces.

module Fam-over-hom
  {x y} {u : Hom x y} {P : Disp-family.Ob[ x ]} {Q : Disp-family.Ob[ y ]}
  (fα΅’ : Disp-family.Hom[ u ] P Q)
  where

  map-tot : Hom (tot P) (tot Q)
  map-tot = fα΅’ .fst .to

  fam-square : u ∘ fam P ≑ fam Q ∘ map-tot
  fam-square = fα΅’ .fst .commute

  map-tot' : Hom[ map-tot ] (tot' P) (tot' Q)
  map-tot' = fα΅’ .snd

open Fam-over-hom

fam-over-hom
  : βˆ€ {x y} {u : Hom x y} {P : Disp-family.Ob[ x ]} {Q : Disp-family.Ob[ y ]}
  β†’ (f : Hom (tot P) (tot Q))
  β†’ u ∘ fam P ≑ fam Q ∘ f
  β†’ Hom[ f ] (tot' P) (tot' Q)
  β†’ Disp-family.Hom[ u ] P Q
fam-over-hom f p f' .fst .to = f
fam-over-hom f p f' .fst .commute = p
fam-over-hom f p f' .snd = f'

As a fibrationπŸ”—

If E\mathcal{E} is a fibration, and B\mathcal{B} has all pullbacks, then the category of displayed families is also a fibration. This follows by more abstract nonsense. In fact, this proof is why we defined it using abstract nonsense!

module _
  (fib : Cartesian-fibration E)
  (pb : βˆ€ {x y z} (f : Hom x y) (g : Hom z y) β†’ Pullback B f g)
  where

  Disp-family-fibration : Cartesian-fibration Disp-family
  Disp-family-fibration =
    fibration-∘ (Codomain-fibration B pb) (Change-of-base-fibration Dom E fib)

Constant familiesπŸ”—

There is a vertical functor from E\mathcal{E} to the category of E\mathcal{E}-valued families that takes each Ex\mathcal{E}_{x} to the constant family.

ConstDispFam : Vertical-functor E Disp-family
ConstDispFam .Vertical-functor.Fβ‚€' {x = x} x' =
  fam-over x id x'
ConstDispFam .Vertical-functor.F₁' {f = f} f' =
  fam-over-hom f id-comm f'
ConstDispFam .Vertical-functor.F-id' =
  Slice-pathp B refl refl ,β‚š sym (transport-refl _)
ConstDispFam .Vertical-functor.F-∘' =
  Slice-pathp B refl refl ,β‚š sym (transport-refl _)

This functor is in fact fibred, though the proof is somewhat involved!

ConstDispFam-fibred : is-vertical-fibred ConstDispFam
ConstDispFam-fibred {a = a} {b} {a'} {b'} {f = f} f' f'-cart = cart where
  open Vertical-functor ConstDispFam
  module f' = is-cartesian f'-cart
  open is-cartesian

We begin by fixing some notation for the constant family on b'.

  Ξ”b' : Disp-family.Ob[ b ]
  Ξ”b' = fam-over b id b'

Next, a short yet crucial lemma: if we have a displayed family over xx, a map m:B(x,a)m : \mathcal{B}(x, a), and a morphism of displayed families from PP to the constant family on bβ€²b', then we can construct a map from the displayed total space of PP to aβ€²a'. This is constructed via the universal map of the cartesian morphism fβ€²f'.

  coh : βˆ€ {x : Ob} {P : Disp-family.Ob[ x ]}
      β†’ (m : Hom x a) (h' : Disp-family.Hom[ f ∘ m ] P Ξ”b')
      β†’ f ∘ (m ∘ fam P) ≑ map-tot h'
  coh m h' = assoc _ _ _ βˆ™ fam-square h' βˆ™ idl _

  tot-univ : {x : Ob} {P : Disp-family.Ob[ x ]} (m : Hom x a)
    β†’ (h' : Disp-family.Hom[ f ∘ m ] P Ξ”b')
    β†’ Hom[ m ∘ fam P ] (tot' P) a'
  tot-univ {P = P} m h' =
    f'.universal (m ∘ fam P) $ hom[ coh m h' ]⁻ (map-tot' h')

We can use this lemma to construct a universal map in E\mathcal{E}.

  cart : is-cartesian Disp-family f (F₁' f')
  cart .universal {u' = u'} m h' =
    fam-over-hom (m ∘ fam u') (sym (idl _)) (tot-univ m h')

Commutivity and uniqueness follow from the fact that fβ€²f' is cartesian.

  cart .commutes {x} {P} m h' =
    Ξ£-path (Slice-pathp B _ (coh m h')) $ from-pathp $ cast[] $
      hom[] (f' ∘' map-tot' (cart .universal m h')) ≑[]⟨ ap hom[] (f'.commutes _ _) βŸ©β‰‘[]
      hom[] (hom[] (map-tot' h'))                   ≑[ coh m h' ]⟨ to-pathp⁻ (hom[]-βˆ™ _ _ βˆ™ reindex _ _) ⟩]
      map-tot' h' ∎
  cart .unique {x} {P} {m = m} {h' = h'} m' p =
    Ξ£-path (Slice-pathp B refl (sym (fam-square m' βˆ™ idl _)))
    $ f'.unique _ $ from-pathp⁻ $ cast[] {q = coh m h'} $
      f' ∘' hom[] (map-tot' m') ≑[]⟨ to-pathp (smashr _ (ap (f ∘_) (fam-square m' βˆ™ idl _)) βˆ™ reindex _ _) βŸ©β‰‘[]
      hom[] (f' ∘' map-tot' m') ≑[]⟨ ap map-tot' p βŸ©β‰‘[]
      map-tot' h'               ∎

We also provide a bundled version of this functor.

ConstDispFamVf : Vertical-fibred-functor E Disp-family
ConstDispFamVf .Vertical-fibred-functor.vert = ConstDispFam
ConstDispFamVf .Vertical-fibred-functor.F-cartesian = ConstDispFam-fibred