Data refinement and algebraic structure

We recall Hoare's formulation of data refinement in terms of upward, downwa rd and total simulations between locally ordered functors from the structur ed locally ordered category generated by a programming language with an abs tract data type to a semantic locally ordered category: we use a Simple imp erative language with a data type for stacks as leading example. We give a unified category theoretic account of the sort of structures on a category that allow upward simulation to extend from ground types and ground program s to all types and programs of the language. This answers a question of Hoa re about the category theory underlying his constructions. It involves a ca reful study of algebraic structure on the category of small locally ordered categories, and a new definition of sketch of such structure. This is acco mpanied by a range of derailed examples. We extend that analysis to total s imulations for modelling constructors of mixed variance such as higher orde r types.