2 files changed, 53 insertions, 0 deletions
diff --git a/Category/Monoidal/Hypergraph.agda b/Category/Monoidal/Hypergraph.agda
new file mode 100644
index 0000000..bfc4c26
--- /dev/null
+++ b/Category/Monoidal/Hypergraph.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level; _⊔_)
+
+module Category.Monoidal.Hypergraph {o ℓ e : Level} {C : Category o ℓ e} {M : Monoidal C} (S : Symmetric M) where
+
+import Categories.Category.Monoidal.Interchange.Braided as Interchange
+
+open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
+open import Object.Monoid.Frobenius S using (IsSpecialCommutativeFrobeniusMonoid)
+
+open Category C
+open Symmetric S
+
+open Interchange braided using (module swapInner)
+open Shorthands using (λ⇒; λ⇐)
+open swapInner renaming (from to i⇒)
+
+record Hypergraph : Set (o ⊔ ℓ ⊔ e) where
+
+  field
+    scfm : {A : Obj} → IsSpecialCommutativeFrobeniusMonoid A
+
+  open module ISCFM {A} = IsSpecialCommutativeFrobeniusMonoid (scfm {A}) using (μ; η; δ; ϵ)
+
+  field
+    δ-compat : {X Y : Obj} → δ {X ⊗₀ Y} ≈ i⇒ ∘ δ ⊗₁ δ
+    μ-compat : {X Y : Obj} → μ {X ⊗₀ Y} ≈ μ ⊗₁ μ ∘ i⇒
+    η-compat : {X Y : Obj} → η {X ⊗₀ Y} ≈ η ⊗₁ η ∘ λ⇐
+    ϵ-compat : {X Y : Obj} → ϵ {X ⊗₀ Y} ≈ λ⇒ ∘ ϵ ⊗₁ ϵ
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