{-# 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