Lax naturality through enrichment^{∗}

Dedicated to Robert Gordon on the occasion of his 60th birthday

Yoshiki Kinoshita^{†}and John Power^{‡}

26 December, 1994 Revised 26 July, 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 theory underlying his constructions, but he was unaware of the details.

Prompted by Hoare’s question, the second author of this paper wrote an article “An algebraic formulation for data refinement” [14] in which he gave a partial answer by use of monads on enriched categories, and the connection between monads and universal algebra. However, the answer was only partial because the theory of monads on enriched categories was insufficient at the time to encapsulate all of Hoare’s constructions. Specifically, there was an account of monads enriched over a symmetric monoidal closed category (see [13], or [17] for an account directed towards computer scientists); but no account in which the symmetry axiom is dropped. Dropping assymmetry is essential because Hoare used lax transformations which are inherently assymetric (see Section 2). That in turn prompted the second author to write a series of articles, [5], [6] and [4], with Robert Gordon to extend the relationship between enriched monads and algebraic structure by dropping symmetry. That has now been completed, but the articles are accessible to only a tiny readership as they are written in the setting of categories enriched over biclosed bicategories, and assume some knowledge of that setting. Moreover, although establishing the central abstract result required, they are not immediately reducible to Hoare’s question without further analysis as there are special features of the enriched categories implicit in his work.

∗This work has been done with the support of the MITI’s Cooperative Architecture Project. The second author also acknowledges the support of ESPRIT Basic Research Action 6453: Types for proofs and programs.

†Cooperative Architecture Project Team, Electrotechnical Laboratory, 1–1–4 Umezono, Tsukuba-shi, Ibaraki, 305 Japan

‡Department of Computer Science, University of Edinburgh, King’s Buildings, Edinburgh, EH9 3JZ Scotland

So, in this paper, we give a more broadly accessible account of algebraic structure on categories enriched over the particular monoidal biclosed category LocOrd_{l}: that is the category of small locally ordered categories, together with the tensor product ⊗ (described in Section 2) for which − ⊗ A has right adjoint given by Lax(A, −), where Lax(A, B) is given by locally ordered functors and lax transformations. Of course, LocOrd_{l} was the monoidal biclosed category implicitly used by Hoare, as explained in [14]. Although motivated by Hoare’s constructions, this is inherently a mathematical paper rather than a computer science one, as we give an abstract treatment of small locally ordered categories with algebraic structure. The special features of LocOrd_{l} that we use arise primarily in studying sketches and contravariance. Note that this paper does not definitively establish the connection to the computer science problem of data refinement, as Hoare’s development remains to be fleshed out and properly analysed.

We were pleasantly surprised to discover (Proposition 8.2) that small locally ordered categories, locally ordered functors, and lax transformations that pointwise have left adjoints, form a 2-category (but see [2] for a more general result). In fact, it is technically delicate but not difficult to prove that they form a locally finitely presentable 2-category. A mild variant of that formed the basis for Hoare’s account of structures of mixed variance, such as the closure in a cartesian closed locally ordered category. We were also pleased (Theorem 7.3) to see that a careful analysis of cotensors allows us to deduce that the universal property of the free algebra on a sketch extends to account for structure respecting lax transformations: that is not simply an assertion that the evident forgetful functor enriches.

The paper is organized as follows. In Section 2, we describe the enrichment we require and give the basic category theoretic definitions. In Sections 3 and 4, we describe the abstract mathematical result we require. In Section 5, we adapt it to our particular setting, and spell it out more explicitly. Section 6 is devoted to examples. Section 7 gives an account of sketches, and Section 8 accounts for contravariance, thus completing our analysis.

2 V-monads for monoidal biclosed V

A monoidal category V is called biclosed if for every object X of V, both − ⊗ X: V_{∘} → V_{∘} and X ⊗ −: V_{∘} → V_{∘} have right adjoints, denoted [ X, −]_{r} and [ X, −]_{l} respectively. For monoidal biclosed locally small V, it is evident how to define V-categories, V-functors and V-natural transformations, yielding the 2-category V-Cat of small V-categories. The category V_{∘} enriches to a V-category with hom given by [ X, Y ]_{r}. Note that [ X, Y ]_{r} cannot be replaced by [ X, Y ]_{l} here, using the usual conventions of Kelly’s book [11]. One can speak of representable V-functors and there is an elegant theory of V-adjunctions, see for instance [5]. If V_{∘} is complete, then it is shown in [18] that V-Cat is complete. So we can speak of the Eilenberg-Moore Vcategory for a V-monad. If V is also cocomplete, there is an elegant theory of limits and colimits in V-categories generalising the situation for symmetric monoidal closed V, see for instance [6].

Spelling out the situation for monads, a V-monad on a V-category C consists of a V-functor T: C → C and V-natural transformations η: 1 → T and μ: T^{2} → T satisfying the usual three axioms. The Eilenberg-Moore V-category T -Alg has as objects the T_{∘}-algebras, where T_{∘} is the ordinary monad underlying T, on the ordinary category C_{∘} underlying C. Given algebras ⟨A, a⟩ and ⟨B, b⟩, the hom object T -Alg(⟨A, a⟩, ⟨B, b⟩) is the equaliser in V of the diagram

[figure: C(A, B); C(a, B); C(T (A), B); T; C(T (A), b); C(T (A), T (B))]  (1)

Composition in T -Alg is determined by that in C.

There is a forgetful V-functor U: T -Alg → C, and it has a left adjoint. If C is complete, then so is T -Alg, and U preserves limits.

