Bifibrations

src/Cat/Displayed/Bifibration.lagda.md

@@ -0,0 +1,132 @@
+```agda
+open import Cat.Displayed.Base
+open import Cat.Displayed.Fibre
+open import Cat.Functor.Adjoint
+open import Cat.Functor.Adjoint.Hom
+open import Cat.Instances.Functor
+open import Cat.Prelude
+
+import Cat.Displayed.Cartesian.Indexing
+import Cat.Displayed.Cocartesian.Indexing
+import Cat.Displayed.Cocartesian
+import Cat.Displayed.Cocartesian.Weak
+import Cat.Displayed.Cartesian
+import Cat.Displayed.Cartesian.Weak
+import Cat.Displayed.Reasoning
+import Cat.Reasoning
+
+module Cat.Displayed.Bifibration
+  {o ℓ o′ ℓ′} {ℬ : Precategory o ℓ} (ℰ : Displayed ℬ o′ ℓ′) where
+```
+
+<!--
+```agda
+open Cat.Displayed.Cocartesian ℰ
+open Cat.Displayed.Cocartesian.Weak ℰ
+open Cat.Displayed.Cartesian ℰ
+open Cat.Displayed.Cartesian.Weak ℰ
+open Cat.Displayed.Reasoning ℰ
+
+open Precategory ℬ
+open Displayed ℰ
+```
+-->
+
+
+# Bifibrations
+
+A displayed category $\cE \liesover \cB$ is a **bifibration** if it both
+a fibration and an opfibration. This means that $\cE$ 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.
+
+[reindexing]: Cat.Displayed.Cartesian.Indexing.html
+[opreindexing]: Cat.Displayed.Cocartesian.Indexing.html
+
+<!--
+[TODO: Reed M, 31/01/2023] Link to two-sided fibration
+when that page is written.
+-->
+
+
+```agda
+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 $\cE$ is a bifibration, then its opreindexing functors are
+[left adjoints] to reindexing functors. To see this, note that we need
+to construct a natural isomorphism between $\cE_{y}(u_{*}(-),-)$ and
+$\cE_{x}(-,u^{*}(-))$. However, we have already shown that
+$\cE_{y}(u_{*}(-),-)$ and $\cE_{x}(-,u^{*}(-))$ are both naturally
+isomorphic to $\cE_{u}(-,-)$ (see `opfibration→hom-iso`{.Agda} and
+`fibration→hom-iso`{.Agda}), so all we need to do is compose these
+natural isomorphisms!
+
+[left adjoints]: Cat.Functor.Adjoint.html
+
+```agda
+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 $\cE$ is a cartesian fibration where every reindexing
+functor has a left adjoint, then $\cE$ is a bifibration!
+To see this, note that we have a natural iso
+$\cE_{u}(x',-) \simeq \cE_{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
+$\cE_{x}(x', u^{*}(-)) \simeq \cE_{y}(L_{u}(x'),-)$. Composing these
+yields a natural iso $\cE_{u}(x',-) \simeq \cE_{y}(L_{u}(x'),-)$, which
+implies that $\cE$ is a weak opfibration due to
+`hom-iso→weak-opfibration`{.Agda}.
+
+Furthermore, $\cE$ is a fibration, which allows us to upgrade the
+weak opfibration to an opfibration!
+
+```agda
+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.
+
+```agda
+  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
+```

src/Cat/Displayed/Cartesian.lagda.md

@@ -147,6 +147,38 @@ composite, rather than displayed directly over a composite.
     ·· ap (coe1→0 (λ i → Hom[ q i ] u′ a′)) (sym (unique m₂′ (from-pathp⁻ β)))
 ```
 
+Furthermore, if $f'' : a'' \to_{f} b'$ is also displayed over $f$,
+there's a unique vertical map $a'' \to a'$. This witnesses the fact that
+every cartesian map is [weakly cartesian].
+
+[weakly cartesian]: Cat.Displayed.Cartesian.Weak.html
+
+```agda
+  universalv : ∀ {a″} (f″ : Hom[ f ] a″ b′) → Hom[ id ] a″ a′
+  universalv f″ = universal′ (idr _) f″
+
+  commutesv
+    : ∀ {x′} → (g′ : Hom[ f ] x′ b′)
+    → f′ ∘′ universalv g′ ≡[ idr _ ] g′
+  commutesv = commutesp (idr _)
+
+  uniquev
+    : ∀ {x′} {g′ : Hom[ f ] x′ b′}
+    → (h′ : Hom[ id ] x′ a′)
+    → f′ ∘′ h′ ≡[ idr _ ] g′
+    → h′ ≡ universalv g′
+  uniquev h′ p = uniquep (idr f) refl (idr f) h′ p
+
+  uniquev₂
+    : ∀ {x′} {g′ : Hom[ f ] x′ b′}
+    → (h′ h″ : Hom[ id ] x′ a′)
+    → f′ ∘′ h′ ≡[ idr _ ] g′
+    → f′ ∘′ h″ ≡[ idr _ ] g′
+    → h′ ≡ h″
+  uniquev₂ h′ h″ p q =
+    uniquep₂ (idr f) refl (idr f) h′ h″ p q
+```
+
 ## Properties of Cartesian Morphisms
 
 The composite of 2 cartesian morphisms is in turn cartesian.
