Do-notation in type theory

• do-notation - terms have a unique derivation
• do-notation - quotienting by interchange
• do-notation - composition
• arrow notation

References

• Generalising Monads to Arrows (Hughes)
• A New Notation for Arrows (Patterson)

Tags: Type theory, Type theory for symmetric monoidal categories.