Our leading example of monoidal biclosed V is given as follows. Given locally ordered categories A and B, and locally ordered functors H, K: A → B a lax transformation α: H ⇒ K from H to K consists of, for each object a of A, an arrow α_{a}: H(a) → K(a), such that for every arrow f: a → b in A, we have

[figure: H(a); α_{a}; K(a); ≥; H(b); H(f); α_{b}; K(b).; K(f)]  (2)

Dually, an oplax transformation from H to K has the same data but with the inequality of (2) reversed. Given lax transformations α, β: H ⇒ K, we say α ≤ β if α_{a} ≤ β_{a} in B for every a in A. Thus we have a locally ordered category Lax(A, B) given by locally ordered functors and lax transformations. Our monoidal biclosed category V consists of the category of small locally ordered categories and locally ordered functors, together with that monoidal structure (described in Gray’s book [8], Theorem I,4.9.) for which, for each object A of V, − ⊗ A has right adjoint Lax(A, −). We call this tensor product the Gray tensor product. To give an explicit definition of it, let A and B be small locally ordered categories. Then we define A ⊗ B to be the locally ordered category

• whose objects are pairs ⟨a, b⟩ ∈ | A | × | B |;

• where a 1-cell from ⟨a, b⟩ to ⟨a′, b′⟩ is a finite sequence of non-identity 1-cells alternating between 1-cells in A and 1-cells in B such that the subsequence of 1-cells in A is a directed path in A from a to a′ and the subsequence of 1-cells in B is a directed path in B from b to b′ (we often write the sequence of 1-cells as a sequence of pairs of a 1-cell and an object, as below);

• whose identity on ⟨a, b⟩ is the empty sequence;

• whose composition is given by first concatenating the sequences, then factoring according to the composition and identities in A and B; and

• whose local order is generated by the local order on A and that on B

and

⟨a, b⟩ \overline{⟨f, b⟩_{}}⟨a′, b⟩

≥

[figure: ⟨a, b′⟩; ⟨a, g⟩; ⟨f, b′⟩; ⟨a′, b′⟩; ⟨a′, g⟩]

for any f: a → a′ and g: b → b′.

For example,

⟨a, b⟩ \overline{f_{1}: a → a_{1} ^{}}⟨a_{1}, b⟩

[figure: ⟨a_{1}, b_{1}⟩; g_{1}: b → b_{1}; f_{2}: a_{1} → a′; ⟨a′, b_{1}⟩]

⟨a′, b′⟩ g_{2}: b_{1} → b_{}

with f_{i} ≠ id, g_{i} ≠ id for i = 1, 2, is a 1-cell from ⟨a, b⟩ to ⟨a′, b′⟩. The sequence alternates between maps in A and maps in B. The two subsequences

are a →^{f_{1}} a_{1} →^{f_{2}} a′ and b →^{g_{1}} b_{1} →^{g_{2}} b′. To compose this 1-cell and ⟨a′, b′⟩ →^{h: b′→b′′}

⟨a′, b′′⟩, we must compose g_{2} with h. Then if that composite is id, delete it from the sequence.

A variant of the Gray tensor product is now appearing extensively in category theory, for instance in [7]. The Gray tensor product, as defined here, is not symmetric, but it is biclosed: A ⊗ − has right adjoint given by Oplax(A, −), where Oplax(A, B) is the locally ordered category of locally ordered functors from A to B and oplax transformations between them. We will denote this monoidal biclosed category by LocOrd_{l}.

3 Locally finitely presentable V-categories

A monoidal biclosed category V is called locally finitely presentable as a closed category if V_{∘} is locally finitely presentable, if the unit I of V is finitely presentable, and if x ⊗ y is finitely presentable whenever x and y are.

LocOrd_{l} is locally finitely presentable as a closed category. Henceforth, all monoidal biclosed categories to which we refer will be assumed to be locally finitely presentable as closed categories.

A V-category C is said to have finite tensors if for every finitely presentable object x of V, and for every object A of C, [ x, C(A, −) ]_{r}: C → V is representable, i.e., if there exists an object x ⊗ A of C together with a natural isomorphism [ x, C(A, −) ]_{r} ≅ C(x ⊗ A, −). The V-category C has finite cotensors if it satisfies the dual condition that for every finitely presentable x in V and every A in C, the V_{t}-functor [ x, C(−, A) ]_{l}: C^{op} → V_{t} is representable, where V_{t} is the dual of V; i.e., there exists an object x ∩| A of C together with a natural isomorphism [ x, C(−, A) ]_{l} ≅ C(−, x ∩| A). A V-category C is cocomplete whenever C_{∘} is cocomplete, C has finite tensors, and x ⊗ −: C_{∘} → C_{∘} preserves colimits for all finitely presentable x. A cocomplete V-category C is locally finitely presentable (lfp) if C_{∘} is locally finitely presentable, C has finite cotensors, and x ∩| −: C_{∘} → C_{∘} preserves filtered colimits for all finitely presentable x.

For any V that is locally finitely presentable as a closed category, V is necessarily a locally finitely presentable V-category. So, in particular, LocOrd_{l} is a locally finitely presentable LocOrd_{l}-category.

4 Algebraic Structure

We now define algebraic structure on an lfp V-category C. Let | C_{f} | denote the discrete V-category on the set of (isomorphism classes of) finitely presentable objects in C_{∘}. Then a signature on C consist of a V-functor S: | C_{f} | → C. For each c ∈ | C_{f} |, S(c) is called the object of basic operations of arity c.

From S, we construct F (S): C_{f} → C as follows: set

S_{0} = J, the inclusion of C_{f} in C
S_{n+1} = J + ∑_{d∈| C_{f} |} C(d, S_{n}(−)) ⊗ S(d),

and define

