QYGKKLQAJXTU65RIGPGJ2VGX4R2FNTZCLY3G4PIF6ANJSO7M44KAC
* Relevance-Non-linear Logic
If we have a strong monad T of effects that is
1. Monoidal: the two morphisms from the strength are equal: par : TA x TB -> T (A x B)
this induces for every A1,...,An par_n : T A1 x ⋯ -> T (A1 × ⋯)
Then we have a symmetric multicategory, where
f : ϕA1,... ⊢ ψB
is a morphism
f : A1 x ⋯ -> B
satisfying ψ ∘ T f ∘ par_n = f ∘ ϕA1 × ⋯ : T(A1) × ⋯ -> B
2. Idempotent: For any f : A -> T B, par(f,f) = μ ∘ TΔ ∘ f