{-# 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} ≈ λ⇒ ∘ ϵ ⊗₁ ϵ