From 8ac913160fcb3e6ec6af2b0f4cb25f45edd8212b Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Tue, 28 Oct 2025 12:26:54 -0500 Subject: Add symmetric monoidal structure to Pull and System --- Functor/Monoidal/Strong/Properties.agda | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) (limited to 'Functor/Monoidal/Strong') diff --git a/Functor/Monoidal/Strong/Properties.agda b/Functor/Monoidal/Strong/Properties.agda index f4774b4..9eb7579 100644 --- a/Functor/Monoidal/Strong/Properties.agda +++ b/Functor/Monoidal/Strong/Properties.agda @@ -16,15 +16,17 @@ import Categories.Category.Construction.Core as Core open import Categories.Functor.Monoidal using (StrongMonoidalFunctor) open import Categories.Functor.Properties using ([_]-resp-≅) -module C where - open MonoidalCategory C public - open ⊗-Utilities.Shorthands monoidal public using (α⇐; λ⇐; ρ⇐) +private + + module C where + open MonoidalCategory C public + open ⊗-Utilities.Shorthands monoidal public using (α⇐; λ⇐; ρ⇐) -module D where - open MonoidalCategory D public - open ⊗-Utilities.Shorthands monoidal using (α⇐; λ⇐; ρ⇐) public - open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) public - open ⊗-Utilities monoidal using (_⊗ᵢ_) public + module D where + open MonoidalCategory D public + open ⊗-Utilities.Shorthands monoidal using (α⇐; λ⇐; ρ⇐) public + open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) public + open ⊗-Utilities monoidal using (_⊗ᵢ_) public open D @@ -35,12 +37,12 @@ private variable X Y Z : C.Obj - Fα : F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z)) - Fα = [ F ]-resp-≅ C.associator - α : {A B C : Obj} → (A ⊗₀ B) ⊗₀ C ≅ A ⊗₀ (B ⊗₀ C) α = associator + Fα : F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z)) + Fα = [ F ]-resp-≅ C.associator + λ- : {A : Obj} → unit ⊗₀ A ≅ A λ- = unitorˡ -- cgit v1.2.3