diff options
Diffstat (limited to 'Category/Monoidal/Hypergraph/Bundle.agda')
| -rw-r--r-- | Category/Monoidal/Hypergraph/Bundle.agda | 20 |
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 |