From 4e6acbf8b8084bea12327683aceb300a9b64c367 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 3 Sep 2026 19:22:21 -0500
Subject: Add Frobenius monoids and hypergraph categories

---
 Category/Monoidal/Hypergraph/Bundle.agda | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 Category/Monoidal/Hypergraph/Bundle.agda

(limited to 'Category/Monoidal/Hypergraph/Bundle.agda')

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
-- 
cgit v1.2.3