Comprehension coproducts

src/Cat/Displayed/Bifibration.lagda.md

@@ -2,9 +2,9 @@
 ```agda
 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.Displayed.Fibre
 open import Cat.Prelude
 
 import Cat.Displayed.Cocartesian.Indexing
@@ -14,6 +14,7 @@ import Cat.Displayed.Cartesian.Weak
 import Cat.Displayed.Cocartesian
 import Cat.Displayed.Cartesian
 import Cat.Displayed.Reasoning
+import Cat.Displayed.Fibre.Reasoning
 import Cat.Reasoning
 ```
 -->
@@ -31,8 +32,13 @@ open Cat.Displayed.Cartesian ℰ
 open Cat.Displayed.Cartesian.Weak ℰ
 open Cat.Displayed.Reasoning ℰ
 
-open Precategory ℬ
+open Cat.Reasoning ℬ
 open Displayed ℰ
+open Functor
+open _⊣_
+open _=>_
+private
+  module Fib = Cat.Displayed.Fibre.Reasoning ℰ
 ```
 -->
 
@@ -45,8 +51,9 @@ 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.
+Note that a bifibration is *not* the same as a "profunctor valued in
+categories". Those are a distinct concept, called **two-sided
+fibrations**.
 
 [reindexing]: Cat.Displayed.Cartesian.Indexing.html
 [opreindexing]: Cat.Displayed.Cocartesian.Indexing.html
@@ -56,7 +63,6 @@ these are called **two-sided fibrations**, and are a distinct concept.
 when that page is written.
 -->
 
-
 ```agda
 record is-bifibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
   field
@@ -70,14 +76,15 @@ record is-bifibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
 # Bifibrations and Adjoints
 
 If $\cE$ 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 $\cE_{y}(u_{*}(-),-)$ and
+adjoints]] to its reindexing functors.  To show this, it will suffice to
+construct 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
+isomorphic to $\cE_{u}(-,-)$[^proof], so all we need to do is compose these
 natural isomorphisms!
 
+[^proof]: see `opfibration→hom-iso`{.Agda} and `fibration→hom-iso`{.Agda}.
+
 ```agda
 module _ (bifib : is-bifibration) where
   open is-bifibration bifib
@@ -92,19 +99,21 @@ module _ (bifib : is-bifibration) where
       (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}.
+In fact, if $\cE \liesover \cB$ is a cartesian fibration where every
+reindexing functor has a left adjoint, then $\cE$ is a bifibration!
+
+Since $\cE$ is a fibration, every $u : x \to y$ in $\cB$ induces a
+natural isomorphism $\cE_{u}(x',-) \simeq \cE_{x}(x', u^{*}(-))$, by the
+universal property of [[cartesian lifts]]. If $u^{*}$ additionally has a
+left adjoint $L_{u}$, we have natural isomorphisms
+
+$$
+\cE_{u}(x',-) \simeq \cE_{x}(x',u^{*}(-)) \simeq \cE_{y}(L_{u}(x')-)\text{,}
+$$
 
-Furthermore, $\cE$ is a fibration, which allows us to upgrade the
-weak opfibration to an opfibration!
+which implies $\cE$ `is a weak opfibration`{.Agda
+id=`hom-iso→weak-opfibration}; and any weak opfibration that's also a
+fibration is a proper opfibration.
 
 ```agda
 module _ (fib : Cartesian-fibration) where
@@ -121,8 +130,7 @@ module _ (fib : Cartesian-fibration) where
       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))
@@ -133,3 +141,91 @@ With some repackaging, we can see that this yields a bifibration.
   left-adjoint-base-change→bifibration L adj .is-bifibration.opfibration =
     left-adjoint-base-change→opfibration L adj
 ```
