Merge pull request #492 from jacquescomeaux/monoidal-refactor

Clean up monoidal functor properties

Author: JacquesCarette

src/Categories/Category/Instance/Properties/Cats.agda

@@ -16,11 +16,12 @@ open import Categories.Category.Monoidal.Instance.Cats
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Construction.Constant using (constNat)
+import Categories.Morphism.Properties as MP
 import Categories.Morphism.Reasoning as MR
 open import Categories.NaturalTransformation
   using (NaturalTransformation; _∘ˡ_) renaming (id to idNT)
 open import Categories.NaturalTransformation.NaturalIsomorphism
-  using (NaturalIsomorphism; _≃_; module LeftRightId)
+  using (NaturalIsomorphism; _≃_)
 open import Categories.Object.Terminal using (Terminal)
 
 -- It's easier to define exponentials with respect to the *canonical*
@@ -55,14 +56,14 @@ module CanonicallyCartesianClosed {l} where
       ; commute     = λ _ → ⟺ (MR.id-comm B ○ ∘-resp-≈ʳ B commute)
       ; sym-commute = λ _ → MR.id-comm B ○ ∘-resp-≈ʳ B commute
       }
-    ; iso = iso-id-id
+    ; iso = λ _ → id-iso
     }
     where
       open Functor G renaming (F₀ to G₀; F₁ to G₁)
       open Category hiding (_∘_)
       open Category B using (_∘_)
       open HomReasoning B
-      open LeftRightId G
+      open MP B
 
       commute : ∀ {a₁ a₂ b₁ b₂} {f₁ : C [ a₁ , b₁ ]} {f₂ : A [ a₂ , b₂ ]} →
                 B [ (G₁ (f₁ , id A) ∘ G₁ (id C , f₂)) ≈ G₁ (f₁ , f₂) ]
@@ -105,7 +106,6 @@ module CanonicallyCartesianClosed {l} where
       open Category B using (_∘_)
       open HomReasoning B
       open NaturalTransformation
-      open LeftRightId H
 
       commute₁ : ∀ {a b c} (f : A [ a , b ]) →
                  B [ (η (H₁ (id C)) b ∘ (H₀ c $₁ f)) ≈ H₀ c $₁ f ]

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

@@ -1,7 +1,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category using (Category; module Commutation)
-open import Categories.Category.Monoidal
+open import Categories.Category.Monoidal.Core
 open import Categories.Category.Monoidal.Braided using (Braided)
 
 module Categories.Category.Monoidal.Braided.Properties
@@ -15,9 +15,9 @@ open import Categories.Category.Monoidal.Reasoning M
 import Categories.Category.Monoidal.Utilities M as MonoidalUtilities
 open import Categories.Functor using (Functor)
 open import Categories.Morphism.Reasoning C hiding (push-eq)
-open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper; module ≃)
 open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
-  using (push-eq)
+  using (push-eq; flip-bifunctor-NI)
 
 open Category C
 open Commutation C
@@ -136,18 +136,29 @@ braiding-coherence-inv = to-≈ braiding-coherence-iso
 
 inv-Braided : Braided M
 inv-Braided = record
