Freyd category

Last updated Oct 7, 2024

Freyd category A Freyd category is a cartesian-based strong promonad.

• copyable and discardable Freyd categories

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).