Split monoidal functor properties into multiple files

Author: jacquescomeaux

src/Categories/Functor/Monoidal/Braided/Properties.agda

@@ -0,0 +1,133 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Functor.Monoidal.Braided.Properties where
+
+open import Categories.Functor.Monoidal.Braided using (module Lax; module Strong)
+import Categories.Category.Monoidal.Utilities as ⊗-Util
+import Categories.Category.Monoidal.Braided.Properties as B-Properties
+
+open import Level
+open import Data.Product using (_,_)
+open import Categories.Functor.Monoidal.Properties using (idF-IsStrongMonoidal; ∘-IsMonoidal; ∘-IsStrongMonoidal)
+open import Categories.Category.Monoidal.Bundle using (BraidedMonoidalCategory)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Properties using ([_]-resp-square)
+import Categories.Morphism.Reasoning as MR
+
+private
+  variable
+    o o′ o″ ℓ ℓ′ ℓ″ e e′ e″ : Level
+
+private
+
+  module WithShorthands (C : BraidedMonoidalCategory o ℓ e) where
+    open BraidedMonoidalCategory C public
+    open B-Properties braided using (module Shorthands)
+    open Shorthands public
+
+  module _
+    {C : BraidedMonoidalCategory o ℓ e}
+    {D : BraidedMonoidalCategory o′ ℓ′ e′}
+    (let module C = BraidedMonoidalCategory C)
+    (let module D = BraidedMonoidalCategory D)
+    {F : Functor C.U D.U}
+    where
+
+    module LaxShorthands (F-IsMonoidal : Lax.IsBraidedMonoidalFunctor C D F) where
+      open Functor F public
+      open Lax.IsBraidedMonoidalFunctor F-IsMonoidal public
+      open BraidedMonoidalCategory D
+      φ : {X Y : C.Obj} → F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y)
+      φ {X} {Y} = ⊗-homo.η (X , Y)
+
+    module StrongShorthands (F-IsStrongMonoidal : Strong.IsBraidedMonoidalFunctor C D F) where
+      open Functor F public
+      open Strong.IsBraidedMonoidalFunctor F-IsStrongMonoidal public
+      open BraidedMonoidalCategory D
+      φ⇒ : {X Y : C.Obj} → F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y)
+      φ⇒ {X} {Y} = ⊗-homo.⇒.η (X , Y)
+      φ⇐ : {X Y : C.Obj} → F₀ (X C.⊗₀ Y) ⇒ F₀ X ⊗₀ F₀ Y
+      φ⇐ {X} {Y} = ⊗-homo.⇐.η (X , Y)
+
+-- The identity functor is braided monoidal
+
+module _ (C : BraidedMonoidalCategory o ℓ e) where
+
+  idF-IsStrongBraidedMonoidal : Strong.IsBraidedMonoidalFunctor C C idF
+  idF-IsStrongBraidedMonoidal = record
+    { isStrongMonoidal = idF-IsStrongMonoidal monoidalCategory
+    ; braiding-compat  = MR.id-comm U
+    }
+    where open BraidedMonoidalCategory C
+
+  idF-IsBraidedMonoidal : Lax.IsBraidedMonoidalFunctor C C idF
+  idF-IsBraidedMonoidal =
+    Strong.IsBraidedMonoidalFunctor.isLaxBraidedMonoidal idF-IsStrongBraidedMonoidal
+
+  idF-StrongBraidedMonoidal : Strong.BraidedMonoidalFunctor C C
+  idF-StrongBraidedMonoidal = record { isBraidedMonoidal = idF-IsStrongBraidedMonoidal }
+
+  idF-BraidedMonoidal : Lax.BraidedMonoidalFunctor C C
+  idF-BraidedMonoidal = record { isBraidedMonoidal = idF-IsBraidedMonoidal }
+
+-- Functor composition preserves braided monoidality
+
+module _ {A : BraidedMonoidalCategory o ℓ e}
+         {B : BraidedMonoidalCategory o′ ℓ′ e′}
+         {C : BraidedMonoidalCategory o″ ℓ″ e″} where
+
+  private
+    module A = WithShorthands A
+    module B = WithShorthands B
+    module C = WithShorthands C
+
+  ∘-IsBraidedMonoidal : ∀ {G : Functor B.U C.U} {F : Functor A.U B.U} →
+                        Lax.IsBraidedMonoidalFunctor B C G →
+                        Lax.IsBraidedMonoidalFunctor A B F →
+                        Lax.IsBraidedMonoidalFunctor A C (G ∘F F)
+  ∘-IsBraidedMonoidal {G} {F} GB FB = record
+    { isMonoidal      = ∘-IsMonoidal _ _ _ G.isMonoidal F.isMonoidal
+    ; braiding-compat = B-compat
+    }
+    where
+      open C
+      open HomReasoning
+      open MR C.U
+      module F = LaxShorthands FB
+      module G = LaxShorthands GB
+      B-compat : {X Y : A.Obj} → G.₁ (F.₁ (A.σ⇒ {X} {Y})) ∘ G.₁ F.φ ∘ G.φ ≈ (G.₁ F.φ ∘ G.φ) ∘ σ⇒
+      B-compat = begin
+        G.₁ (F.₁ A.σ⇒) ∘ G.₁ F.φ ∘ G.φ  ≈⟨ extendʳ ([ G ]-resp-square F.braiding-compat) ⟩
+        G.₁ F.φ ∘ G.₁ B.σ⇒ ∘ G.φ        ≈⟨ pushʳ G.braiding-compat ⟩
+        (G.₁ F.φ ∘ G.φ) ∘ σ⇒            ∎
+
+  ∘-IsStrongBraidedMonoidal : ∀ {G : Functor B.U C.U} {F : Functor A.U B.U} →
+                              Strong.IsBraidedMonoidalFunctor B C G →
+                              Strong.IsBraidedMonoidalFunctor A B F →
+                              Strong.IsBraidedMonoidalFunctor A C (G ∘F F)
+  ∘-IsStrongBraidedMonoidal {G} {F} GB FB = record
+    { isStrongMonoidal =
+      ∘-IsStrongMonoidal _ _ _ (isStrongMonoidal GB) (isStrongMonoidal FB)
+    ; braiding-compat =
+      Lax.IsBraidedMonoidalFunctor.braiding-compat
+        (∘-IsBraidedMonoidal (isLaxBraidedMonoidal GB) (isLaxBraidedMonoidal FB))
+    }
+    where open Strong.IsBraidedMonoidalFunctor
+
+  ∘-BraidedMonoidal : Lax.BraidedMonoidalFunctor B C →
+                      Lax.BraidedMonoidalFunctor A B →
+                      Lax.BraidedMonoidalFunctor A C
+  ∘-BraidedMonoidal G F = record
+    { isBraidedMonoidal =
+      ∘-IsBraidedMonoidal (isBraidedMonoidal G) (isBraidedMonoidal F)
+    }
+    where open Lax.BraidedMonoidalFunctor hiding (F)
+
+  ∘-StrongBraidedMonoidal : Strong.BraidedMonoidalFunctor B C →
+                            Strong.BraidedMonoidalFunctor A B →
+                            Strong.BraidedMonoidalFunctor A C
+  ∘-StrongBraidedMonoidal G F = record
+    { isBraidedMonoidal =
+      ∘-IsStrongBraidedMonoidal (isBraidedMonoidal G) (isBraidedMonoidal F)
+    }
+    where open Strong.BraidedMonoidalFunctor hiding (F)