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 -indexed families of objects. To construct such a fibration, we recall that every family is equivalent to the total space of its fibres (see here for more details). Itβs quite rare for to have something that looks like a universe, but it does have enough structure to talk about fibres! We can consider a morphism to be a sort of βgeneralized familyβ over , where is playing the role of the total space. Objects over then encode an -indexed family of objects.
This is all quite abstract, so letβs look at an example. Consider some category fibred over . There is already a natural notion of an -indexed family of -objects here; namely, a map and a map . To see that we obtain the definition from before, note that we can turn this family of sets into a map by taking the total space of . Furthermore, is a set, so we can consider the space of objects . We can embed each into by reindexing along the second projection
To show the reverse direction, suppose we have some function , along with an object . We can obtain a family of sets by taking the fibres of . Furthermore, note that for each , we have a map from the fibre of at to ; reindexing along this map yields an object as desired.
Now that we are armed with the intuition, on with the construction! Recall that the object objects over shall be triples , and morphisms over are given by triples . The first portion of this data can be obtained by using the codomain fibration over . The remaining data involving is then added by composing the codomain fibration with the base change of along the functor 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 is given by a map between -valued total spaces; this map must commute with the family structure on and . Finally, we have a map between the -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 is a fibration, and 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 to the category of -valued families that takes each 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 , a map , and a morphism of displayed families from to the constant family on , then we can construct a map from the displayed total space of to . This is constructed via the universal map of the cartesian morphism .
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 .
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 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