module Cat.Displayed.Bifibration
  {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where


A displayed category EB\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B} is a bifibration if is it both a fibration and an opfibration. This means that E\mathcal{E} is equipped with both reindexing and opreindexing functors, which allows us to both restrict and extend along morphisms X→YX \to Y 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
    fibration : Cartesian-fibration
    opfibration : Cocartesian-fibration

  module fibration = Cartesian-fibration fibration
  module opfibration = Cocartesian-fibration opfibration

Bifibrations and Adjoints🔗

If E\mathcal{E} 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 Ey(u∗(−),−)\mathcal{E}_{y}(u_{*}(-),-) and Ex(−,u∗(−))\mathcal{E}_{x}(-,u^{*}(-)). However, we have already shown that Ey(u∗(−),−)\mathcal{E}_{y}(u_{*}(-),-) and Ex(−,u∗(−))\mathcal{E}_{x}(-,u^{*}(-)) are both naturally isomorphic to Eu(−,−)\mathcal{E}_{u}(-,-)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

    : ∀ {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 EB\mathcal{E} \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} \mathcal{B} is a cartesian fibration where every reindexing functor has a left adjoint, then E\mathcal{E} is a bifibration!

Since E\mathcal{E} is a fibration, every u:x→yu : x \to y in B\mathcal{B} induces a natural isomorphism Eu(x′,−)≃Ex(x′,u∗(−))\mathcal{E}_{u}(x',-) \simeq \mathcal{E}_{x}(x', u^{*}(-)), by the universal property of cartesian lifts. If u∗u^{*} additionally has a left adjoint LuL_{u}, we have natural isomorphisms

Eu(x′,−)≃Ex(x′,u∗(−))≃Ey(Lu(x′)−), \mathcal{E}_{u}(x',-) \simeq \mathcal{E}_{x}(x',u^{*}(-)) \simeq \mathcal{E}_{y}(L_{u}(x')-)\text{,}

which implies E\mathcal{E} 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

    : (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⁻¹)

Adjoints from cocartesian maps🔗

Let f:X→Yf : X \to Y be a morphism in B\mathcal{B}, and let L:EX→EYL : \mathcal{E}_{X} \to \mathcal{E}_{Y} be a functor. If we are given a natural transformation η:Id⁡→f∗∘L\eta : \operatorname{Id}_{} \to f^{*} \circ L with f‾∘η\overline{f} \circ \eta cocartesian, then LL is a left adjoint to f∗f^{*}.

    : ∀ {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 Hom\mathbf{Hom}-sets

EXLA,B≃EYA,f∗B.\mathcal{E}_{X}{L A, B} \simeq \mathcal{E}_{Y}{A, f^{*}B}\text{.}

The map v↦f∗(v)∘ηv \mapsto f^{*}(v) \circ \eta gives us the forward direction of this equivalence, so all that remains is to find an inverse. Since f‾∘η\overline{f}\circ\eta is cocartesian, it satisfies a mapping-out universal property: if v:A→f∗Bv : A \to f^{*} B is a vertical map in E\mathcal{E}, we can construct a vertical map LA→BLA \to B by factoring f‾∘v\overline{f} \circ v through the cocartesian f‾∘η\overline{f} \circ \eta; 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)

        : ∀ {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′ _)
        (λ 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.
        : 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 _))))

  1. see opfibration→hom-iso and fibration→hom-iso.↩︎