@@ -397,6 +429,35 @@ vertical+cartesian→invertible {x′ = x′} {x″ = x″} {f′ = f′} f-cart
       hom[] id′ ∎
 ```
 
+Furthermore, $f' : x' \to_{f} y'$ is cartesian if and only if the
+function $f \cdot' -$ is an equivalence.
+
+```agda
+postcompose-equiv→cartesian
+  : ∀ {x y x′ y′} {f : Hom x y}
+  → (f′ : Hom[ f ] x′ y′)
+  → (∀ {w w′} {g : Hom w x} → is-equiv {A = Hom[ g ] w′ x′} (f′ ∘′_))
+  → is-cartesian f f′
+postcompose-equiv→cartesian f′ eqv .is-cartesian.universal m h′ =
+  equiv→inverse eqv h′
+postcompose-equiv→cartesian f′ eqv .is-cartesian.commutes m h′ =
+  equiv→counit eqv h′
+postcompose-equiv→cartesian f′ eqv .is-cartesian.unique m′ p =
+  sym (equiv→unit eqv m′) ∙ ap (equiv→inverse eqv) p
+
+cartesian→postcompose-equiv
+  : ∀ {x y z x′ y′ z′} {f : Hom y z} {g : Hom x y} {f′ : Hom[ f ] y′ z′}
+  → is-cartesian f f′
+  → is-equiv {A = Hom[ g ] x′ y′} (f′ ∘′_)
+cartesian→postcompose-equiv cart =
+  is-iso→is-equiv $
+    iso (universal _)
+        (commutes _)
+        (λ g′ → sym (unique g′ refl))
+  where open is-cartesian cart
+```
+
+
 ## Cartesian Lifts
 
 We call an object $a'$ over $a$ together with a Cartesian arrow $f' : a'
@@ -436,6 +497,23 @@ record Cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
     Cartesian-lift (has-lift f y′)
 ```
 
+Note that if $\cE$ is a fibration, we can define an operation that
+allows us to move vertical morphisms between fibres. This actually
+extends to a collection of functors, called [base change functors].
+This operation is also definable for [weak fibrations], as it only
+uses the universal property that yields a vertical morphism.
+
+[base change functors]: Cat.Displayed.Cartesian.Indexing.html
+[weak fibrations]: Cat.Displayed.Cartesian.Weak.html#is-weak-cartesian-fibration
+
+```agda
+  rebase : ∀ {x y y′ y″} → (f : Hom x y)
+           → Hom[ id ] y′ y″
+           → Hom[ id ] (has-lift.x′ f y′) (has-lift.x′ f y″)
+  rebase f vert =
+    has-lift.universalv f _ (hom[ idl _ ] (vert ∘′ has-lift.lifting f _))
+```
+
 A Cartesian fibration is a displayed category having Cartesian lifts for
 every right corner.
 
@@ -472,24 +550,3 @@ fibre over a ring $R$ is the category of $R$-modules, Cartesian lifts
 are given by restriction of scalars.
 
 [category of modules]: Algebra.Ring.Module.html
-
-## Properties of Cartesian Fibrations
-
-If $\cE$ is a fibration, then every morphism is equivalent to
-a vertical morphism.
-
-```agda
-open Cartesian-lift
-open Cartesian-fibration
-
-fibration→vertical-equiv
-  : ∀ {X Y X′ Y′}
-  → (fib : Cartesian-fibration)
-  → (u : Hom X Y)
-  → Hom[ u ] X′ Y′ ≃ Hom[ id ] X′ (fib .has-lift u Y′ .x′)
-fibration→vertical-equiv fib u = Iso→Equiv $
-  (λ u′ → fib .has-lift _ _ .universal id (hom[ idr u ]⁻ u′)) ,
-  iso (λ u′ → hom[ idr u ] (fib .has-lift _ _ .lifting ∘′ u′))
-      (λ u′ → sym $ fib .has-lift _ _ .unique u′ (sym (hom[]-∙ _ _ ∙ liberate _)))
-      (λ u′ → (hom[]⟩⟨ fib .has-lift _ _ .commutes _ _) ·· hom[]-∙ _ _ ·· liberate _)
-```