Add Frobenius monoids and hypergraph categoriesmain

1 files changed, 20 insertions, 0 deletions

diff --git a/Category/Monoidal/Hypergraph/Bundle.agda b/Category/Monoidal/Hypergraph/Bundle.agda
new file mode 100644
index 0000000..3b18613
--- /dev/null
+++ b/Category/Monoidal/Hypergraph/Bundle.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Monoidal.Hypergraph.Bundle where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Category.Monoidal.Hypergraph using (Hypergraph)
+open import Level using (Level; _⊔_; suc)
+
+record HypergraphCategory {o ℓ e : Level} : Set (suc (o ⊔ ℓ ⊔ e)) where
+
+  field
+    U : Category o ℓ e
+    monoidal : Monoidal U
+    symmetric : Symmetric monoidal
+    hypergraph : Hypergraph symmetric
+
+  open Symmetric symmetric public
+  open Hypergraph hypergraph public