“Elgot categories” is a term charged with multiple incompatible meanings.
- Elgot Categories and Abacus Programs (Nester, 2025): uses Elgot category for a distributive monoidal category with uniform trace, but additionally with a natural numbers object.
- The Denotational Semantics of SAA (Ghalayini, Krishnaswami, 2024): introduce “distributive Freyd-Elgot categories” (or “strong Elgot structures on distributive Freyd categories”, or “strong Elgot categories”) to be Freyd categories with all coproducts and uniform fixpoints.
- Elgot Theories, A New Perspective of Iteration Theories (Adámek, Milius, Velebil, 2009): Elgot monads and Elgot theories, cocartesian uniform traced.
I have employed “imperative categories” for Freyd categories with strong Elgot structure---in the sense of Ghalayini and Krishnaswami---“imperative monoidal categories” for Elgot categories in the sense of Nester (and, while not necessarily asking for a natural numbers object, certainly expecting it in most examples), and “locally-posetal imperative categories” for those we employ for program logics reasoning.