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 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 $
      fibrationβ†’hom-iso fibration f ∘ni opfibrationβ†’hom-iso opfibration f ni⁻¹

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 →
      adjunct-hom-iso-from (adj u) _ ni⁻¹ ∘ni fibrationβ†’hom-iso-from fib u

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

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

  1. see opfibrationβ†’hom-iso and fibrationβ†’hom-iso.β†©οΈŽ