module Cat.Displayed.Bifibration {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where
open Cat.Displayed.Cocartesian ℰ open Cat.Displayed.Cocartesian.Weak ℰ open Cat.Displayed.Cartesian ℰ open Cat.Displayed.Cartesian.Weak ℰ open Cat.Displayed.Reasoning ℰ open Cat.Reasoning ℬ open Displayed ℰ open Functor open _⊣_ open _=>_ private module Fib = Cat.Displayed.Fibre.Reasoning ℰ
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 valued in categories”. Those are a distinct concept, called two-sided fibrations.
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 show this, it will suffice to construct natural isomorphism between and . However, we have already shown that and are both naturally isomorphic to 1, 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!
Since is a fibration, every in induces a natural isomorphism , by the universal property of cartesian lifts. If additionally has a left adjoint , we have natural isomorphisms
which implies
is a weak opfibration
; and any
weak opfibration that’s also a fibration is a proper 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⁻¹)
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
Adjoints from cocartesian maps🔗
Let be a morphism in , and let be a functor. If we are given a natural transformation with cocartesian, then is a left adjoint to .
cocartesian→left-adjoint-base-change : ∀ {x y} {L : Functor (Fibre ℰ x) (Fibre ℰ y)} {f : Hom x y} → (L-unit : Id => base-change f F∘ L) → (∀ x → is-cocartesian (f ∘ id) (has-lift.lifting f (L .F₀ x) ∘′ L-unit .η x)) → L ⊣ base-change f
We will construct the adjunction by constructing a natural equivalence of -sets
The map gives us the forward direction of this equivalence, so all that remains is to find an inverse. Since is cocartesian, it satisfies a mapping-out universal property: if is a vertical map in , we can construct a vertical map by factoring through the cocartesian ; The actual universal property says that this factorising process is an equivalence.
cocartesian→left-adjoint-base-change {x = x} {y = y} {L = L} {f = f} L-unit cocart = hom-iso→adjoints (λ v → base-change f .F₁ v Fib.∘ L-unit .η _) precompose-equiv equiv-natural where module cocart x = is-cocartesian (cocart x) module f* = Functor (base-change f) precompose-equiv : ∀ {x′ : Ob[ x ]} {y′ : Ob[ y ]} → is-equiv {A = Hom[ id ] (F₀ L x′) y′} (λ v → f*.₁ v Fib.∘ L-unit .η x′) precompose-equiv {x′} {y′} = is-iso→is-equiv $ iso (λ v → cocart.universalv _ (has-lift.lifting f _ ∘′ v)) (λ v → has-lift.uniquep₂ _ _ _ _ refl _ _ (Fib.pulllf (has-lift.commutesp f _ id-comm _) ∙[] symP (assoc′ _ _ _) ∙[] cocart.commutesv x′ _) refl) (λ v → symP $ cocart.uniquep x′ _ _ _ _ $ assoc′ _ _ _ ∙[] Fib.pushlf (symP $ has-lift.commutesp f _ id-comm _))
Futhermore, this equivalence is natural, but that’s a very tedious proof.
equiv-natural : hom-iso-natural {L = L} {R = base-change f} (λ v → f*.₁ v Fib.∘ L-unit .η _) equiv-natural g h k = has-lift.uniquep₂ _ _ _ _ _ _ _ (Fib.pulllf (has-lift.commutesp f _ id-comm _) ∙[] pushl[] _ (pushl[] _ (to-pathp⁻ (smashr _ _)))) (Fib.pulllf (has-lift.commutesp f _ id-comm _) ∙[] extendr[] _ (Fib.pulllf (Fib.pulllf (has-lift.commutesp f _ id-comm _))) ∙[] extendr[] _ (pullr[] _ (to-pathp (L-unit .is-natural _ _ h))) ∙[] pullr[] _ (Fib.pulllf (extendr[] _ (has-lift.commutesp f _ id-comm _))))
see
opfibration→hom-iso
andfibration→hom-iso
.↩︎