Merge pull request #276 from sstucki/interchange

Add interchange for monoidal categories
agda · May 3, 2021 · 5e4de42 · 5e4de42
2 parents 650f1bf + 2261861
commit 5e4de42
Show file tree

Hide file tree

Showing 3 changed files with 756 additions and 0 deletions.
diff --git a/Everything.agda b/Everything.agda
@@ -178,6 +178,7 @@ import Categories.Category.Monoidal.Instance.Rels
 import Categories.Category.Monoidal.Instance.Setoids
 import Categories.Category.Monoidal.Instance.Sets
 import Categories.Category.Monoidal.Instance.StrictCats
+import Categories.Category.Monoidal.Interchange
 import Categories.Category.Monoidal.Properties
 import Categories.Category.Monoidal.Reasoning
 import Categories.Category.Monoidal.Rigid
@@ -282,6 +283,7 @@ import Categories.Functor.Monoidal
 import Categories.Functor.Monoidal.Braided
 import Categories.Functor.Monoidal.Properties
 import Categories.Functor.Monoidal.Symmetric
+import Categories.Functor.Monoidal.Tensor
 import Categories.Functor.Power
 import Categories.Functor.Power.Functorial
 import Categories.Functor.Power.NaturalTransformation