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

Bifibrations🔗

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 XYX \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
  field
    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

  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 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:xyu : 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 uu^{*} 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

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

Adjoints from cocartesian maps🔗

Let f:XYf : X \to Y be a morphism in B\mathcal{B}, and let L:EXEYL : \mathcal{E}_{X} \to \mathcal{E}_{Y} be a functor. If we are given a natural transformation η:IdfL\eta : \operatorname{Id}_{} \to f^{*} \circ L with fη\overline{f} \circ \eta cocartesian, then LL is a left adjoint to ff^{*}.

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

EXLA,BEYA,fB.\mathcal{E}_{X}{L A, B} \simeq \mathcal{E}_{Y}{A, f^{*}B}\text{.}

The map vf(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:AfBv : A \to f^{*} B is a vertical map in E\mathcal{E}, we can construct a vertical map LABLA \to B by factoring fv\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)

      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 _))))

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