1 files changed, 59 insertions, 0 deletions
diff --git a/Functor/Monoidal/Braided/Strong/Properties.agda b/Functor/Monoidal/Braided/Strong/Properties.agda
new file mode 100644
index 0000000..66dc4c0
--- /dev/null
+++ b/Functor/Monoidal/Braided/Strong/Properties.agda
@@ -0,0 +1,59 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+open import Categories.Category.Monoidal using (BraidedMonoidalCategory)
+open import Categories.Functor.Monoidal.Braided using (module Strong)
+open Strong using (BraidedMonoidalFunctor)
+
+module Functor.Monoidal.Braided.Strong.Properties
+  {o o′ ℓ ℓ′ e e′ : Level}
+  {C : BraidedMonoidalCategory o ℓ e}
+  {D : BraidedMonoidalCategory o′ ℓ′ e′}
+  (F,φ,ε : BraidedMonoidalFunctor C D) where
+
+import Categories.Category.Construction.Core as Core
+import Categories.Category.Monoidal.Utilities as ⊗-Utilities
+import Functor.Monoidal.Strong.Properties as MonoidalProp
+
+open import Categories.Functor.Properties using ([_]-resp-≅)
+
+private
+
+  module C = BraidedMonoidalCategory C
+  module D = BraidedMonoidalCategory D
+
+open D
+open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ)
+open ⊗-Utilities monoidal using (_⊗ᵢ_)
+open BraidedMonoidalFunctor F,φ,ε
+open MonoidalProp monoidalFunctor public
+
+private
+
+  variable
+    A B : Obj
+    X Y : C.Obj
+
+  σ : A ⊗₀ B ≅ B ⊗₀ A
+  σ = braiding.FX≅GX
+
+  σ⇐ : B ⊗₀ A ⇒ A ⊗₀ B
+  σ⇐ = braiding.⇐.η _
+
+  Fσ : F₀ (X C.⊗₀ Y) ≅ F₀ (Y C.⊗₀ X)
+  Fσ = [ F ]-resp-≅ C.braiding.FX≅GX
+
+  Fσ⇐ : F₀ (Y C.⊗₀ X) ⇒ F₀ (X C.⊗₀ Y)
+  Fσ⇐ = F₁ (C.braiding.⇐.η _)
+
+  φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y)
+  φ = ⊗-homo.FX≅GX
+
+open HomReasoning
+open Shorthands using (φ⇐)
+
+braiding-compatᵢ : Fσ {X} {Y} ∘ᵢ φ ≈ᵢ φ ∘ᵢ σ
+braiding-compatᵢ = ⌞ braiding-compat ⌟
+
+braiding-compat-inv : φ⇐ ∘ Fσ⇐ {X} {Y} ≈ σ⇐ ∘ φ⇐
+braiding-compat-inv = to-≈ braiding-compatᵢ