Basic monoidal category theory (#364)

- reverse monoidal categories
- braided, symmetric monoidal categories
- monoidal categories with diagonals
- cartesian monoidal categories are symmetric monoidal with diagonals
- (lax) monoidal functors, braided/symmetric/diagonal monoidal functors,
monoidal natural transformations
- monoidal functors take monoids to monoids, functorially
- a bunch of extra coherence properties for monoidal and braided
monoidal categories
- tensorial strengths, equivalence between left and right strengths in a
braided monoidal category, every Sets-endofunctor is strong

My initial motivation was to understand the precise relationship between
(symmetric) monoidal monads and commutative strong monads, which is why
I'm formalising strengths here, but that page could use more prose.
Edits welcome.

Some proofs are truly nightmarish, and I feel like we're still missing
some important reasoning combinators for isomorphisms but I don't want
to think about it right now.

default.nix

@@ -21,7 +21,7 @@ let
       collection-latex
       xcolor
       preview
-      pgf tikz-cd
+      pgf tikz-cd braids
       mathpazo
       varwidth xkeyval standalone;
   };

src/Cat/Bi/Base.lagda.md

@@ -418,7 +418,7 @@ have components $F_1(f)F_1(g) \To F_1(fg)$ and $\id \To F_1(\id)$.
 ```agda
     compositor
       : ∀ {A B C}
-      → C.compose F∘ Cat⟨ P₁ {B} {C} F∘ Fst , P₁ {A} {B} F∘ Snd ⟩ => P₁ F∘ B.compose
+      → C.compose F∘ (P₁ {B} {C} F× P₁ {A} {B}) => P₁ F∘ B.compose
 
     unitor : ∀ {A} → C.id C.⇒ P₁ .Functor.F₀ (B.id {A = A})
 ```

src/Cat/Functor/Base.lagda.md

@@ -181,7 +181,7 @@ Functor-path {C = C} {D = D} {F = F} {G = G} p0 p1 i .F-∘ f g =
 
 <!--
 ```agda
-module _ {C : Precategory o ℓ} {D : Precategory o₁ ℓ₁} where
+module F-iso {C : Precategory o ℓ} {D : Precategory o₁ ℓ₁} (F : Functor C D) where
   private module _ where
     module C = Cat.Reasoning C
     module D = Cat.Reasoning D
@@ -195,17 +195,17 @@ We have also to make note of the following fact: absolutely all functors
 preserve isomorphisms, and, more generally, preserve invertibility.
 
 ```agda
-  F-map-iso : ∀ {x y} (F : Functor C D) → x C.≅ y → F # x D.≅ F # y
-  F-map-iso F x .to       = F .F₁ (x .to)
-  F-map-iso F x .from     = F .F₁ (x .from)
-  F-map-iso F x .inverses =
+  F-map-iso : ∀ {x y} → x C.≅ y → F # x D.≅ F # y
+  F-map-iso x .to       = F .F₁ (x .to)
+  F-map-iso x .from     = F .F₁ (x .from)
+  F-map-iso x .inverses =
     record { invl = sym (F .F-∘ _ _) ∙ ap (F .F₁) (x .invl) ∙ F .F-id
            ; invr = sym (F .F-∘ _ _) ∙ ap (F .F₁) (x .invr) ∙ F .F-id
            }
     where module x = C._≅_ x
 
-  F-map-invertible : ∀ {x y} (F : Functor C D) {f : C.Hom x y} → C.is-invertible f → D.is-invertible (F .F₁ f)
-  F-map-invertible F inv =
+  F-map-invertible : ∀ {x y} {f : C.Hom x y} → C.is-invertible f → D.is-invertible (F .F₁ f)
+  F-map-invertible inv =
     D.make-invertible (F .F₁ _)
       (sym (F .F-∘ _ _) ·· ap (F .F₁) x.invl ·· F .F-id)
       (sym (F .F-∘ _ _) ·· ap (F .F₁) x.invr ·· F .F-id)
