arrow notation

I will be calling Arrow notation to the arrow do-notation of Haskell, internal language for strong promonads.

• Freyd category arrow notation
• symmetric monoidal arrow notation
• copy-discard-compare arrow notation
• copy-discard arrow notation
• do-notation - composition
• do-notation - terms have a unique derivation
• do-notation - quotienting by interchange
• do-notation - theory of effectful copy-discard categories
• do-notation - loop do-notation

Prerequisites

• Freyd category
• effectful category
• symmetric monoidal category
• adjunction

Tags: internal language.