| Lax Naturality Through Enrichment (1995) | |||||||||||||||
Abstract | |||||||||||||||
| We develop the relationship between algebraic structure and monads enriched over the monoidal biclosed category LocOrd l of small locally ordered categories, with closed structure given by Lax(A; B). We state the theorem, give a series of examples, and incorporate an account of sketches and contravariance into the theory. This was motivated by C.A.R. Hoare's use of category theoretic structures to model data refinement. 1 Introduction In 1987, C.A.R. Hoare wrote a draft paper, "Data refinement in a categorical setting" [10] in which he used category theory to provide an abstract formalism for his development of data refinement over the previous twenty years [9]. The notion of data refinement is central to the programming method called stepwise refinement proposed by Wirth [19], and gave rise to work on abstract data types such as the IOTA programming system developed by Nakajima, Honda and Nakahara [16]. As Hoare said in [10], there was evidently a unified body of category theo... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||