open import Cat.Functor.Adjoint.Hom
open import Cat.Instances.Functor
open import Cat.Displayed.Fibre
open import Cat.Functor.Adjoint
open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Cocartesian.Indexing
import Cat.Displayed.Cartesian.Indexing
import Cat.Displayed.Cocartesian.Weak
import Cat.Displayed.Cartesian.Weak
import Cat.Displayed.Cocartesian
import Cat.Displayed.Cartesian
import Cat.Displayed.Reasoning
import Cat.Reasoning

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 X→YX \to Y in the base.

Note that a bifibration is not the same as a β€œprofunctor of categories”; these are called two-sided fibrations, and are a distinct concept.

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 see this, note that we need to construct a 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}(-,-) (see opfibrationβ†’hom-iso and fibrationβ†’hom-iso), 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\mathcal{E} is a cartesian fibration where every reindexing functor has a left adjoint, then E\mathcal{E} is a bifibration! To see this, note that we have a natural iso Eu(xβ€²,βˆ’)≃Ex(xβ€²,uβˆ—(βˆ’))\mathcal{E}_{u}(x',-) \simeq \mathcal{E}_{x}(x', u^{*}(-)) for every u:xβ†’yu : x \to y in the base. However, uβˆ—u^{*} has a left adjoint LuL_{u} for every uu, so we also have a natural isomorphism Ex(xβ€²,uβˆ—(βˆ’))≃Ey(Lu(xβ€²),βˆ’)\mathcal{E}_{x}(x', u^{*}(-)) \simeq \mathcal{E}_{y}(L_{u}(x'),-). Composing these yields a natural iso Eu(xβ€²,βˆ’)≃Ey(Lu(xβ€²),βˆ’)\mathcal{E}_{u}(x',-) \simeq \mathcal{E}_{y}(L_{u}(x'),-), which implies that E\mathcal{E} is a weak opfibration due to hom-isoβ†’weak-opfibration.

Furthermore, E\mathcal{E} is a fibration, which allows us to upgrade the weak opfibration to an 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⁻¹)

With some repackaging, we can see that this yields a bifibration.

  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