σ_{0}: S_{0} → S_{1} to be inj: J → J + ∑_{d∈| C_{f} |} C(d, S_{0}(−)) ⊗ S(d)

σ_{n} = J + ∑_{d∈| C_{f} |} C(d, σ_{n−1}(−)) ⊗ S(d): S_{n} → S_{n+1}

F (S) = colim_{n<ω} S_{n}.

In many cases of interest, each σ_{n} is a monomorphism, so F (S) is the union of { S_{n} }_{n<ω}. For each c, we call F (S)(c) the object of derived c-ary operations.

A signature is typically accompanied by equations between derived operations. So we define the equations of an algebraic theory with signature S to consist of a V-functor E: | C_{f} | → C together with V-natural transformations τ_{1}, τ_{2}: E → F (S)(K(−)), where K: | C_{f} | → C_{f} is the inclusion.

Algebraic structure on C consists of a signature S, together with equations ⟨E, τ_{1}, τ_{2}⟩. We will generally denote algebraic structure by ⟨S, E⟩, suppressing τ_{1} and τ_{2}.

We now define the algebras for a given algebraic structure. Given a signature S, an S-algebra consists of an object A of C together with a map ν_{c}: C(c, A) → C(S(c), A) for each c. So, an S-algebra consists of a carrier A and an interpretation of the basic operations of the signature. This interpretation extends canonically to the derived operations, giving an F (S)(K(−))- algebra, as follows:

ν_{0}: C(c, A) → C(S_{0}(c), A) is the identity;

to give ν_{n+1}: C(c, A) → C(S_{n+1}(c), A), using the fact that C(−, A) preserves colimits, is to give a map C(c, A) → C(c, A), which we will make the identity, and for each d in | C_{f} |, a map

C(c, A) → [ C(d, S_{n}(c)), C(S(d), A) ]_{r},

or equivalently, C(c, A)⊗C(d, S_{n}(c)) → C(S(d), A), which is given inductively by

[figure: C(c, A) ⊗ C(d, S_{n}(c)); ν_{n} ⊗ id; C(S_{n}(c), A) ⊗ C(d, S_{n}(c)); comp; C(d, A); ν; C(S(d), A)]

Given signature S and equations E, an ⟨S, E⟩-algebra is an S-algebra that satisfies the equations, i.e., an S-algebra ⟨A, ν⟩ such that both legs of

[figure: C(c, A); ν_{ω}; C(F (S)(Kc), A); C(τ_{1}_{c}, A); C(τ_{2}_{c}, A); C(E(c), A)]

agree.

Given ⟨S, E⟩-algebras ⟨A, ν⟩ and ⟨B, δ⟩, we define the hom object ⟨S, E⟩-Alg(⟨A, ν⟩, ⟨B, δ⟩) to be the equaliser in V of

[figure: C(A, B); { C(c, −) }_{c∈| C_{f} |}; ∏_{c}[ C(c, A), C(c, B) ]_{r}; ∏_{c}[ C(S(c), A), C(S(c), B) ]_{r}; { C(S(c), −) }_{c∈| C_{f} |}; ∏_{c}[ ν_{c}, C(S(c), B) ]_{r}; ∏_{c}[ C(c, A), C(S(c), B) ]_{r}.; ∏_{c}[ C(c, A), δ_{c}]_{r}] (3)

This agrees with our usual universal algebraic understanding of the notion of homomorphism of algebras, internalising it to V. ⟨S, E⟩-Alg can then be made into a V-category in which composition is induced by that in C. An arrow in the underlying ordinary category ⟨S, E⟩-Alg_{∘} is an arrow f: A → B in C_{∘} such that for all finitely presentable c, fν_{c}(−) = δ_{c}(f−): C(c, A) → C(S(c), B), i.e., an arrow in C_{∘} that commutes with all basic c-ary operations for all c.

The main result of [4], which is central to our work is

Theorem 4.1 A V-category A is equivalent to ⟨S, E⟩-Alg for algebraic structure ⟨S, E⟩ on C if and only if there is a finitary V-monad T on C such that A is equivalent to T -Alg.

5 Algebraic Structure on Locally Ordered Categories

The central part of our abstract theorem, Theorem 4.1, can be expressed with considerably less abstract category theoretic terminology in the case of greatest interest to us. As mentioned earlier, LocOrd_{l} is locally finitely presentable as a closed category, and also as a LocOrd_{l}-category. Moreover, the finitely presentable objects of LocOrd_{l} include all the finite locally ordered categories, which are all that we require. In fact, there are some more finitely presentable objects in LocOrd_{l}, but we will not need them. Further, we only need the forward direction of the theorem. Finally, we can express the definition of algebraic structure with less explicit reference to the tensor product, and we can remove the explicit use of F (S) without important loss of generality.

By mild abuse of notation, let LocOrd_{l}_{f} denote the full sub-LocOrd_{l}- category of LocOrd_{l} determined by the (isomorphism classes of the) finite locally ordered categories, and let | LocOrd_{l}_{f} | denote its set of objects regarded as a discrete LocOrd_{l}-category. Now say a signature on LocOrd_{l} is a LocOrd_{l}-functor S: | LocOrd_{l}_{f} | → LocOrd_{l}, and call S(c) the locally ordered category of basic operations of arity c. We then define

S_{0} = J, the inclusion of LocOrd_{l}_{f} in LocOrd_{l}
S_{n+1} = J + ∑_{d∈| LocOrd_{l}_{f} |} Lax(d, S_{n}(−)) ⊗ S(d),

and define

