Freyd category
References
- Call-By-Push-Value, A Functional-Imperative Synthesis (Levy, 2004)
- Freyd Categories Are Enriched Lawvere Theories (Staton, 2013)
- Environments, continuation semantics and indexed categories (Power, Thielecke)
- Arrows, like Monads, are Monoids (Heunen, Jacobs) discusses the correspondence between strong promonads and locally small Freyd categories (Theorem 5.4).