* 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