chore: Tweak bicategory prose and address review comments

Co-authored-by: Amélia Liao <me@amelia.how>

Author: aathn

src/Cat/Bi/Base.lagda.md

@@ -713,11 +713,12 @@ diagrams **in** bicategories, which are (mercifully) limited to 2-cells.
   open Modification
   open _=>ₗ_
 
-  Mod-pathp : {α α' β β' : F =>ₗ G}
-            → (p : α ≡ α') (q : β ≡ β')
-            → {a : Modification α β} {b : Modification α' β'}
-            → (∀ x → PathP _ (a .Γ x) (b .Γ x))
-            → PathP (λ i → Modification (p i) (q i)) a b
+  Mod-pathp
+    : {α α' β β' : F =>ₗ G}
+    → (p : α ≡ α') (q : β ≡ β')
+    → {a : Modification α β} {b : Modification α' β'}
+    → (∀ x → PathP _ (a .Γ x) (b .Γ x))
+    → PathP (λ i → Modification (p i) (q i)) a b
   Mod-pathp p q path i .Γ x                            = path x i
   Mod-pathp p q {a} {b} path i .is-natural {x} {y} {f} =
     is-prop→pathp
@@ -726,10 +727,11 @@ diagrams **in** bicategories, which are (mercifully) limited to 2-cells.
       (a .is-natural)
       (b .is-natural) i
 
-  _Γᵈ_ : {α α' β β' : F =>ₗ G} {p : α ≡ α'} {q : β ≡ β'}
-       → {a : Modification α β} {b : Modification α' β'}
-       → PathP (λ i → Modification (p i) (q i)) a b
-       → ∀ x → PathP _ (a .Γ x) (b .Γ x)
+  _Γᵈ_
+    : {α α' β β' : F =>ₗ G} {p : α ≡ α'} {q : β ≡ β'}
+    → {a : Modification α β} {b : Modification α' β'}
+    → PathP (λ i → Modification (p i) (q i)) a b
+    → ∀ x → PathP _ (a .Γ x) (b .Γ x)
   p Γᵈ x = apd (λ i e → e .Γ x) p
 
   _Γₚ_ : {α β : F =>ₗ G} {a b : Modification α β} → a ≡ b → ∀ x → a .Γ x ≡ b .Γ x

src/Cat/Bi/Diagram/Colimit.lagda.md

@@ -61,7 +61,7 @@ conditions should hold up to isomorphism or merely a directed
 transformation. For example, in a 1-category, given two parallel
 morphisms
 
