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.Fibre.Reasoning
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

open Cat.Displayed.Cocartesian β°
open Cat.Displayed.Cocartesian.Weak β°
open Cat.Displayed.Cartesian β°
open Cat.Displayed.Cartesian.Weak β°
open Cat.Displayed.Reasoning β°

open Cat.Reasoning β¬
open Displayed β°
open Functor
open _β£_
open _=>_
private
module Fib = Cat.Displayed.Fibre.Reasoning β°


# 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


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 $(opfibrationβhom-iso opfibration f niβ»ΒΉ) βni fibrationβhom-iso fibration f  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 β

  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
fib


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