blob: bfc4c261ee20c0f21e113f4697c4dbd5a1baf39b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
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} ≈ λ⇒ ∘ ϵ ⊗₁ ϵ
|