-~~~{.quiver}
+~~~{.quiver .attach-around}
 \[\begin{tikzcd}
 	A & B
 	\arrow["f", shift left, from=1-1, to=1-2]
@@ -109,14 +109,14 @@ pseudofunctor $F$, illustrated in the diagram below.
 	\arrow[""{name=0, anchor=center, inner sep=0}, "{{\phi_i}}", from=2-1, to=1-2]
 	\arrow["{{F(f)}}"', from=2-1, to=2-2]
 	\arrow["{{\phi_j}}"', from=2-2, to=1-2]
-	\arrow[Rightarrow, from=0, to=2-2, shorten <= 0.2em]
+	\arrow["{\small\nu_f}", Rightarrow, from=0, to=2-2, shorten <= 0.2em]
 \end{tikzcd}\]
 ~~~
 
-For each object $i$ in the diagram, $\phi_i : F(i) \to X$ gives a leg of
-the cocone, and for any morphism $f : i \to j$, we have a 2-cell
-isomorphism $\nu_f : \phi_i \cong \phi_j F(f)$ in place of the usual
-commutativity requirement for cocones.
+For each object $i$ in the diagram, the map $\phi_i : F(i) \to X$ gives
+a leg of the cocone, and for any morphism $f : i \to j$, we have an
+invertible 2-cell $\nu_f : \phi_i \cong \phi_j F(f)$ in place of the
+usual commutativity requirement for cocones.
 
 As is often the case in bicategorical definitions, we have the choice of
 whether to consider cocones $F \to \Delta_X$ which commute strongly (so
@@ -125,8 +125,7 @@ that $\nu_f$ is an isomorphism as above), or to take cocones with
 2-cell).  The latter choice yields the notion of a **lax colimit** (or
 oplax, depending on the direction of the 2-cells).  It is known that
 (op-)lax colimits can be expressed as bicolimits by altering the diagram
-category, but in this page, we mainly deal with lax colimits, so we opt
-to define those directly.
+category, but here we give a direct definition.
 
 <!--
 TODO: Also define bicolimits and oplax colimits properly.
@@ -140,26 +139,23 @@ equivalence $\bicat{C}(L,-) \cong [\bicat{I},\bicat{C}]_o(F,\Delta)$,
 where $[\bicat{I},\bicat{C}]_o$ denotes the bicategory of pseudofunctors
 from $\bicat{I}$ to $\bicat{C}$ together with *oplax* transformations
 between them.[^why-oplax] The codomain of this equivalence can be
-translated into Agda as follows.
+translated into Mikan as follows.
 
-[^why-oplax]: The reason that the lax colimit involves oplax
-transformations is that a lax colimit is defined to coincide with a lax
-limit in the opposite bicategory, which ends up reversing the direction
-of cocone 2-cells.
+[^why-oplax]: The reason the definition involves oplax transformations
+is that a lax colimit is defined to coincide with a lax limit in the
+opposite bicategory, which ends up reversing the direction of cocone
+2-cells.
 
 ```agda
   lax-cocones-at : Pseudofunctor C (Cat _ _)
   lax-cocones-at = Hom-from-bi (Pseudoₒ I C) (opᵖ F) P∘ Const-pseudoₒ
 ```
 
 Now, by a bicategorical Yoneda argument, any pseudonatural equivalence
-of the form discussed is determined by its value at $\id : L \to L$,
+of the form above is determined by its value at $\id : L \to L$,
 which is a cocone $F \To \Delta_L$, namely the universal colimiting
-cocone.
-
-Under the Yoneda correspondence, a cocone at $L$ induces a functor
-$\bicat{C}(L,X) \to [\bicat{I},\bicat{C}]_o(F,\Delta_L)$ by
-precomposition.
+cocone. Conversely, any cocone at $L$ induces a functor $\bicat{C}(L,X)
+\to [\bicat{I},\bicat{C}]_o(F,\Delta_L)$ by precomposition.
 
 ```agda
   module _ (L : Ob) (univ-cocone : opᵖ F .lax =>ₒ ConstP L .lax) where
@@ -184,16 +180,17 @@ mostly boil down to automated bicategory reasoning.
         F∘ Flip (Lax.compose _ _) F∘ Const-pseudoₒ.Const₁
         ≅ⁿ postaction (Cat _ _) (hom→cocone₀ X) F∘ compose
       hom→cocone-nat = to-natural-iso ni where
+        open make-natural-iso
         ni : make-natural-iso _ _
-        ni .make-natural-iso.eta f .η g .Γ a         = α← _
-        ni .make-natural-iso.eta f .η g .is-natural  = bicat! C
-        ni .make-natural-iso.eta f .is-natural g h α = ext λ _ → bicat! C
-        ni .make-natural-iso.inv f .η g .Γ a         = α→ _
-        ni .make-natural-iso.inv f .η g .is-natural  = bicat! C
-        ni .make-natural-iso.inv f .is-natural g h α = ext λ _ → bicat! C
-        ni .make-natural-iso.eta∘inv f               = ext λ _ _ → Br.α≅ C .invr
-        ni .make-natural-iso.inv∘eta f               = ext λ _ _ → Br.α≅ C .invl
-        ni .make-natural-iso.natural g h α           = ext λ _ _ → bicat! C
+        ni .eta f .η g .Γ a         = α← _
+        ni .eta f .η g .is-natural  = bicat! C
+        ni .eta f .is-natural g h α = ext λ _ → bicat! C
+        ni .inv f .η g .Γ a         = α→ _
+        ni .inv f .η g .is-natural  = bicat! C
+        ni .inv f .is-natural g h α = ext λ _ → bicat! C
+        ni .eta∘inv f               = ext λ _ _ → Br.α≅ C .invr
+        ni .inv∘eta f               = ext λ _ _ → Br.α≅ C .invl
+        ni .natural g h α           = ext λ _ _ → bicat! C
 
     hom→cocone : Hom-from-bi C L .lax =>ₚ lax-cocones-at .lax
     hom→cocone .lax .σ                = hom→cocone₀
@@ -202,13 +199,12 @@ mostly boil down to automated bicategory reasoning.
     hom→cocone .lax .ν-unitor         = ext λ _ _ → bicat! C
     hom→cocone .naturator-inv f       =
       Cr.iso→invertible Cat[ _ , _ ] (isoⁿ→iso hom→cocone-nat f)
-
 ```
 
 </details>
 
 In other words, to show that $L$ is the lax colimit of $F$, it suffices
-to provide a candidate cocone with apex $L$, and show that
+to provide a candidate cocone with apex $L$, and show that the induced
 `hom→cocone`{.Agda} is a pseudonatural equivalence, which corresponds to
 showing that the provided cocone is universal.
 

src/Cat/Bi/Diagram/Colimit/IndexedCategory.lagda.md

@@ -36,8 +36,7 @@ An especially important case of lax colimits are those of [[indexed
 categories]], i.e., contravariant pseudofunctors from a [[locally
 discrete bicategory]] into $\Cat$.  For an indexed category $F :
 \ca{I}\op \to \Cat$, the lax colimit of $F$ coincides with the
-[[Grothendieck construction]] $\int F$, which is what we show in this
-module.
+[[Grothendieck construction]] $\int F$, which we show in this module.
 
 <!--
 ```agda
@@ -51,7 +50,7 @@ module.
 
   private
     module I      = Precategory I
-    module F      = IndexedCategory F
+    module F      = Indexed-category F
     module F₀ {x} = Cr (F.₀ x)
     module G      = Cr (∫ F.displayed)
     module Cat    = Br (Cat (o ⊔ o') (h ⊔ h'))
@@ -60,21 +59,13 @@ module.
 ```
 -->
 
-```agda
-  univ-cocone : opᵖ F .lax =>ₒ ConstP F.∫ .lax
-```
-
 To construct the universal cocone, we use the canonical inclusion
-functors from the fibre categories of $F$ into $\int F$.
-
-```agda
-  univ-cocone .σ a = F.ιᶠ a
-```
-
-The naturality 2-cells are straightforward to define, and we did so
-already off-screen.
+functors from the fibre categories of $F$ into $\int F$.  The naturality
+2-cells are straightforward to define, and we did so already off-screen.
 
 ```agda
+  univ-cocone : opᵖ F .lax =>ₒ ConstP F.∫ .lax
+  univ-cocone .σ a            = F.ιᶠ a
   univ-cocone .naturator .η f = nat-unidl-to (F.ιᶠ-base-change f)
 ```
 
@@ -133,9 +124,9 @@ which factors the other cocone through the universal one.
 
 Assume that we are given a lax cocone $\alpha : F \To \Delta_X$.  This
 is an oplax transformation with functor components $F(i) \to X$ for each
-$i \in \ca{I}$.  Since an object of $\int F$ bundles an $i \in \ca{I}$
-with some $a \in F(i)$, we can use $\alpha_i$ to map $a$ into $X$,
-giving us the object mapping we need.
+$i : \ca{I}$.  Since an object of $\int F$ bundles an $i : \ca{I}$ with
+some $a : F(i)$, we can use $\alpha_i$ to map $a$ into $X$, giving us
+the object mapping we need.
 
 ```agda
       module α = _=>ₗ_ α
@@ -144,7 +135,7 @@ giving us the object mapping we need.
 ```
 
 For the morphism mapping, we are given $f : i \to j$ in $\ca{I}$,
-together with some $\phi : a \to F(f)(b)$ with $a \in F(i)$ and $b \in
+together with some $\phi : a \to F(f)(b)$ with $a : F(i)$ and $b :
 F(j)$, and we must produce a morphism $\alpha_i(a) \to \alpha_j(b)$.
 Taking $\alpha_i(\phi) : \alpha_i(a) \to \alpha_i(F(f)(b))$ gets us
 almost all of the way.  To complete the definition, we need a morphism
@@ -169,7 +160,7 @@ identities of $\alpha$.
         (α.ν→ f .η Fz ∘ α.σ y .F₁ Ff) ∘ α.ν→ g .η Fy ∘ α.σ x .F₁ Fg          ∎
 ```
 
-Furthermore, assignment of cocones to functors itself extends to a
+Furthermore, this assignment of cocones to functors itself extends to a
 functor from the category of oplax transformations from $F$ to
 $\Delta_X$ to the functor category $[\int F, X]$.
 
@@ -180,9 +171,9 @@ $\Delta_X$ to the functor category $[\int F, X]$.
 
 The morphism mapping of this functor acts on modifications $\gamma :
 \alpha \to \beta$ between cones, and produces a natural transformation
-of induced functors.  This means that at each object $(i, a) \in \int
-F$, we must give a component morphism $\alpha_i(a) \to \beta_i(a)$ in
-$X$.  But unwrapping the definitions, we see that these are just the
+of induced functors.  This means that at each object $(i, a) : \int F$,
+we must give a component morphism $\alpha_i(a) \to \beta_i(a)$ in $X$.
+But unwrapping the definitions, we see that these are just the
 components of $\gamma$.
 
 ```agda

src/Cat/Bi/Duality.lagda.md

@@ -41,6 +41,7 @@ open Cr._≅_
 open _=>_ renaming (op to opⁿ)
 
 module _ (C : Prebicategory o h ℓ) where
+  open make-natural-iso
   open Prebicategory C
   private
     module C  = Br C
@@ -77,18 +78,18 @@ $\bicat{C}$, and vice versa.
 ```agda
   _^op .Pb.unitor-l = to-natural-iso ni where
     ni : make-natural-iso _ _
-    ni .make-natural-iso.eta           = ρ→
-    ni .make-natural-iso.inv           = ρ←
-    ni .make-natural-iso.eta∘inv _     = C.ρ≅ .invl
-    ni .make-natural-iso.inv∘eta _     = C.ρ≅ .invr
-    ni .make-natural-iso.natural _ _ _ = sym $ ρ→nat _
+    ni .eta           = ρ→
+    ni .inv           = ρ←
+    ni .eta∘inv _     = C.ρ≅ .invl
+    ni .inv∘eta _     = C.ρ≅ .invr
+    ni .natural _ _ _ = sym $ ρ→nat _
   _^op .Pb.unitor-r = to-natural-iso ni where
     ni : make-natural-iso _ _
-    ni .make-natural-iso.eta           = λ→
-    ni .make-natural-iso.inv           = λ←
-    ni .make-natural-iso.eta∘inv _     = C.λ≅ .invl
-    ni .make-natural-iso.inv∘eta _     = C.λ≅ .invr
-    ni .make-natural-iso.natural _ _ _ = sym $ λ→nat _
+    ni .eta           = λ→
+    ni .inv           = λ←
+    ni .eta∘inv _     = C.λ≅ .invl
+    ni .inv∘eta _     = C.λ≅ .invr
+    ni .natural _ _ _ = sym $ λ→nat _
 ```
 
 Finally, the associator in $\bicat{C}\op$ is given by the inverse of the
@@ -97,10 +98,10 @@ associator of $\bicat{C}$.
 ```agda
   _^op .Pb.associator = to-natural-iso ni where
     ni : make-natural-iso _ _
-    ni .make-natural-iso.eta _         = α← _
-    ni .make-natural-iso.inv _         = α→ _
-    ni .make-natural-iso.eta∘inv _     = C.α≅ .invr
-    ni .make-natural-iso.inv∘eta _     = C.α≅ .invl
+    ni .eta _     = α← _
+    ni .inv _     = α→ _
+    ni .eta∘inv _ = C.α≅ .invr
+    ni .inv∘eta _ = C.α≅ .invl
 ```
 
 <details>
@@ -111,7 +112,7 @@ expects.
 </summary>
 
 ```agda
-    ni .make-natural-iso.natural _ _ _ =
+    ni .natural _ _ _ =
          CH.car (CH.cdr (ap (C._◀ _) (compose.rlmap _ _)) ∙ compose.rlmap _ _)
       ∙∙ sym (α←nat _ _ _)
       ∙∙ CH.cdr (CH.cdr (ap (_ C.▶_) (compose.lrmap _ _)) ∙ compose.lrmap _ _)
@@ -164,24 +165,24 @@ opposite direction, which we achieve by taking their inverses.
 ```agda
   _^co .Pb.unitor-l = to-natural-iso ni where
     ni : make-natural-iso _ _
-    ni .make-natural-iso.eta           = λ←
-    ni .make-natural-iso.inv           = λ→
-    ni .make-natural-iso.eta∘inv _     = C.λ≅ .invl
-    ni .make-natural-iso.inv∘eta _     = C.λ≅ .invr
-    ni .make-natural-iso.natural _ _ _ = λ←nat _
+    ni .eta           = λ←
+    ni .inv           = λ→
+    ni .eta∘inv _     = C.λ≅ .invl
+    ni .inv∘eta _     = C.λ≅ .invr
+    ni .natural _ _ _ = λ←nat _
   _^co .Pb.unitor-r = to-natural-iso ni where
     ni : make-natural-iso _ _
-    ni .make-natural-iso.eta           = ρ←
-    ni .make-natural-iso.inv           = ρ→
-    ni .make-natural-iso.eta∘inv _     = C.ρ≅ .invl
-    ni .make-natural-iso.inv∘eta _     = C.ρ≅ .invr
-    ni .make-natural-iso.natural _ _ _ = ρ←nat _
+    ni .eta           = ρ←
+    ni .inv           = ρ→
+    ni .eta∘inv _     = C.ρ≅ .invl
+    ni .inv∘eta _     = C.ρ≅ .invr
+    ni .natural _ _ _ = ρ←nat _
   _^co .Pb.associator = to-natural-iso ni where
     ni : make-natural-iso _ _
-    ni .make-natural-iso.eta           = α←
-    ni .make-natural-iso.inv           = α→
-    ni .make-natural-iso.eta∘inv _     = C.α≅ .invl
-    ni .make-natural-iso.inv∘eta _     = C.α≅ .invr
+    ni .eta           = α←
+    ni .inv           = α→
+    ni .eta∘inv _     = C.α≅ .invl
+    ni .inv∘eta _     = C.α≅ .invr
 ```
 
 <details>
@@ -191,7 +192,7 @@ whiskerings.
 </summary>
 
 ```agda
-    ni .make-natural-iso.natural _ _ _ =
+    ni .natural _ _ _ =
          CH.cdr (CH.car (ap (_ C.▶_) (compose.rlmap _ _)) ∙ compose.rlmap _ _)
       ∙∙ α←nat _ _ _
       ∙∙ CH.car (CH.car (ap (C._◀ _) (compose.lrmap _ _)) ∙ compose.lrmap _ _)
@@ -224,8 +225,9 @@ module _ {B : Prebicategory o h ℓ} {C : Prebicategory o' h' ℓ'} where
 -->
 
 As with functors, lax functors have duals going between the opposite
-categories.  All we need to do is apply the compositor in with the
-opposite order of arguments and reorder the hexagon diagram accordingly.
+categories.  The compositor of the opposite functor is given by flipping
+the original compositor, and the hexagon diagram can be reordered
+accordingly.
 
 ```agda
     opˡ : Lax-functor (B ^op) (C ^op)
@@ -242,10 +244,11 @@ opposite order of arguments and reorder the hexagon diagram accordingly.
     opˡ .left-unit  = F.right-unit
 ```
 
-On the other hand, there is no good notion of "conjugate dual" from
+On the other hand, there is no good notion of a "conjugate dual" from
 $\bicat{B}\co$ to $\bicat{C}\co$ for a lax functor: we would need to
 invert the directions of the compositor and unitor, but for a lax
-functor, this is not possible.
+functor, this is not possible.  On the other hand, for pseudofunctors we
+get both flavors of duals.
 
 <!--
 ```agda
@@ -254,20 +257,16 @@ functor, this is not possible.
 ```
 -->
 
-For pseudofunctors, the situation is a bit different.  As with lax
-functors, we get a dual between the opposite bicategories, by the same
-construction as above.
-
 ```agda
     opᵖ : Pseudofunctor (B ^op) (C ^op)
     opᵖ .lax                    = opˡ (F .lax)
     opᵖ .unitor-inv             = F.unitor-inv
     opᵖ .compositor-inv (f , g) = F.compositor-inv (g , f)
 ```
 
-A pseudofunctor $F$ also has a conjugate dual, whose action on objects
-is the same, but whose action on $\hom$-categories is given by the
-opposite of $F$'s morphism mapping.
+The conjugate dual of a pseudofunctor $F$ acts the same as $F$ on
+objects, but its action on $\hom$-categories is given by the opposite of
+$F$'s action.
 
 ```agda
     co : Pseudofunctor (B ^co) (C ^co)