σ_{0}: S_{0} → S_{1} to be inj: J → J + ∑_{d∈| LocOrd_{l}_{f} |} Lax(d, S_{0}(−)) ⊗ S(d) σ_{n} = J + ∑_{d∈| LocOrd_{l}_{f} |} Lax(d, σ_{n−1}(−)) ⊗ S(d): S_{n} → S_{n+1}.

Then we say algebraic structure on LocOrd_{l} consists of a signature S together with a LocOrd_{l}-functor E: | LocOrd_{l}_{f} | → LocOrd_{l} of equations to-

gether with LocOrd_{l}-natural transformations E [figure: τ_{1}; τ_{2}] S_{n}(K(−)) for some

n, where K: | LocOrd_{l}_{f} | → LocOrd_{l}_{f} is the inclusion. We denote such algebraic structure by ⟨S, E⟩.

Given a signature S, an S-algebra consists of a small locally ordered category A together with a locally ordered functor ν_{c}: Lax(c, A) → Lax(S(c), A) for each finite c. An S-algebra extends to an S_{n}-algebra for each n, by induction as follows:

• ν_{0}: Lax(c, A) → Lax(S_{0}(c), A) is the identity

• ν_{n+1}: Lax(c, A) → Lax(S_{n+1}(c), A) is given using the inductive definition of S_{n+1}, by the identity functor from Lax(c, A) to Lax(c, A), and for each finite d, the functor

Lax(c, A) → Lax(Lax(d, S_{n}(c)), Lax(S(d), A))

given by

Lax(c, A)

\begin{matrix}ν_{n} \\ \end{matrix}
Lax(S_{n}(c), A)

“postcomposition”
Lax(Lax(d, S_{n}(c)), Lax(d, A))
\overline{Lax(id, ν_{d})} Lax(Lax(d, S_{n}(c)), Lax(S(d), A)).

So, this takes a functor h: c → A to the functor from Lax(d, S_{n}(c)) to Lax(S(d), A) taking φ: d → S_{n}(c) to ν(ν_{n}(h) ∘ φ): S(d) → A.

An ⟨S, E⟩-algebra is an S-algebra such that both legs of

[figure: Lax(c, A); ν_{n}; Lax(S_{n}(K(c)), A); Lax(τ_{1}_{c}, A); Lax(τ_{2}_{c}, A); Lax(E(c), A)]

agree.

The LocOrd_{l}-category ⟨S, E⟩-Alg is defined in the evident way, by restricting (3) appropriately. Then we have

Corollary 5.1 For any algebraic structure ⟨S, E⟩ on LocOrd_{l}, ⟨S, E⟩-Alg is finitarily LocOrd_{l}-monadic over LocOrd_{l}.

6 Examples

In this section, we give a series of examples, all implicit in Hoare’s work, of algebraic structures ⟨S, E⟩ on LocOrd_{l}. Theorem 4.1 tells us that for each such algebraic structure, there is a finitary monad T on LocOrd_{l} for which the LocOrd_{l}-category ⟨S, E⟩-Alg of algebras for the given algebraic structure is equivalent to T -Alg.

For a particularly simple example of algebraic structure on LocOrd_{l}, consider

Example 6.1 S: | LocOrd_{l}_{f} | → LocOrd_{l}