@@ -222,36 +222,38 @@ already coherent enough to ensure that these actions agree:
 ```agda
   F-map-path
     : (ccat : is-category C) (dcat : is-category D)
-    → ∀ (F : Functor C D) {x y} (i : x C.≅ y)
-    → ap# F (Univalent.iso→path ccat i) ≡ Univalent.iso→path dcat (F-map-iso F i)
-  F-map-path ccat dcat F {x} = Univalent.J-iso ccat P pr where
+    → ∀ {x y} (i : x C.≅ y)
+    → ap# F (Univalent.iso→path ccat i) ≡ Univalent.iso→path dcat (F-map-iso i)
+  F-map-path ccat dcat {x} = Univalent.J-iso ccat P pr where
     P : (b : C.Ob) → C.Isomorphism x b → Type _
     P b im = ap# F (Univalent.iso→path ccat im)
-           ≡ Univalent.iso→path dcat (F-map-iso F im)
+           ≡ Univalent.iso→path dcat (F-map-iso im)
 
     pr : P x C.id-iso
     pr =
       ap# F (Univalent.iso→path ccat C.id-iso) ≡⟨ ap (ap# F) (Univalent.iso→path-id ccat) ⟩
       ap# F refl                               ≡˘⟨ Univalent.iso→path-id dcat ⟩
       dcat .to-path D.id-iso                   ≡⟨ ap (dcat .to-path) (ext (sym (F .F-id))) ⟩
-      dcat .to-path (F-map-iso F C.id-iso)     ∎
+      dcat .to-path (F-map-iso C.id-iso)     ∎
 ```
 
 <!--
 ```agda
   ap-F₀-to-iso
-    : ∀ (F : Functor C D) {y z}
-    → (p : y ≡ z) → path→iso (ap# F p) ≡ F-map-iso F (path→iso p)
-  ap-F₀-to-iso F {y} =
-    J (λ _ p → path→iso (ap# F p) ≡ F-map-iso F (path→iso p))
+    : ∀ {y z}
+    → (p : y ≡ z) → path→iso (ap# F p) ≡ F-map-iso (path→iso p)
+  ap-F₀-to-iso {y} =
+    J (λ _ p → path→iso (ap# F p) ≡ F-map-iso (path→iso p))
       (D.≅-pathp (λ _ → F .F₀ y) (λ _ → F .F₀ y)
         (Regularity.fast! (sym (F .F-id))))
 
   ap-F₀-iso
-    : ∀ (cc : is-category C) (F : Functor C D) {y z : C.Ob}
-    → (p : y C.≅ z) → path→iso (ap# F (cc .to-path p)) ≡ F-map-iso F p
-  ap-F₀-iso cc F p = ap-F₀-to-iso F (cc .to-path p)
-                   ∙ ap (F-map-iso F) (Univalent.iso→path→iso cc p)
+    : ∀ (cc : is-category C) {y z : C.Ob}
+    → (p : y C.≅ z) → path→iso (ap# F (cc .to-path p)) ≡ F-map-iso p
+  ap-F₀-iso cc p = ap-F₀-to-iso (cc .to-path p)
+                 ∙ ap F-map-iso (Univalent.iso→path→iso cc p)
+
+open F-iso public
 ```
 -->
 

src/Cat/Functor/Equivalence.lagda.md

@@ -462,7 +462,7 @@ indeed the same path:
     abstract
       square : ap# F x≡y ≡ Fx≡Fy
       square =
-        ap# F x≡y                         ≡⟨ F-map-path ccat dcat F x≅y ⟩
+        ap# F x≡y                         ≡⟨ F-map-path F ccat dcat x≅y ⟩
         dcat .to-path ⌜ F-map-iso F x≅y ⌝ ≡⟨ ap! (equiv→counit (is-ff→F-map-iso-is-equiv {F = F} ff) _)  ⟩
         dcat .to-path Fx≅Fy               ∎
 

src/Cat/Functor/Hom/Representable.lagda.md

