Do-notation in type theory

Last updated Jan 8, 2025

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

References

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

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