-  { braiding = niHelper (record
-    { η       = λ _ → σ⇐
-    ; η⁻¹     = λ _ → σ⇒
-    ; commute = λ{ (f , g) → braiding.⇐.commute (g , f) }
-    ; iso     = λ{ (X , Y) → record
-      { isoˡ = braiding.iso.isoʳ (Y , X)
-      ; isoʳ = braiding.iso.isoˡ (Y , X) } }
-    })
+  { braiding = ≃.sym (flip-bifunctor-NI braiding)
   ; hexagon₁ = hexagon₂-inv
   ; hexagon₂ = hexagon₁-inv
   }
 
+-- The opposite monoidal category is braided.
+
+braided-Op : Braided monoidal-Op
+braided-Op = record
+    { braiding = braiding.op′
+    ; hexagon₁ = hexagon₁-inv
+    ; hexagon₂ = hexagon₂-inv
+    }
+
+-- The inverse of the braiding is also a braiding on the opposite monoidal category.
+
+inv-braided-Op : Braided monoidal-Op
+inv-braided-Op = record
+    { braiding = ≃.sym (flip-bifunctor-NI braiding.op′)
+    ; hexagon₁ = hexagon₂
+    ; hexagon₂ = hexagon₁
+    }
+
 -- A variant of the above coherence law for the inverse of the braiding.
 
 inv-braiding-coherence : [ unit ⊗₀ X ⇒ X ]⟨

src/Categories/Category/Monoidal/Bundle.agda

@@ -7,44 +7,52 @@ open import Level
 
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Monoidal.Core using (Monoidal)
+open import Categories.Category.Monoidal.Properties using (monoidal-Op)
 open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Category.Monoidal.Braided.Properties using (braided-Op)
 open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Categories.Category.Monoidal.Symmetric.Properties using (symmetric-Op)
 
 record MonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
   field
     U        : Category o ℓ e
     monoidal : Monoidal U
 
-  open Category U public
+  open Category U hiding (op) public
   open Monoidal monoidal public
 
+  op : MonoidalCategory o ℓ e
+  op = record { monoidal = monoidal-Op monoidal }
+
 record BraidedMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
   field
     U         : Category o ℓ e
     monoidal  : Monoidal U
     braided   : Braided monoidal
 
   monoidalCategory : MonoidalCategory o ℓ e
-  monoidalCategory = record { U = U ; monoidal = monoidal }
+  monoidalCategory = record { monoidal = monoidal }
 
-  open Category U public
+  open Category U hiding (op) public
   open Braided braided public
 
+  op : BraidedMonoidalCategory o ℓ e
+  op = record { braided = braided-Op braided }
+
 record SymmetricMonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
   field
     U         : Category o ℓ e
     monoidal  : Monoidal U
     symmetric : Symmetric monoidal
 
-  open Category U public
+  open Category U hiding (op) public
   open Symmetric symmetric public
 
   braidedMonoidalCategory : BraidedMonoidalCategory o ℓ e
-  braidedMonoidalCategory = record
-    { U        = U
-    ; monoidal = monoidal
-    ; braided  = braided
-    }
+  braidedMonoidalCategory = record { braided = braided }
 
   open BraidedMonoidalCategory braidedMonoidalCategory public
     using (monoidalCategory)
+
+  op : SymmetricMonoidalCategory o ℓ e
+  op = record { symmetric = symmetric-Op symmetric }

src/Categories/Category/Monoidal/Properties.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 open import Categories.Category
-import Categories.Category.Monoidal as M
+import Categories.Category.Monoidal.Core as M
 
 -- Properties of Monoidal Categories
 

src/Categories/Category/Monoidal/Reasoning.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category using (Category)
-open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Core using (Monoidal)
 
 module Categories.Category.Monoidal.Reasoning {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where
 

src/Categories/Category/Monoidal/Symmetric/Properties.agda

@@ -1,16 +1,17 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Categories.Category using (Category)
-open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Core using (Monoidal)
 open import Categories.Category.Monoidal.Symmetric using (Symmetric)
 
 module Categories.Category.Monoidal.Symmetric.Properties
   {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (SM : Symmetric M) where
 
-open import Data.Product using (_,_)
-
 import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
+
+open import Categories.Category.Monoidal.Properties M using (monoidal-Op)
 open import Categories.Morphism.Reasoning C
+open import Data.Product using (_,_)
 
 open Category C
 open HomReasoning
@@ -27,3 +28,13 @@ braiding-selfInverse = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _)
 
 inv-commutative : ∀ {X Y} → braiding.⇐.η (X , Y) ∘ braiding.⇐.η (Y , X) ≈ id
 inv-commutative = ∘-resp-≈ braiding-selfInverse braiding-selfInverse ○ commutative
+
+-- The opposite monoidal category is symmetric
+
+open BraidedProperties braided using (braided-Op)
+
+symmetric-Op : Symmetric monoidal-Op
+symmetric-Op = record
+    { braided = braided-Op
+    ; commutative = inv-commutative
+    }

src/Categories/Diagram/End/Parameterized.agda

@@ -16,9 +16,10 @@ open import Categories.Functor hiding (id)
 open import Categories.Functor.Bifunctor
 open import Categories.Functor.Bifunctor.Properties
 open import Categories.Functor.Limits
-open import Categories.NaturalTransformation renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
+open import Categories.NaturalTransformation renaming (id to idN)
 open import Categories.NaturalTransformation.Dinatural hiding (_≃_)
 open import Categories.NaturalTransformation.NaturalIsomorphism renaming (_≃_ to _≃ⁱ_)
+open import Categories.NaturalTransformation.Properties using (flip-bifunctor-NT)
 open import Categories.NaturalTransformation.Equivalence
 
 import Categories.Category.Construction.Wedges as Wedges
@@ -42,7 +43,7 @@ F ♯ = curry.₀ F.flip
 
 end-η♯ : {F G : Functor (P ×ᶜ (Category.op C ×ᶜ C)) D} (η : NaturalTransformation F G)
          ⦃ ef : ∫ (F ♯) ⦄ ⦃ eg : ∫ (G ♯) ⦄ → NaturalTransformation (∫.E ef) (∫.E eg)
-end-η♯ η ⦃ ef ⦄ ⦃ eg ⦄ = end-η (curry.₁ (η ▹ⁿ Swap))
+end-η♯ η ⦃ ef ⦄ ⦃ eg ⦄ = end-η (curry.₁ (flip-bifunctor-NT η))
 
 module _ (F : Functor (P ×ᶜ ((Category.op C) ×ᶜ C)) D) {ω : ∀ X → ∫ (appˡ F X)} where
   private

src/Categories/Functor/Bifunctor.agda

@@ -29,7 +29,13 @@ module Bifunctor (H : Bifunctor C D E) where
   reduce-× F G = H ∘F (F ⁂ G)
 
   flip : Bifunctor D C E
-  flip = H ∘F Swap
+  flip = record
+      { F₀ = λ (X , Y) → F₀ (Y , X)
+      ; F₁ = λ (f , g) → F₁ (g , f)
+      ; identity = λ { {A , B} → identity {B , A} }
+      ; homomorphism = λ { {f = (f , f′)} {g , g′} → homomorphism {f = (f′ , f)} {g′ , g} }
+      ; F-resp-≈ = λ (≈f , ≈g) → F-resp-≈ (≈g , ≈f) 
+      }
 
   appˡ : Category.Obj C → Functor D E
   appˡ c = H ∘F constˡ c
@@ -70,5 +76,5 @@ open Bifunctor public using (appˡ; appʳ) renaming (flip to flip-bifunctor)
 overlap-× : ∀ (H : Bifunctor C D E) (F : Functor A C) (G : Functor A D) → Functor A E
 overlap-× H = Bifunctor.overlap-× H
 
-reduce-× : ∀ (H : Bifunctor C D E) (F : Functor A C) (G : Functor B D) -> Bifunctor A B E
+reduce-× : ∀ (H : Bifunctor C D E) (F : Functor A C) (G : Functor B D) → Bifunctor A B E
 reduce-× H = Bifunctor.reduce-× H

src/Categories/Functor/Monoidal.agda

@@ -10,9 +10,12 @@ open import Categories.Category.Product
 open import Categories.Category.Monoidal
 
 open import Categories.Functor hiding (id)
+open import Categories.Functor.Properties using ([_]-resp-≅)
 open import Categories.NaturalTransformation hiding (id)
 open import Categories.NaturalTransformation.NaturalIsomorphism
 
+import Categories.Category.Construction.Core as Core
+import Categories.Category.Monoidal.Utilities as ⊗-Utilities
 import Categories.Morphism as Mor
 
 private
@@ -72,6 +75,11 @@ module _  (C : MonoidalCategory o ℓ e) (D : MonoidalCategory o′ ℓ′ e′)
     open Functor F public
     open IsMonoidalFunctor isMonoidal public
 
+module _  (C : MonoidalCategory o ℓ e) (D : MonoidalCategory o′ ℓ′ e′) where
+  private
+    module C = MonoidalCategory C
+    module D = MonoidalCategory D
+    open Mor D.U
 
   -- strong monoidal functor
   record IsStrongMonoidalFunctor (F : Functor C.U D.U) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
@@ -113,15 +121,61 @@ module _  (C : MonoidalCategory o ℓ e) (D : MonoidalCategory o′ ℓ′ e′)
                       ≈ unitorʳ.from
                       ⟩
 
-    isMonoidal : IsMonoidalFunctor F
-    isMonoidal = record
+    isLaxMonoidal : IsMonoidalFunctor C D F
+    isLaxMonoidal = record
       { ε             = ε.from
       ; ⊗-homo        = ⊗-homo.F⇒G
       ; associativity = associativity
       ; unitaryˡ      = unitaryˡ
       ; unitaryʳ      = unitaryʳ
       }
 
+    private
+
+      module F = Functor F
+
+      φ : {X Y : C.Obj} → F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y)
+      φ = ⊗-homo.FX≅GX
+
+      Fα : {X Y Z : C.Obj} → F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z))
+      Fα = [ F ]-resp-≅ C.associator
+
+      Fλ : {X : C.Obj} → F₀ (C.unit C.⊗₀ X) ≅ F₀ X
+      Fλ = [ F ]-resp-≅ C.unitorˡ
+
+      Fρ : {X : C.Obj} → F₀ (X C.⊗₀ C.unit) ≅ F₀ X
+      Fρ = [ F ]-resp-≅ C.unitorʳ
+
+      α : {A B C : Obj} → (A ⊗₀ B) ⊗₀ C ≅ A ⊗₀ (B ⊗₀ C)
+      α = D.associator
+
+      λ- : {A : Obj} → unit ⊗₀ A ≅ A
+      λ- = D.unitorˡ
+
+      ρ : {A : Obj} → A ⊗₀ unit ≅ A
+      ρ = D.unitorʳ
+
+    open ⊗-Utilities monoidal using (_⊗ᵢ_)
+    open Core.Shorthands U using (⌞_⌟; to-≈; _∘ᵢ_; idᵢ; _≈ᵢ_)
+
+    associativityᵢ : {X Y Z : C.Obj} → Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α
+    associativityᵢ = ⌞ associativity ⌟
+
+    unitaryˡᵢ : {X : C.Obj} → Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ-
+    unitaryˡᵢ = ⌞ unitaryˡ ⌟
+
+    unitaryʳᵢ : {X : C.Obj} → Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ
+    unitaryʳᵢ = ⌞ unitaryʳ ⌟
+
+    isOplaxMonoidal : IsMonoidalFunctor C.op D.op F.op
+    isOplaxMonoidal = record
+      { ε             = ε.to
+      ; ⊗-homo        = ⊗-homo.⇐.op
+      ; associativity = to-≈ associativityᵢ
+      ; unitaryˡ      = to-≈ unitaryˡᵢ
+      ; unitaryʳ      = to-≈ unitaryʳᵢ
+      }
+
   record StrongMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
     field
       F : Functor C.U D.U
@@ -130,5 +184,5 @@ module _  (C : MonoidalCategory o ℓ e) (D : MonoidalCategory o′ ℓ′ e′)
     open Functor F public
     open IsStrongMonoidalFunctor isStrongMonoidal public
 
-    monoidalFunctor : MonoidalFunctor
-    monoidalFunctor = record { F = F ; isMonoidal = isMonoidal }
+    monoidalFunctor : MonoidalFunctor C D
+    monoidalFunctor = record { F = F ; isMonoidal = isLaxMonoidal }

src/Categories/Functor/Monoidal/Braided.agda

@@ -88,7 +88,7 @@ module Strong where
 
     isLaxBraidedMonoidal : Lax.IsBraidedMonoidalFunctor F
     isLaxBraidedMonoidal = record
-      { isMonoidal      = isMonoidal
+      { isMonoidal      = isLaxMonoidal
       ; braiding-compat = braiding-compat
       }