S(c) = \{ \begin{matrix}1 & if c = 1 \\ 0 & otherwise, \end{matrix}

with E(c) = 0 for all c. An ⟨S, E⟩-algebra is then a small locally ordered category A, together with an endofunctor on it: this follows since Lax(1, A) is equivalent to A. This agrees with Hoare’s example of a “functorial generator”, which is one of his two leading examples.

Example 6.2 S: | LocOrd_{l}_{f} | → LocOrd_{l}

S(c) = \{ \begin{matrix}1 & if c = 2, where 2 is the discrete category on two elements, \\ 0 & otherwise, \end{matrix}

with E(c) = 0 for all c. An ⟨S, E⟩-algebra is a small locally ordered category A together with a locally ordered functor ∘: A × A → A.

Example 6.3 S: | LocOrd_{l}_{f} | → LocOrd_{l}

S(c) = \{ \begin{matrix}2 & if c = 1, where 2 is the category \{ 0 → 1 \} \\ 0 & otherwise, \end{matrix}

and E(c) = 0 for all c.

An ⟨S, E⟩-algebra is a small locally ordered category A together with two locally ordered endofunctors H and K on it, and an oplax transformation from H to K: this is because a locally ordered functor from A ≅ Lax(1, A) to Lax(2, A) amounts to exactly the above. This is the second of Hoare’s two leading examples, that of a “simulation generator”.

Example 6.4 To obtain a small strict monoidal locally ordered category as an ⟨S, E⟩-algebra, first put

S(c) = \{ \begin{matrix}1 & if c = 2 \\ 1 & if c = 0 \\ 0 & otherwise \end{matrix}

Then an S- algebra is a small locally ordered category A together with locally ordered functors ∘: A × A → A and I: 1 → A.

The equations apply to derived operations; so we need to describe S_{2}.

S_{0}: LocOrd_{l}_{f} → LocOrd_{l} is the inclusion J.
S_{1}(c) = c + ∑_{d∈| LocOrd_{l}_{f} |} Lax(d, c) ⊗ S(d),

but for all d other than 0 and 2, S(d) = 0, and so Lax(d, c) ⊗ S(d) = 0; and Lax(0, c) = 1 and Lax(2, c) = c × c. So

S_{1}(c) = c + S(0) + (c × c) ⊗ S(2) = c + 1 + c × c.

The S-algebra ⟨A, I: 1 → A, ∘: A × A → A⟩ yields an S_{1}-algebra ⟨A, ν_{1}⟩ given by A, and the functor from Lax(c, A) to Lax(S_{1}(c), A) with

• first component Lax(c, A) → Lax(c, A) the identity

• second component Lax(c, A) → Lax(1, A) the constant at I

• third component Lax(c, A) → Lax(c × c, A) sending h to the functor sending ⟨X, Y ⟩ to h(X) ∘ h(Y).

Now,

S_{2}(c) = c + ∑_{d∈| LocOrd_{l}_{f} |} Lax(d, S_{1}(c)) ⊗ S(d).

Again, for all d other than 0 and 2, S(d) = 0, and so Lax(d, S_{1}(c))⊗S(d) = 0; Lax(0, S_{1}(c)) = 1, and Lax(2, S_{1}(c)) = S_{1}(c) × S_{1}(c). So,

S_{2}(c) = c + S(0) + (S_{1}(c) × S_{1}(c)) ⊗ S(2)
= c + 1 + S_{1}(c) × S_{1}(c).

Our S-algebra yields the S_{2}-algebra given by A and the locally ordered functor from Lax(c, A) to Lax(S_{2}(c), A) with

• first component Lax(c, A) → Lax(c, A) the identity

• second component Lax(c, A) → Lax(1, A) the constant at I

• third component Lax(c, A) → Lax(S_{1}(c) × S_{1}(c), A) sending h to the functor sending a pair ⟨X, Y ⟩ to (ν_{1}h)(X) ∘(ν_{1}h)(Y).

Spelling out the third component in more detail, S_{1}(c) = c + 1 + c × c. So there are nine classes of possibilities for the pair ⟨X, Y ⟩, and we have Lax(c, A) → Lax((c + 1 + c × c) × (c + 1 + c × c), A). On the first and second components of each copy of S_{1}(c) respectively, our functor sends h to X ↦ h(X) ∘ I. On the second and first component respectively, h is sent to X ↦ I ∘ h(X). On the first and third components, we have h sent to ⟨X, ⟨Y, Z⟩⟩ ↦ h(X) ∘(h(Y) ∘ h(Z)). On the third and first components, h goes to ⟨⟨X, Y ⟩, Z⟩ ↦ (h(X) ∘ h(Y)) ∘ h(Z). So we put

E(c) = \{ \begin{matrix}2 & if c = 1, \\ 1 & if c = 3, \\ 0 & otherwise, \end{matrix}

and define τ_{1}, τ_{2}: E → S_{2} with components

τ_{1}, τ_{2}: E(1) ⟶ S_{2}(1) = 1 + S(0) + S_{1}(1) × S_{1}(1),

so that τ_{1} is the constant on the first component of S_{2}(1), and τ_{2} sends one element to the first and second component of the copies of S_{1}(1) and sends the other element to the second and first components of the copies of S_{1}(1); and we define τ_{1}, τ_{2}: E(3) → S_{2}(3) = 3 + S(0) + S_{1}(3) × S_{1}(3) by having τ_{1} choose the first and third components of S_{1}(3) = 3 + 1 + 3 × 3, thus an element of 3 × (3 × 3), and we choose that element by choosing the first, second and third components of 3 respectively; and similarly for τ_{2} but with the third and first components of S_{1}(3).

Then, an ⟨S, E⟩-algebra is precisely a small strict monoidal locally ordered category. With some effort, one can modify ⟨S, E⟩ so that an ⟨S, E⟩-algebra is a small monoidal locally ordered category; one can add symmetry too.

Example 6.5 To obtain a small locally ordered category with a terminal object as an ⟨S, E⟩-algebra, we first consider what an equational formulation of such a locally ordered category would entail. We require a small locally ordered category A, together with an object T of A, equivalently a functor from 1 = Lax(0, A) to A = Lax(1, A). We also require for each object X of A, a map from X to T. This is given by the existence of a functor t from A = Lax(1, A) to Lax(2, A), subject to equations to assert that the first component of t_{X} must be X, and the second component must be T. That is forced by commutativity of the diagrams

[figure: A; t; Lax(2, A); id; A; Lax(∂_{0}, A); and; A; t; Lax(2, A); 1; T; A.; Lax(∂_{1}, A)]

Observe that the presence of t also asserts that for every arrow f: X → Y in A, we have

[figure: X; t_{X}; T; ≤; Y; f; t_{Y}; T.; ^{id^{T}}]  (4)

But that is a harmless addition, as that is true for any map f: X → Y in a locally ordered category with terminal object T.

Finally, we must assert the unicity of t_{X}. To do that, it suffices to add the equation t_{T} = id_{T}, which amounts to the commutativity of

[figure: 1; T; A; A; T; Δ; Lax(2, A); t]

and to assert that for each f: X → Y, diagram (4) commutes: for that is always true in any category with terminal object T, and it follows from the commutativity that we have the desired unicity by putting Y = T and since t_{T} = id_{T}. To express that commutativity, we need a new operation

(−)_{t}: Lax(2, A) → Lax(3, A)

taking a map f: X → Y to a commutative triangle, together with equations to force that commutative triangle to be of the form

X  \overline{f  ^{}}Y
[figure: t_{X}; t_{Y}]
T.

This amounts to the assertion that three diagrams commute. Let 3 have objects a, b and c, with maps from a to b and from b to c. Let inc_{1}: 2 → 3 choose a and b; let inc_{2} choose a and c and let inc_{3} choose b and c. Then we want

Lax(2, A) \overline{(−)_{t}^{}}Lax(3, A)
[figure: id]
Lax(2, A), Lax(inc_{1}, A)_{}

Lax(2, A) \overline{(−)_{t}^{}}Lax(3, A)

[figure: A; Lax(∂_{0}, A); t; Lax(2, A); Lax(inc_{2}, A)]

and

Lax(2, A) \overline{(−)_{t}^{}}Lax(3, A)

[figure: A; Lax(∂_{1}, A); t; Lax(2, A).; Lax(inc_{3}, A)]

We can then encode these operations and equations in terms of algebraic structure, just as we did for small strict monoidal locally ordered categories, c.f.[3].

Example 6.6 The argument of Example 6.5 is representative: it extends without much effort to binary products (Hoare’s “cartesian product”), an initial object and binary coproducts (Hoare’s “discriminated union”). It does not seem to extend to small locally ordered categories with equalisers, the reason being that given a diagram of the form

[figure: A; f; g; B; A′; h; f′; g′; B′; k]

with f′h ≤ kf and g′h ≤ kg, there is no reason to expect it to extend to the equalisers of ⟨f, g⟩ and ⟨f′, g′⟩.

7 Sketches

It follows from the previous section that many examples of small locally ordered categories with structure form LocOrd_{l}-categories of the form T -Alg for a finitary LocOrd_{l}-monad T on LocOrd_{l}. It follows that for any small locally ordered category L_{0}, one can consider the free T -algebra L on L_{0}; and lax transformations between locally ordered functors from L_{0} to a T - algebra M lift uniquely to structure respecting lax transformations on L.

But to give a full account of Hoare’s data refinement, we need a little more, as his starting point L_{0} need not be just a small locally ordered category, but may also possess some more axioms, such as stating that a certain object be a product of two others.

In order to incorporate that into our account, we need a new definition, so that we can extend the notion of sketch to an “⟨S, E⟩-sketch”, for arbitrary algebraic structure ⟨S, E⟩. This is essentially a special case of Power and Wells’ “E-sketches” [15] but in a somewhat more sophisticated setting.

Definition 7.1 Given algebraic structure ⟨S, E⟩ on a locally finitely presentable V-category C, an ⟨S, E⟩-sketch consists of an object A of C together with a finite family of triples ⟨c_{i}, j_{i}: d_{i} → F (S)c_{i}, φ_{i}: d_{i} → A⟩ consisting of finitely presentable objects c_{i} and d_{i}, and maps j_{i} and φ_{i} in C.

We generally supress j_{i}, leaving it implicit from d_{i}, thus using the notation ⟨c_{i}, d_{i}, φ_{i}⟩.

Given a finite family D of pairs ⟨c_{i}, d_{i}⟩ (with j_{i} implicit), we will call an ⟨S, E⟩-sketch whose family of triples has first two components determined by D an ⟨S, E, D⟩-sketch. A map of ⟨S, E, D⟩-sketches from ⟨A, { φ_{i} }⟩ to ⟨B, { ψ_{i} }⟩ is a map f: A → B in C such that fφ_{i} = ψ_{i} for each i. This gives a category ⟨S, E, D⟩-Sketch, which is finitarily monadic over C_{∘}: in fact, we can enrich it to a V-category finitarily monadic over C by describing ⟨S_{D}, E_{D}⟩ by

S_{D}(c) = \{ \begin{matrix}∑_{i} d_{i} & if c = 0, \\ 0 & otherwise \end{matrix}

and E_{D}(c) = 0 for all c.

Also, given D, we define a category ⟨S, E, D⟩-Alg with objects ⟨S, E⟩- algebras ⟨A, ν⟩ together with, for each ⟨c_{i}, d_{i}⟩, a map h_{i}: c_{i} → A. Note that the domain of h_{i} is c_{i}, not d_{i}, but each h_{i}: c_{i} → A determines the map ν(h_{i}) ∘ j_{i}: d_{i} → A. The maps of ⟨S, E, D⟩-Alg are evident. It is finitarily monadic over C_{∘}, and the evident functor U: ⟨S, E, D⟩-Alg → ⟨S, E, D⟩-Sketch commutes with the forgetful functors to C_{∘} and hence has a left adjoint F (See [1] Section 3.7 and [15]).

Now, to incorporate all the data Hoare has in his L_{0} into our account, we view L_{0} as an ⟨S, E, D⟩-sketch for appropriate ⟨S, E, D⟩ and L = F(L_{0}). We need to do a little more work to obtain the result we seek, but first for an example

Example 7.2 Let ⟨S, E⟩ be the algebraic structure for small locally ordered categories with binary products. Let D consist of one pair ⟨2, d⟩, where d is the free category on the graph

· ← · → · ,

with the inclusion into F (S)(2) yielding that part of F (S)(2) that gives the product cone over two objects. Then, an object of ⟨S, E, D⟩-Sketch is a small locally ordered category together with a diagram of the form

A ←^{f} C →^{g} B.

An object of ⟨S, E, D⟩-Alg is a small locally ordered category B with binary products, together with a pair ⟨X, Y ⟩ of objects of B. A map in ⟨S, E, D⟩-Sketch from A to U(B) is a locally ordered functor H: A → B that sends the diagram

A ←^{f} C →^{g} B.

to the cone

X ←^{π_{0}} X × Y →^{π_{1}} Y,

so H(A) = X, H(B) = Y, and H(C) = X × Y, with f and g sent to the projections. This determines a map in ⟨S, E, D⟩-Alg from F(A) to B: it is a locally ordered functor that strictly preserves binary products and sends ⟨A, B⟩ to ⟨X, Y ⟩. Since it preserves binary products strictly, it takes C to X × Y and respects the projections.

Now, to consider the behaviour of the construction F with respect to lax transformations, given any locally ordered category B, the locally ordered category \overline{B} = Oplax(2, B) has the property that to give a locally ordered functor from any A to \overline{B} is to give a pair of locally ordered functors ⟨G, F ⟩ from A to B, together with a lax transformation α: G ⇒ F, naturally in A. Moreover, it follows from general theory about monads that if B has a T -algebra structure, then \overline{B} acquires a T -algebra structure, and the above universal property lifts to T -Alg.

So, in particular, to give a locally ordered functor from c to \overline{B} is to give a pair ⟨h, k⟩ of locally ordered functors from c to \overline{B} and a lax transformation ρ: h ⇒ k.

So, given an ⟨S, E⟩-algebra ⟨B, ν⟩ together with, for each ⟨c_{i}, d_{i}⟩ in D, a pair ⟨h_{i}, k_{i}⟩ of locally ordered functors from c_{i} to B and a lax transformation ρ: h_{i} ⇒ k_{i}, with corresponding locally ordered functor χ_{i}: c_{i} → \overline{B}, and given an ⟨S, E, D⟩-sketch ⟨A, { φ_{i}: d_{i} → A }⟩, the following correspond bijectively:

• a pair of locally ordered functors G, F: A → B, and a lax transformation α: G ⇒ F such that G(φ_{i}) = ν(h_{i}) ∘ j_{i}, F (φ_{i}) = ν(k_{i}) ∘ j_{i}, and α(φ_{i}) = ν(ρ_{i}) ∘ j_{i}

• an ⟨S, E, D⟩-sketch morphism from ⟨A, \{ φ_{i} \}⟩ to U(⟨\overline{B}, \overline{ν}, \{ χ_{i} \}⟩)

• an ⟨S, E, D⟩-algebra map from F(⟨A, \{ φ_{i} \}⟩) to ⟨\overline{B}, \overline{ν}, \{ χ_{i} \}⟩

• a pair ⟨\overline{G}, \overline{F} ⟩ of ⟨S, E⟩-algebra maps from F(⟨A, \{ φ_{i} \}⟩) to ⟨B, ν⟩

and a 2-cell of ⟨S, E⟩-algebras \overline{α}: \overline{G} ⇒ \overline{F} respecting the D-structures of F(⟨A, { φ_{i} }⟩) and the family ⟨h_{i}, k_{i}, ρ_{i}⟩.

Putting this all together, we have Theorem 7.3 Every sketch respecting lax transformation

α: G ⇒ F: ⟨A, { φ_{i} }⟩ → U(B, ν, h, k, ρ)

extends uniquely to structure respecting

\overline{α}: \overline{G} ⇒ \overline{F}: F(⟨A, \{ φ_{i} \}⟩) → ⟨ B, ν, h, k, ρ ⟩.

8 Contravariance

Finally, we require an account of contravariance. It is well known that the category of small cartesian closed categories does not enrich over Cat. So, it is usual to restrict to enrichment over the cartesian closed category of groupoids. However, when one has locally ordered structure, one can—and Hoare does—do something more delicate, which is to restrict not to lax transformations that are isomorphisms, but to total transformations as follows.

Definition 8.1 Given locally ordered functors G, F: A → B, a total transformation from G to F is a lax transformation α: G ⇒ F such that for every object X of A, α_{X}: G(X) → F (X) has a left adjoint retraction, i.e., there exists a 1-cell ℓ_{X}: F (X) → G(X) such that ℓ_{X} ∘ α_{X} = id_{G(X)} and id_{F (X)} ≤ α_{X} ∘ ℓ_{X}.

It is well known that given the data for α such that each α_{X} has a left adjoint ℓ_{X}, then α is lax if and only if ℓ is oplax (see, for instance, [12]). For the analysis of this section, the assumption that the left adjoint be a retraction is unnecessary. However, it is part of Hoare’s definition, so we include it. This also corresponds to the common domain theoretic notion of a projection-embedding pair.

Proposition 8.2 The following data

• small locally ordered categories

• locally ordered functors

• total transformations

with the evident composition, form a 2-category.

Proof The only non-trivial part is to prove the interchange law; that amounts to showing that, given total transformations α: G ⇒ F: B → C and β: K ⇒ H: A → B, the diagram

[figure: G ∘ K; α ∘ K; F ∘ K; G ∘ H; G ∘ β; α ∘ H; F ∘ H; F ∘ β]

commutes. Given X an object of A, lax naturality of α shows that we have

[figure: G(K(X)); α_{K(X)}; F (K(X)); ≥; G(H(X)); G(β_{X}); α_{H(X)}; F (H(X)).; F (β_{X})]  (5)

But each β_{X} has a left adjoint ℓ_{X}, also a 1-cell in B. So lax naturality of α also asserts that we have

[figure: G(H(X)); α_{H(X)}; F (H(X)); ≥; G(K(X)); G(ℓ_{X}); α_{K(X)}; F (K(X)),; F (ℓ_{X})]  (6)

but since G(ℓ_{X}) ⊣ G(β_{X}) and F (ℓ_{X}) ⊣ F (β_{X}), it follows that by taking the mates under these adjunctions of (6) we have

[figure: G(H(X)); α_{H(X)}; F (H(X)); ≤; G(K(X)); G(β_{X}); α_{K(X)}; F (K(X)).; F (β_{X})]  (7)

Putting (5) and (7) together gives the result.

We call this 2-category Tot.

Proposition 8.3 Tot is locally finitely presentable as a 2-category.

Proof Cotensors with 2 are as follows: given small locally ordered B, an object of 2 ∩| B is a reflection in B, i.e., a 1-cell that has a left adjoint retraction. A 1-cell in 2 ∩| B from h to h′ amounts to a square of the form

[figure: b; ⊂; h; ⊤; c; b′; f; ⊂; h′; ⊤; c′; g]  with g ∘ h ≤ h′ ∘ f.

Then, [ 2, Tot(A, B) ] ≅ Tot(A, 2 ∩| B).

The functor 2 ∩| −: LocOrd_{∘} → LocOrd_{∘} preserves filtered colimits and limits, so has a left adjoint 2 ⊗ −. To describe 2 ⊗ B, first take the tensor in LocOrd_{l}, then freely make the maps of the form ⟨2, b⟩ into reflections, so for instance 2 ⊗ 2 looks like

\overline{} ; ≤ ; ^{^{}⊣ _{}∩} \overline{}^{^{}⊣ _{}∩}.

We already know that LocOrd_{∘} is locally finitely presentable. □

By Proposition 8.3, we have the full strength of our main abstract theorem, Theorem 4.1, immediately at our disposal: the definition of algebraic structure is as before, applied to the V-category Tot, where V is Cat. Our analysis of sketches extends naturally too: the only property we used of \overline{B} was that it was 2 ∩| B. So we have a full account of Hoare’s total simulations in this setting.

Example 8.4 [Closure of a cartesian category] First observe that for any LocOrd_{l}-enriched algebraic structure ⟨S, E⟩ on LocOrd_{l}, ⟨S, E⟩-Alg_{∘} is finitarily monadic over LocOrd_{∘}. It is not automatically true, but nonetheless true in all our examples, that for any such ⟨S, E⟩, it restricts to Cat-enriched algebraic structure on Tot. So we shall only study closure.

To give that, the main data we need is a function that to each pair ⟨X, Y ⟩ provides a diagram of the form

[ X, Y ] × X \overline{ev ^{}}Y
[figure: π_{0}; π_{1}]
[ X, Y ]  X.

So we add

S(2) = [figure: ·; ·; · ·.]

Then Tot(2, A) → Tot(S(2), A) is to make the above construction. Given

reflections X ⟶^{f} ; ⊤ ; ⟵_{g} X′ and Y ⟶^{h} ; ⊤ ; ⟵_{k} Y′, we must verify that in a cartesian

closed locally ordered category, we obtain a pointwise reflection between the diagrams

[figure: [ X, Y ] × X; ev; Y; π_{0}; π_{1}; [ X, Y ]  X; and; [ X′, Y′] × X′; ev′; Y′; π′_{0}; π′_{1}; [ X′, Y′]  X′]

with the right adjoint part lax. The only piece of data that is not completely obvious is the map [ X, Y ] → [ X′, Y′] which is to have a left adjoint retraction; we define it to be

[ X, Y ] \overline{[ g, h]_{}}[ X′, Y′].

It has adjoint [ f, k], which is a retract. The laxness of the right adjoint part is trivial (in fact strict for π_{0} and π_{1}); for ev, it amounts to

[ X, Y ] × X \overline{[ g, h] × f_{}}[ X′, Y′] × X′
≥
[figure: Y; ev; h; Y′,; ev′]

which in fact holds strictly in any cartesian closed category. For the unit, one wants and has exactly

X  \overline{f  ^{}}X′
≥
[figure: [ Y, Y × X]; η; [ k, h × f ]; [ Y′, Y′ × X′].; η]

References

[1] Michael Barr and Charles Wells. Toposes, Triples and Theories, volume 278 of Grundlagen der mathematischen Wissenschaften. Springer-Verlag, 1985.

[2] A. Carboni, G.M. Kelly, and R.J. Wood. A 2-categorical approach to change of base and geometric morphisms I. to appear in Journal of Pure and Applied Algebra.

[3] E.J. Dubuc and G.M. Kelly. A presentation of topoi as algebraic relative to categories or graphs. Journal of Algebra, 81:420–433, 1983.

[4] R. Gordon and A.J. Power. Algebraic structure for bicategory enriched categories. (submitted).

[5] R. Gordon and A.J. Power. Enrichment through variation. Journal of Pure and Applied Algebra. (to appear).

[6] R. Gordon and A.J. Power. Gabriel-Ulmer duality in categories enriched in bicategories. (submitted).

[7] R. Gordon, A.J. Power, and R. Street. Coherence for tricategories. to appear as a volume of Memoirs American Mathematical Society.

[8] J.W. Gray. Formal category theory—adjointness for 2-categories, volume 391 of Springer Lecture Notes in Mathematics. Spriger-Verlag, 1974.

[9] C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271–281, 1972.

[10] C.A.R. Hoare. Data refinement in a categorical setting. unpublished manuscript, 1987.

[11] G. M. Kelly. Basic Concepts of Enriched Category Theory, volume 64 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1982.

[12] G.M. Kelly. Doctrinal adjunction, in Category Seminar Sydney 1972/73, volume 420 of Springer Lecture Notes in Mathematics, pages 257–280. Springer-Verlag, 1974.

[13] G.M. Kelly and A.J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89:163–179, 1993.

[14] A.J. Power. An algebraic formulation for data refinement, in Proceedings of the Mathematical Foundations of Programming Semantics, volume 442 of Springer Lecture Notes in Computer Science, pages 390–401. Springer-Verlag, 1990.

[15] A.J. Power and C. Wells. A formalism for the specification of essentially algebraic structures in 2-categories. Mathematical Structures in Computer Science, 2:1–28, 1992.

[16] R. Nakajima, M. Honda and H. Nakahara. Hierarchical program specification and verification—a many-sorted logical approach. Acta Informatica, 14:135–155, 1980.

[17] Edmund Robinson. Variations on algebra: monadicity and generalisations of equational theories. To appear in Mathematical Structures in Computer Science.

[18] R. Street. Enriched categories and cohomology. Questiones Mathematica, 6:265–283, 1983.

[19] N. Wirth. Program development by stepwise refinement. CACM, 14:221–227, 1971.