@@ -118,7 +118,7 @@ Representation-is-prop {F = F} c-cat x y = path where
       (Nat-pathp _ _ λ a → Hom-pathp-reflr (Sets _)
         {A = F .F₀ a} {q = λ i → el! (C.Hom a (objs i))}
         (funext λ x →
-           ap (λ e → e .Sets.to) (ap-F₀-iso c-cat (Hom-from C a) _) $ₚ _
+           ap (λ e → e .Sets.to) (ap-F₀-iso (Hom-from C a) c-cat _) $ₚ _
         ·· sym (Y.rep.to .is-natural _ _ _) $ₚ _
         ·· ap Y.Rep.from (sym (X.rep.from .is-natural _ _ _ $ₚ _)
                        ·· ap X.Rep.to (C.idl _)
@@ -305,7 +305,7 @@ Corepresentation-is-prop {F = F} c-cat X Y = path where
        (Nat-pathp _ _ λ a → Hom-pathp-reflr (Sets _)
          {A = F .F₀ a} {q = λ i → el! (C.Hom (objs i) a)}
          (funext λ x →
-           ap (λ e → e .Sets.to) (ap-F₀-iso (opposite-is-category c-cat) (Hom-into C a) _) $ₚ _
+           ap (λ e → e .Sets.to) (ap-F₀-iso (Hom-into C a) (opposite-is-category c-cat) _) $ₚ _
            ·· sym (corep.to Y .is-natural _ _ _ $ₚ _)
            ·· ap (Corep.from Y) (sym (corep.from X .is-natural _ _ _ $ₚ _)
                                  ·· ap (Corep.to X) (C.idr _)

src/Cat/Functor/Naturality.lagda.md

@@ -11,7 +11,7 @@ import Cat.Reasoning
 module Cat.Functor.Naturality where
 ```
 
-# Working with natural transformations
+# Working with natural transformations {defines="natural-isomorphism"}
 
 Working with natural transformations can often be more cumbersome than
 working directly with the underlying families of morphisms; moreover, we
@@ -33,7 +33,8 @@ module _ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} where
 -->
 
 We'll refer to the natural-transformation versions of predicates on
-morphisms by a superscript `ⁿ`:
+morphisms by a superscript `ⁿ`. A **natural isomorphism** is simply an
+isomorphism in a functor category.
 
 ```agda
   Inversesⁿ : {F G : Functor C D} → F => G → G => F → Type _
@@ -200,6 +201,15 @@ to an invertible natural transformation, resp. natural isomorphism.
     ate : _ => _
     ate .η x = D.is-invertible.inv (i x)
     ate .is-natural = inverse-is-natural eta _ (λ x → D.is-invertible.invl (i x)) (λ x → D.is-invertible.invr (i x))
+
+  push-eqⁿ : ∀ {F G} (α : F ≅ⁿ G) {a b} {f g : C.Hom a b} → F .F₁ f ≡ F .F₁ g → G .F₁ f ≡ G .F₁ g
+  push-eqⁿ {F = F} {G = G} α {f = f} {g} p =
+    G .F₁ f                                           ≡⟨ D.insertl (α .Isoⁿ.invl ηₚ _) ⟩
+    α .Isoⁿ.to .η _ D.∘ α .Isoⁿ.from .η _ D.∘ G .F₁ f ≡⟨ D.refl⟩∘⟨ α .Isoⁿ.from .is-natural _ _ _ ⟩
+    α .Isoⁿ.to .η _ D.∘ F .F₁ f D.∘ α .Isoⁿ.from .η _ ≡⟨ D.refl⟩∘⟨ p D.⟩∘⟨refl ⟩
+    α .Isoⁿ.to .η _ D.∘ F .F₁ g D.∘ α .Isoⁿ.from .η _ ≡˘⟨ D.refl⟩∘⟨ α .Isoⁿ.from .is-natural _ _ _ ⟩
+    α .Isoⁿ.to .η _ D.∘ α .Isoⁿ.from .η _ D.∘ G .F₁ g ≡⟨ D.cancell (α .Isoⁿ.invl ηₚ _) ⟩
+    G .F₁ g                                           ∎
 ```
 -->
 

src/Cat/Functor/Properties.lagda.md

@@ -207,7 +207,7 @@ module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
 
   is-ff→F-map-iso-is-equiv
     : {F : Functor C D} → is-fully-faithful F
-    → ∀ {X Y} → is-equiv (F-map-iso {x = X} {Y} F)
+    → ∀ {X Y} → is-equiv (F-map-iso F {x = X} {Y})
   is-ff→F-map-iso-is-equiv {F = F} ff = is-iso→is-equiv isom where
     isom : is-iso _
     isom .is-iso.inv    = is-ff→essentially-injective {F = F} ff

src/Cat/Functor/Reasoning.lagda.md

@@ -4,6 +4,7 @@ open import 1Lab.Path
 
 open import Cat.Base
 
+import Cat.Functor.Base
 import Cat.Reasoning
 ```
 -->
@@ -19,13 +20,14 @@ private
   module 𝒞 = Cat.Reasoning 𝒞
   module 𝒟 = Cat.Reasoning 𝒟
 open Functor F public
+open Cat.Functor.Base.F-iso F public
 ```
 
 <!--
 ```agda
 private variable
   A B C : 𝒞.Ob
-  a b c d : 𝒞.Hom A B
+  a a' b b' c c' d : 𝒞.Hom A B
   X Y Z : 𝒟.Ob
   f g h i : 𝒟.Hom X Y
 ```
@@ -75,6 +77,13 @@ module _ (ab≡c : a 𝒞.∘ b ≡ c) where
   pullr : (f 𝒟.∘ F₁ a) 𝒟.∘ F₁ b ≡ f 𝒟.∘ F₁ c
   pullr = 𝒟.pullr collapse
 
+module _ (abc≡d : a 𝒞.∘ b 𝒞.∘ c ≡ d) where
+  collapse3 : F₁ a 𝒟.∘ F₁ b 𝒟.∘ F₁ c ≡ F₁ d
+  collapse3 = ap (F₁ a 𝒟.∘_) (sym (F-∘ b c)) ∙ collapse abc≡d
+
+  pulll3 : F₁ a 𝒟.∘ (F₁ b 𝒟.∘ (F₁ c 𝒟.∘ f)) ≡ F₁ d 𝒟.∘ f
+  pulll3 = 𝒟.pulll3 collapse3
+
 module _ (c≡ab : c ≡ a 𝒞.∘ b) where
   expand : F₁ c ≡ F₁ a 𝒟.∘ F₁ b
   expand = sym (collapse (sym c≡ab))
@@ -99,6 +108,13 @@ module _ (p : a 𝒞.∘ c ≡ b 𝒞.∘ d) where
     f 𝒟.∘ F₁ a 𝒟.∘ F₁ c 𝒟.∘ g ≡ f 𝒟.∘ F₁ b 𝒟.∘ F₁ d 𝒟.∘ g
   extend-inner = 𝒟.extend-inner weave
 
+module _ (p : a 𝒞.∘ b 𝒞.∘ c ≡ a' 𝒞.∘ b' 𝒞.∘ c') where
+  weave3 : F₁ a 𝒟.∘ F₁ b 𝒟.∘ F₁ c ≡ F₁ a' 𝒟.∘ F₁ b' 𝒟.∘ F₁ c'
+  weave3 = ap (_ 𝒟.∘_) (sym (F-∘ b c)) ·· weave p ·· ap (_ 𝒟.∘_) (F-∘ b' c')
+
+  extendl3 : F₁ a 𝒟.∘ (F₁ b 𝒟.∘ (F₁ c 𝒟.∘ f)) ≡ F₁ a' 𝒟.∘ (F₁ b' 𝒟.∘ (F₁ c' 𝒟.∘ f))
+  extendl3 = 𝒟.extendl3 weave3
+
 module _ (p : F₁ a 𝒟.∘ F₁ c ≡ F₁ b 𝒟.∘ F₁ d) where
   swap : F₁ (a 𝒞.∘ c) ≡ F₁ (b 𝒞.∘ d)
   swap = F-∘ a c ·· p ·· sym (F-∘  b d)

src/Cat/Functor/Reasoning/FullyFaithful.lagda.md

@@ -1,7 +1,6 @@
 <!--
 ```agda
 open import Cat.Functor.Properties
-open import Cat.Functor.Base
 open import Cat.Prelude hiding (injective)
 
 import Cat.Functor.Reasoning as Fr
@@ -43,10 +42,10 @@ module _ {a} {b} where
   open Equiv (F₁ {a} {b} , ff) public
 
 iso-equiv : ∀ {a b} → (a C.≅ b) ≃ (F₀ a D.≅ F₀ b)
-iso-equiv {a} {b} = (F-map-iso {x = a} {b} F , is-ff→F-map-iso-is-equiv {F = F} ff)
+iso-equiv {a} {b} = (F-map-iso {x = a} {b} , is-ff→F-map-iso-is-equiv {F = F} ff)
 
 module iso {a} {b} =
-  Equiv (F-map-iso {x = a} {b} F , is-ff→F-map-iso-is-equiv {F = F} ff)
+  Equiv (F-map-iso {x = a} {b} , is-ff→F-map-iso-is-equiv {F = F} ff)
 ```
 -->
 

src/Cat/Instances/Comma/Univalent.lagda.md

@@ -94,8 +94,8 @@ an identification $o \equiv o'$.
       lemma' : PathP (λ i → X.Hom (F.₀ (objs i .x)) (G.₀ (objs i .y)))
                 (ob .map) (ob' .map)
       lemma' = transport
-        (λ i → PathP (λ j → X.Hom (F-map-path yuniv xuniv F x-is-x (~ i) j)
-                                  (F-map-path zuniv xuniv G y-is-y (~ i) j))
+        (λ i → PathP (λ j → X.Hom (F-map-path F yuniv xuniv x-is-x (~ i) j)
+                                  (F-map-path G zuniv xuniv y-is-y (~ i) j))
                     (ob .map) (ob' .map)) $
         Univalent.Hom-pathp-iso xuniv $
           X.pulll   (sym (isom.to .sq)) ∙