open import Cat.Functor.Adjoint.Hom open import Cat.Instances.Functor open import Cat.Displayed.Fibre open import Cat.Functor.Adjoint open import Cat.Displayed.Base open import Cat.Prelude import Cat.Displayed.Cocartesian.Indexing import Cat.Displayed.Cartesian.Indexing import Cat.Displayed.Cocartesian.Weak import Cat.Displayed.Cartesian.Weak import Cat.Displayed.Cocartesian import Cat.Displayed.Cartesian import Cat.Displayed.Reasoning import Cat.Reasoning module Cat.Displayed.Bifibration {o β oβ² ββ²} {β¬ : Precategory o β} (β° : Displayed β¬ oβ² ββ²) where
Bifibrationsπ
A displayed category is a bifibration if is it both a fibration and an opfibration. This means that is equipped with both reindexing and opreindexing functors, which allows us to both restrict and extend along morphisms in the base.
Note that a bifibration is not the same as a βprofunctor of categoriesβ; these are called two-sided fibrations, and are a distinct concept.
record is-bifibration : Type (o β β β oβ² β ββ²) where field fibration : Cartesian-fibration opfibration : Cocartesian-fibration module fibration = Cartesian-fibration fibration module opfibration = Cocartesian-fibration opfibration
Bifibrations and Adjointsπ
If is a bifibration, then its opreindexing functors are left adjoints to its reindexing functors. To see this, note that we need to construct a natural isomorphism between and . However, we have already shown that and are both naturally isomorphic to (see opfibrationβhom-iso and fibrationβhom-iso), so all we need to do is compose these natural isomorphisms!
module _ (bifib : is-bifibration) where open is-bifibration bifib open Cat.Displayed.Cartesian.Indexing β° fibration open Cat.Displayed.Cocartesian.Indexing β° opfibration cobase-changeβ£base-change : β {x y} (f : Hom x y) β cobase-change f β£ base-change f cobase-changeβ£base-change {x} {y} f = hom-natural-isoβadjoints $ (opfibrationβhom-iso opfibration f niβ»ΒΉ) niβ fibrationβhom-iso fibration f
In fact, if is a cartesian fibration where every reindexing functor has a left adjoint, then is a bifibration! To see this, note that we have a natural iso for every in the base. However, has a left adjoint for every , so we also have a natural isomorphism . Composing these yields a natural iso , which implies that is a weak opfibration due to hom-isoβweak-opfibration.
Furthermore, is a fibration, which allows us to upgrade the weak opfibration to an opfibration!
module _ (fib : Cartesian-fibration) where open Cartesian-fibration fib open Cat.Displayed.Cartesian.Indexing β° fib left-adjoint-base-changeβopfibration : (L : β {x y} β (f : Hom x y) β Functor (Fibre β° x) (Fibre β° y)) β (β {x y} β (f : Hom x y) β (L f β£ base-change f)) β Cocartesian-fibration left-adjoint-base-changeβopfibration L adj = cartesian+weak-opfibrationβopfibration fib $ hom-isoβweak-opfibration L Ξ» u β fibrationβhom-iso-from fib u niβ (adjunct-hom-iso-from (adj u) _ niβ»ΒΉ)
With some repackaging, we can see that this yields a bifibration.
left-adjoint-base-changeβbifibration : (L : β {x y} β (f : Hom x y) β Functor (Fibre β° x) (Fibre β° y)) β (β {x y} β (f : Hom x y) β (L f β£ base-change f)) β is-bifibration left-adjoint-base-changeβbifibration L adj .is-bifibration.fibration = fib left-adjoint-base-changeβbifibration L adj .is-bifibration.opfibration = left-adjoint-base-changeβopfibration L adj