Type Theory for unbiased monoidal categories Type theory for symmetric monoidal categories type theory for a strong monoidal endofunctor Type theory for delayed feedback Syntax sugar for a Lucid language Reduction in symmetric monoidal categories arrow notation