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

open Cat.Reasoning B open Displayed E open Cat.Displayed.Reasoning E open Functor open Total-hom open /-Obj open Slice-hom

# 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
$\mathcal{B}$-indexed
families of
$\mathcal{E}$
objects. To construct such a fibration, we recall that every family
$P : X \to \mathrm{Type}$
is equivalent to the total space of its fibres (see here for more
details). Itβs quite rare for
$\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
$\mathcal{B}(a, x)$
to be a sort of βgeneralized familyβ over
$x$,
where
$a$
is playing the role of the total space. Objects
$a' : \mathcal{E}_{a}$
over
$a$
then encode an
$x$-indexed
family of
$\mathcal{E}$
objects.

This is all quite abstract, so letβs look at an example. Consider some category $\mathcal{E}$ fibred over $\mathbf{Sets}$. There is already a natural notion of an $I$-indexed family of $\mathcal{E}$-objects here; namely, a map $P : I \to \mathrm{Set}$ and a map $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 $\mathrm{fst} : \Sigma (i : I) P(i) \to I$ by taking the total space of $P$. Furthermore, $\Sigma (i : I) P(i)$ is a set, so we can consider the space of objects $\mathcal{E}_{\Sigma (i : I) P(i)}$. We can embed each $X(i) : E_{P(i)}$ into $\mathcal{E}_{\Sigma (i : I) P(i)}$ by reindexing along the second projection $\Sigma (i : I) P(i) \to P(i)$

To show the reverse direction, suppose we have some function $f : A \to I$, along with an object $\mathcal{E}_{A}$. We can obtain a family of sets $f^{-1} : I \to \mathrm{Set}$ by taking the fibres of $f$. Furthermore, note that for each $i : I$, we have a map $f^{-1}(i) \to A$ from the fibre of $f$ at $A$ to $A$; reindexing along this map yields an object $\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 : \mathcal{B}$
shall be triples
$(a : \mathcal{B}) \times \mathcal{B}(a, x) \times \mathcal{E}_{a}$,
and morphisms
$f : (a, f, a') \to (b, g, b')$
over
$u : x \to y$
are given by triples
$(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
$\mathcal{B}$.
The remaining data involving
$\mathcal{E}$
is then added by composing the codomain fibration with the base change of
$\mathcal{E}$
along the functor
$\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, Q$ is given by a map between $\mathcal{B}$-valued total spaces; this map must commute with the family structure on $P$ and $Q$. Finally, we have a map between the $\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
$\mathcal{E}$
is a fibration, and
$\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 $\mathcal{E}$ to the category of $\mathcal{E}$-valued families that takes each $\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 $x$, a map $m : \mathcal{B}(x, a)$, and a morphism of displayed families from $P$ to the constant family on $b'$, then we can construct a map from the displayed total space of $P$ to $a'$. This is constructed via the universal map of the cartesian morphism $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 $\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'$ 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