open import Cat.Functor.Adjoint.Hom
open import Cat.Instances.Functor
open import Cat.Displayed.Fibre
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 $\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 $\mathcal{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 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


If $\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 $\mathcal{E}_{y}(u_{*}(-),-)$ and $\mathcal{E}_{x}(-,u^{*}(-))$. However, we have already shown that $\mathcal{E}_{y}(u_{*}(-),-)$ and $\mathcal{E}_{x}(-,u^{*}(-))$ are both naturally isomorphic to $\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 $\mathcal{E}$ is a cartesian fibration where every reindexing functor has a left adjoint, then $\mathcal{E}$ is a bifibration! To see this, note that we have a natural iso $\mathcal{E}_{u}(x',-) \simeq \mathcal{E}_{x}(x', u^{*}(-))$ for every $u : x \to y$ in the base. However, $u^{*}$ has a left adjoint $L_{u}$ for every $u$, so we also have a natural isomorphism $\mathcal{E}_{x}(x', u^{*}(-)) \simeq \mathcal{E}_{y}(L_{u}(x'),-)$. Composing these yields a natural iso $\mathcal{E}_{u}(x',-) \simeq \mathcal{E}_{y}(L_{u}(x'),-)$, which implies that $\mathcal{E}$ is a weak opfibration due to hom-iso→weak-opfibration. Furthermore, $\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 →

  left-adjoint-base-change→bifibration