+-->
+
+## Adjoints from cocartesian maps
+
+Let $f : X \to Y$ be a morphism in $\cB$, and let $L : \cE_{X} \to
+\cE_{Y}$ be a functor. If we are given a natural transformation $\eta :
+\rm{Id} \to f^{*} \circ L$ with $\overline{f} \circ \eta$ cocartesian,
+then $L$ is a left adjoint to $f^{*}$.
+
+```agda
+  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 $\hom$-sets
+
+$$\cE_{X}{L A, B} \simeq \cE_{Y}{A, f^{*}B}\text{.}$$
+
+The map $v \mapsto f^{*}(v) \circ \eta$ gives us the forward direction
+of this equivalence, so all that remains is to find an inverse. Since
+$\overline{f}\circ\eta$ is cocartesian, it satisfies a _mapping-out_
+universal property: if $v : A \to f^{*} B$ is a vertical map in $\cE$,
+we can construct a vertical map $LA \to B$ by factoring $\overline{f}
+\circ v$ through the cocartesian $\overline{f} \circ \eta$; The actual
+_universal property_ says that this factorising process is an
+equivalence.
+
+~~~{.quiver}
+\begin{tikzcd}
+  &&& B \\
+  A && LA \\
+  &&& Y \\
+  X && Y
+  \arrow["{\overline{f} \circ \eta}", from=2-1, to=2-3]
+  \arrow["f"', from=4-1, to=4-3]
+  \arrow[lies over, from=2-1, to=4-1]
+  \arrow[lies over, from=2-3, to=4-3]
+  \arrow[dashed, from=2-3, to=1-4]
+  \arrow["id"', from=4-3, to=3-4]
+  \arrow[lies over, from=1-4, to=3-4]
+  \arrow["{\overline{f} \circ v}", curve={height=-12pt}, from=2-1, to=1-4]
+  \arrow["f", curve={height=-12pt}, from=4-1, to=3-4]
+\end{tikzcd}
+~~~
+
+```agda
+  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 ] (F₀ L 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 _))
+```
+
+<details>
+<summary>Futhermore, this equivalence is natural, but that's a very tedious proof.
+</summary>
+
+```agda
+      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 _))))
+```
+</details>

src/Cat/Displayed/Cartesian.lagda.md

@@ -19,7 +19,7 @@ open Cat.Displayed.Morphism E
 open DR E
 ```
 
-# Cartesian morphisms and Fibrations
+# Cartesian morphisms and fibrations
 
 While [[displayed categories]] give the essential framework we need to
 express the idea of families of categories indexed by a category, they
@@ -34,7 +34,7 @@ $\Cat$ is a [[bicategory]] of categories. It turns out that we can
 characterise this assignment entirely in terms of the displayed objects
 and morphisms in $\cE$!
 
-:::{.definition #cartesian-morphism}
+:::{.definition #cartesian-morphism alias="cartesian-map"}
 Fix an arrow $f : a \to b$ in the base category $\cB$, an object $a'$
 over $a$ (resp. $b'$ over $b$), and an arrow $f' : a' \to_f b'$ over
 $f$. We say that $f'$ is **cartesian** if, up to very strong handwaving,
@@ -575,7 +575,7 @@ cartesian→postcompose-equiv cart =
 ```
 
 
-## Cartesian Lifts
+## Cartesian lifts {defines="cartesian-lift"}
 
 We call an object $a'$ over $a$ together with a Cartesian arrow $f' : a'
 \to b'$ a _Cartesian lift_ of $f$. Cartesian lifts, defined by universal
@@ -604,7 +604,7 @@ some choices to be made, and invoking the axiom of choice makes an
 there is exactly _one_ choice to be made, that is, no choice at all.
 Thus, we do not dwell on the distinction.
 
-:::{.definition #fibred-category alias="cartesian-fibration"}
+:::{.definition #fibred-category alias="cartesian-fibration fibration"}
 ```agda
 record Cartesian-fibration : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
   no-eta-equality
@@ -630,7 +630,7 @@ uses the universal property that yields a vertical morphism.
            → 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 _))
+    has-lift.universal′ f _ id-comm (vert ∘′ has-lift.lifting f _)
 ```
 
 A Cartesian fibration is a displayed category having Cartesian lifts for