Kan Extensions in Double Categories (opens in new tab)  λFunctional Programming

Previously: Kan extensions in Haskell. In a double category that is also a proarrow equipment, we have the ability to bend arrows. In particular, in the definition of the counit of the right Kan extension: we can bend the vertical arrow, replacing it with its horizontal conjoint . In a profunctor equipment, this is just […]