Do-notation in type theory

• arrow notation - terms have a unique derivation
• arrow notation - quotienting by interchange
• arrow 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.