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

Bifibrations🔗

A displayed category $E B$ is a bifibration if is it both a fibration and an opfibration. This means that $E$ is equipped with both reindexing and opreindexing functors, which allows us to both restrict and extend along morphisms $X \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$ 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 $E_{y} (u_{*} (-), -)$ and $E_{x} (-, u^{*} (-)) .$ However, we have already shown that $E_{y} (u_{*} (-), -)$ and $E_{x} (-, u^{*} (-))$ are both naturally isomorphic to $E_{u} (-, -)$ ¹, 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 $E B$ is a cartesian fibration where every reindexing functor has a left adjoint, then $E$ is a bifibration!

Since $E$ is a fibration, every $u : x \to y$ in $B$ induces a natural isomorphism $E_{u} (x^{'}, -) ≃ E_{x} (x^{'}, u^{*} (-)),$ by the universal property of cartesian lifts. If $u^{*}$ additionally has a left adjoint $L_{u},$ we have natural isomorphisms

E_{u} (x^{'}, -) ≃ E_{x} (x^{'}, u^{*} (-)) ≃ E_{y} (L_{u} (x^{'}) -),

which implies $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 : X \to Y$ be a morphism in $B,$ and let $L : E_{X} \to E_{Y}$ be a functor. If we are given a natural transformation $η : Id \to f^{*} \circ L$ with $\overline{f} \circ η$ cocartesian, then $L$ is a left adjoint to $f^{*} .$

  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 -sets$

E_{X} L A, B ≃ E_{Y} A, f^{*} B .

The map $v \mapsto f^{*} (v) \circ η$ gives us the forward direction of this equivalence, so all that remains is to find an inverse. Since $\overline{f} \circ η$ is cocartesian, it satisfies a mapping-out universal property: if $v : A \to f^{*} B$ is a vertical map in $E,$ we can construct a vertical map $L A \to B$ by factoring $\overline{f} \circ v$ through the cocartesian $\overline{f} \circ η;$ 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 ] (L .F₀ 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 and fibration→hom-iso.↩︎