On the Lambek embedding and the category of
product-preserving presheaves
Peng Fu

Kohei Kishida

Neil J. Ross

Dalhousie University

University of Illinois at Urbana-Champaign

Dalhousie University

Peter Selinger
Dalhousie University

It is well-known that the category of presheaf functors is complete and cocomplete, and that the
Yoneda embedding into the presheaf category preserves products. However, the Yoneda embedding
does not preserve coproducts. It is perhaps less well-known that if we restrict the codomain of
the Yoneda embedding to the full subcategory of limit-preserving functors, then this embedding
preserves colimits, while still enjoying most of the other useful properties of the Yoneda embedding.
We call this modified embedding the Lambek embedding. The category of limit-preserving functors
is known to be a reflective subcategory of the category of all functors, i.e., there is a left adjoint for the
inclusion functor. In the literature, the existence of this left adjoint is often proved non-constructively,e.g., by an application of Freyd’s adjoint functor theorem. In this paper, we provide an alternative,
more constructive proof of this fact. We first explain the Lambek embedding and why it preservescoproducts. Then we review some concepts from multi-sorted algebras and observe that there isa one-to-one correspondence between product-preserving presheaves and certain multi-sorted term
algebras. We provide a construction that freely turns any presheaf functor into a product-preserving
one, hence giving an explicit definition of the left adjoint functor of the inclusion. Finally, we sketch
how to extend our method to prove that the subcategory of limit-preserving functors is also reflective.

1

Introduction

Let A be a small category. Recall that a presheaf over A is just a functor F : Aop → Set. The category
op
SetA of presheaves has many desirable properties. It is complete and cocomplete, cartesian-closed, andopeven a topos. If A is monoidal, then SetA is monoidal closed, where tensor products and exponentials
opare given by Day’s convolution [1]. Also, the Yoneda embedding y : A → SetA is full and faithful. These
properties make the presheaf category a natural candidate for modeling linear functional programming
languages [5, 8, 9].
Although the Yoneda embedding preserves all existing products (and more generally, limits), it does
not preserve coproducts. In some situations, it is useful to have a version of the Yoneda embedding that
also preserves coproducts. For example, in our work on the categorical semantics of quantum programming languages [5], we start with a base category that models quantum operations, which is monoidal
but not necessarily monoidal closed. In order to account for lambda abstraction (i.e., currying), we canembed the base category into its presheaf category. Sometimes the base category already has coproducts,
and it is natural, and often technically necessary, to require the embedding to also preserve these coproducts. Fortunately, in this situation, there is a variant of the Yoneda embedding, which we call the Lambek
embedding [7], that achieves exactly that.
Before we explain the Lambek embedding, let us first recall why the Yoneda embedding does notpreserve coproducts. Let us consider a small category A with a distinguished object I and a coproduct© P. Fu, K. Kishida, N. J. Ross, P. Selinger
This work is licensed under theCreative Commons Attribution License.

2

On the Lambek embedding and the category of product-preserving presheaves
op

I + I. Let y : A → SetA be the Yoneda embedding, given by y(A) = Hom(−, A). We must show thaty(inj )y(inj )

1y(I) −−−→y(I + I) ←−−2− y(I)op

is not a coproduct cone in SetA . Suppose it is a coproduct cone. Since we know that
inj

inj

1
2
y(I) −−→y(I) + y(I) ←−−y(I)is also a coproduct cone, there exists a unique isomorphism f : y(I + I) → y(I) + y(I) such that thefollowing composition is identity:[y(inj ),y(inj )]f2y(I) + y(I) −−−−1−−−−→ y(I + I) −−→ y(I) + y(I).
op
The Yoneda lemma states that SetA (y(A), F) ∼= F(A) for all F : Aop → Set and A ∈ A. In particular, we
have
opSetA (y(I + I), y(I) + y(I)) ∼= Hom(I + I, I) + Hom(I + I, I).

Since an element in the disjoint union Hom(I + I, I) + Hom(I + I, I) either belongs to the left compoop
nent or the right component, it easily follows that f ∈ SetA (y(I + I), y(I) + y(I)) must be a naturaltransformation that either maps its entire domain to the left component of its codomain, or to the rightcomponent. This implies that f ◦ [y(inj1 ), y(inj2 )] ̸= id.
op
op
We now define the Lambek embedding. Let [SetA ]× be the full subcategory of SetA consisting ofproduct-preserving functors. Note that a product in Aop is a coproduct in A, so that a product-preserving
functor F : Aop → Set is the same thing as a contravariant functor that maps coproducts of A to productsof Set. Every functor of the form y(A) = Hom(−, A) is product-preserving in this sense, because wehave Hom(B + C, A) ∼= Hom(B, A) × Hom(C, A) for all B,C ∈ A. Therefore, the image of the Yoneda
op
op
embedding y : A → SetA is entirely contained in the subcategory [SetA ]× . The Lambek embeddingopy : A → [SetA ]× is defined to be the restriction of y to this codomain, i.e., the unique functor making
the following diagram commute.
Ayop[SetA ]×

y
i

op

SetA

We can show that the Lambek embedding preserves all coproducts that exist in A. For example, if A + B
op
is a coproduct in A, by the Yoneda lemma, for any G ∈ [SetA ]× , we have
op

[SetA ]× (y(A + B), G) =
∼
=
∼
=
∼
=∗
∼
=
∼
=
∼
=

op

[SetA ]× (Hom(−, A + B), G)
op
SetA (Hom(−, A + B), G)
G(A + B)
G(A) × G(B)op
op
SetA (Hom(−, A), G) × SetA (Hom(−, B), G)
op
op[SetA ]× (Hom(−, A), G) × [SetA ]× (Hom(−, B), G)
op[SetA ]× (y(A) + y(B), G),

and therefore y(A + B) ∼= y(A) + y(B). Note that the step marked “*” uses the assumption that G is
product-preserving.

P. Fu, K. Kishida, N. J. Ross, P. Selinger

3
op

Like the category of presheaves, the full subcategory [SetA ]× has many desirable properties. It iscomplete and cocomplete, and it is monoidal closed if A is monoidal [2]. The proofs of these properties
op
op
rely on the fact that [SetA ]× is a reflective subcategory of SetA , i.e., there is an adjunction L ⊣ i :op
op[SetA ]× → SetA . The existence of the left adjoint functor L is not at all obvious. For example,
Kennison’s original proof [6] uses Freyd’s adjoint functor theorem [3], which requires a solution set
condition and the axiom of choice.
op
op
In this paper, we give an explicit construction of the left adjoint functor L : SetA → [SetA ]× . The
methods of this paper are probably already familiar to researchers who specialize in categorical algebra.
However, we believe that outside this immediate field, the connection between presheaves and multisorted type theories is perhaps not as well-known as it should be, and that an explicit description, suchas the one we give here, will be beneficial.
The paper is organized as follows. In Section 2, we briefly review some concepts from multi-sorted
algebras. In Section 3, we show that there is a one-to-one correspondence between presheaves andcertain multi-sorted algebras. In Section 4, we consider multi-sorted algebras corresponding to productpreserving functors. In Section 5, we define a functor L by constructing a multi-sorted term algebra, andwe show that L is the left adjoint of the inclusion functor i. In Section 6, we sketch how to extend our
method to limit-preserving functors.

2

Background on multi-sorted algebras

The definition of a multi-sorted algebra starts by assuming we are given a collection of sorts, usuallydenoted A, B,C, etc. An arity is an (n + 1)-tuple of sorts. A signature is a set of function symbols,
together with an assignment of an arity to each function symbol. We usually write f : A1 , . . . , An → B
to indicate that the function symbol f has arity ⟨A1 , . . . , An , B⟩. When the sorts A1 , . . . , An , B are notimportant, we also sometimes say that f is an n-ary function. In case n = 0, if c is a function symbol ofarity ⟨B⟩, we also write c : B and call c a constant symbol of sort B.
Definition 2.1. Let Σ be a signature. A Σ-algebra T consists of the following data:• For each sort A, a set T (A). The sets T (A) are called the carriers of the algebra.
• For each function symbol f : A1 , . . . , An → B in Σ, a function T ( f ) : T (A1 ) × . . . × T (An ) →T (B).
Definition 2.2. Let A , B be Σ-algebras. A Σ-homomorphism ϕ : A → B consists of:• A function ϕA : A (A) → B(A) for each sort A, such that• for each function symbol f : A1 , . . . , An → B ∈ Σ and all ai ∈ A (Ai ), we haveϕB (A ( f )(a1 , . . . , an )) = B( f )(ϕA1 (a1 ), . . . , ϕAn (an )).
One example of a Σ-algebra is a term algebra. We first define well-sorted terms. For each sort A, we
assume that we are given a countable set XA of variables. We further assume that these sets of variables
are pairwise disjoint, i.e., XA ∩ XB = 0/ when A ̸= B. The set of Σ-terms is freely generated from variables
and function symbols, in the obvious sort-respecting way.
Definition 2.3. The set of Σ-terms of sort A is defined inductively as follows. We write Σ ⊢ t : A to meanthat t is a Σ-term of sort A.
x ∈ XA
Σ⊢x:A

f : A1 , . . . , An → B ∈ ΣΣ ⊢ t1 : A1
Σ ⊢ f (t1 , . . . ,tn ) : B.

...

Σ ⊢ tn : A n

4

On the Lambek embedding and the category of product-preserving presheaves

We say a term is closed if it contains no variables. An equation over a signature Σ is a triple ⟨s,t, A⟩,
where s,t are Σ-terms of sort A. We usually write an equation as s ≈ t : A. If E is a set of equations, wewrite E ⊢ s ≈ t : A to mean that the equation s ≈ t : A follows from the equations in E.
Definition 2.4. The relation E ⊢ s ≈ t : A is inductively defined by the following rules.
(s ≈ t : A) ∈ E(ax)
E ⊢s≈t :AΣ ⊢ s : A (refl)E ⊢s≈s:Ax ∈ XA Σ ⊢ r : A E ⊢ s ≈ t : B(subst)E ⊢ s[r/x] ≈ t[r/x] : B

E ⊢ t ≈ s : B (symm)
E ⊢s≈t :B

E ⊢ r ≈ s : B E ⊢ s ≈ t : B (trans)
E ⊢r≈t :B

E ⊢ si ≈ ti : Ai for all if : A1 , . . . , An → B(cong)
E ⊢ f (s1 , . . . , sn ) ≈ f (t1 , . . . ,tn ) : B
In the rule (subst), s[r/x] denotes the term obtained from s by replacing all occurrences of the variable
x by the term r. This rule ensures that variables are generic, i.e., if an equation holds for a variable, thenit holds for any term.
Definition 2.5. Given a signature Σ, the open term algebra T = Term(Σ) is defined as follows: T (A)is the set of Σ-terms of sort A, and for each function symbol f : A1 , . . . , An → B in Σ, the function
T ( f ) : T (A1 ) × . . . × T (An ) → T (B) is defined by T ( f )(t1 , . . . ,tn ) = f (t1 , . . . ,tn ). The closed term
algebra Term0 (Σ) is defined similarly, except that the carriers consist only of closed terms.
If we are also given a set of equations E, we can define the open and closed quotient term algebras
Term(Σ)/E and Term0 (Σ)/E, which are defined in the same way except that the carriers consist of≈-equivalence classes of (open or closed) terms. The (cong) rule ensures that the function T ( f ) is
well-defined on such equivalence classes.
Definition 2.6. We say that a Σ-algebra T satisfies an equation s ≈ t : A, or equivalently, that the equation
is valid in T , if for any Σ-homomorphism ϕ : Term(Σ) → T , we have ϕA (s) = ϕA (t). If E is a set of
equations, we say that T satisfies E if it satisfies all the equations in E. If T is a Σ-algebra satisfying a
set of equations E, we also say that T is a (Σ, E)-algebra.
By a multi-sorted theory, we mean all of the above data, i.e., a collection of sorts, a signature, and aset of equations. Note that Term(Σ) and Term0 (Σ) are Σ-algebras and Term(Σ)/E and Term0 (Σ)/E are(Σ, E)-algebras.

3

The theory associated to a category A

In the rest of this paper, we will work with a small category A. For convenience and without loss ofopgenerality, we will work with the functor category SetA rather than SetA unless otherwise noted.
Definition 3.1. To the category A, we associate a multi-sorted theory as follows. The sorts are the objectsof A. The signature ΣA contains a unary function symbol f : A → B for every morphism f : A → B in A.
The set of equations EA consists of the following:(id)
id(x) ≈ x : A, whenever id : A → A is an identity morphism and x is a variable of sort A.
(comp) ( f ◦ g)(x) ≈ f (g(x)) : C, whenever f : A → B and g : B → C are morphisms and x is a variableof sort A.
Remark 3.2. There is a one-to-one correspondence between (ΣA , EA )-algebras and functors T : A →Set. Indeed, if T : A → Set is functor, then T is a ΣA -algebra because for each A ∈ A, there is a set
T (A). For each function symbol f : A → B in A, since f is also a morphism of A, there is a function
T ( f ) : T (A) → T (B). The equations (id) and (comp) are satisfied by functoriality. Conversely, every(ΣA , EA )-algebra gives rise to a functor, and the two assignments are mutually inverse.

P. Fu, K. Kishida, N. J. Ross, P. Selinger

4

5

Product-preserving functors

Recall from the introduction that we are interested in taking a functor F : A → Set, and constructing
another functor L(F) : A → Set that is product-preserving. Rather than requiring L(F) to necessarily
preserve all products, we will consider the slightly more general problem of preserving some distinguished class of products. Therefore, we will assume that we are given a small category A and someparticular collection C of product cones in A. We say that a functor is C -product-preserving when it
preserves all of the product cones in C .
On one extreme, we may of course assume that A has all products, and that C is the set of all productcones in A. In that case, a C -product-preserving functor is just the same thing as a product-preserving
functor in the ordinary sense. On the other extreme, C could just consist of a single product coneA ← A × B → B, in which case a functor is C -product-preserving if it preserves just that one product.
For simplicity and ease of exposition, we will assume in the following that C is a collection of binary
product cones. However, the same construction works for n-ary products for any finite n. It also works
for infinite products, assuming that we extend the notion of term algebras to allow terms of infinite arity(which causes no problems). Product cones for n = 0, i.e., terminal objects, are of course also a specialcase.
We first define a theory of product-preserving functors.
Definition 4.1. To a small category A with a distinguished collection C of (binary) product cones, weassociate a multi-sorted theory as follows. The signature ΣC has the same function symbols as ΣA , andfst
snd
additionally, for each product cone A ←− C −−→ B in C , we add a function symbol
pair : A, B → C.
Note that there are already function symbols for all the morphisms of A, including fst : C → A andsnd : C → B. The set of equations EC has the same equations as EA , and additionally, for each productfst
snd
cone A ←− C −−→ B in C , we add the following three equations:(fst)

fst(pair(x, y)) ≈ x : A, whenever x and y are variables of sorts A and B, respectively.

(snd)

snd(pair(x, y)) ≈ y : A, whenever x and y are variables of sorts A and B, respectively.

(pair)

pair(fst(z), snd(z)) ≈ z : C, whenever z is a variable of sort C.

We then have:
Remark 4.2. There is a one-to-one correspondence between (ΣC , EC )-algebras and C -product-preserving functors F : A → Set. The proof is basically the same as that of Remark 3.2. The point is that
F(fst)

the equations (fst), (snd), and (pair) are exactly what is required to ensure that the cone F(A) ←−−−
F(snd)

F(C) −−−−→ F(B) is a product cone in Set.

5

The construction of the functor L

Given a small category A with a distinguished collection C of product cones as in the previous section,
we write [SetA ]C for the full subcategory of SetA consisting of C -product-preserving functors. The
notation [SetA ]× used in the introduction is a special case, where C is the collection of all product cones.
In this section, we will focus on defining the functor L : SetA → [SetA ]C . By Remark 4.2, we knowthat a product-preserving presheaf corresponds to a (ΣC , EC )-algebra. Thus, given any functor F : A →Set, we must construct a (ΣC , EC )-algebra L(F). This can be done freely, as we now show.

6

On the Lambek embedding and the category of product-preserving presheaves

Definition 5.1. To any functor F : A → Set, we associate a multi-sorted theory as follows. The sorts,
signature, and equations are the same as in Definitions 3.1 and 4.1, except for the following:• For each object A ∈ A and each element c ∈ F(A), we add a constant symbol c : A to the signature.
• For each morphism f : A → B ∈ A and each c ∈ F(A), let d = F( f )(c). We add an equationd ≈ f (c) : B.
We write the resulting signature and equation as ΣF and EF , respectively.
The quotient term algebra Term0 (ΣF )/EF still satisfies the equations (id), (comp), (fst), (snd), and(pair), and therefore, by Remark 3.2, it is a product-preserving functor. Hence we define the functor
L : SetA → [SetA ]C to be the following.
Definition 5.2. We define the functor L : SetA → [SetA ]C by
L(F) = Term0 (ΣF )/EF .
We note that L is a well-defined functor, because for every natural transformation α : F → G ∈ SetA ,we have a ΣC -homomorphism L(α) : Term0 (ΣF )/EF → Term0 (ΣG )/EG . This homomorphism is definedinductively on the structure of the terms in Term0 (ΣF )/EF , using α for the constant symbols. In otherwords, we have L(α)( f (t1 , . . . ,tn )) = f (L(α)(t1 ), . . . , L(α)(tn )), where f is any function symbol fromΣC , and L(α)(c) = α(c), where c is one of the constant symbols introduced in Definition 5.1.
Theorem 5.3. We have an adjunction L ⊣ i, where i : SetA → [SetA ]C is the inclusion functor.
Proof. First we will define, for any F : A → Set, a natural transformation ηF : F → iL(F), i.e., ηF : F →Term0 (ΣF )/EF . For any A ∈ A and a ∈ F(A), we define ηF,A (a) = a. Note that ηF is natural in A because
for any f : A → B ∈ A and a ∈ F(A), we have
(Term0 (ΣF )/EF )( f )(ηF,A (a)) = f (a) ≈ b = ηF,B (F( f )(a)),
where b = F( f )(a). Moreover, η is natural in F because for any αA : F(A) → G(A) and a ∈ F(A), we
have(Lα)A (ηF,A (a)) = (Lα)A (a) = αA (a) = ηG,A (αA (a)).
Next, we will show that for any natural transformation γ : F → i(G), there exists a unique naturaltransformation γ̂ : L(F) → G such that γ̂ ◦ ηF = γ. For all A ∈ A, we define γ̂A : (Term0 (ΣF )/EF )(A) →G(A) by induction on the structure of the terms in (Term0 (ΣF )/EF )(A).
• γ̂A (a) = γA (a) for any a ∈ F(A).
• γ̂B ( f (t)) = G( f )(γ̂A (t)) for any f : A → B ∈ A, ΣF ⊢ t : A.
• γ̂C (pair(s,t)) = G(pair)(γ̂A (s), γ̂B (t)) for any cone A ← C → B in C , ΣF ⊢ s : A, and ΣF ⊢ t : B.
We must show that γ̂A : (Term0 (ΣF )/EF )(A) → G(A) is a well-defined function for all A ∈ A. We canshow this by induction on EF ⊢ s ≈ t : B.
• CaseΣF ⊢ a : A b = F( f )(a) f : A → B ∈ A
EF ⊢ b ≈ f (a) : B.
In this case, we have(∗)γ̂B (b) = γB (b) = γB (F( f )(a)) = G( f )(γA (a)) = γ̂B ( f (a)).
The equality (∗) is by naturality of γ.

P. Fu, K. Kishida, N. J. Ross, P. Selinger• Case7ΣF ⊢ s : A ΣF ⊢ t : B
EF ⊢ fst(pair(s,t)) ≈ s : A.

We need to show γ̂B (fst(pair(s,t))) = G(fst)(G(pair)(γ̂A (s), γ̂B (t))) = γ̂A (s). This equality holds
because G is a product-preserving functor.
• CaseΣF ⊢ s : C
EF ⊢ pair(fst(s), snd(s)) ≈ s : C.

We need to show γ̂C (pair(fst(s), snd(s))) = G(pair)(G(fst)(γ̂C (s)), G(snd)(γ̂C (s))) = γ̂C (s). Thisequality holds because G is a product-preserving functor.
• CaseEF ⊢ s1 ≈ t1 : A1 . . . EF ⊢ sn ≈ tn : An
EF ⊢ f (s1 , . . . , sn ) ≈ f (t1 , . . . ,tn ) : B.

We have(∗)γ̂B ( f (s1 , . . . , sn )) = G( f )(γ̂A1 (s1 ), . . . , γ̂An (sn )) = G( f )(γ̂A1 (t1 ), . . . , γ̂An (tn )) = γ̂B ( f (t1 , . . . ,tn )),where the equality (∗) uses the induction hypothesis.
• All the other cases are proved similarly.
Now we show that γ̂ is a natural transformation. Suppose f : A → B ∈ A. We need to showG( f )(γ̂A (t)) = γ̂B ((Term0 (ΣF )/EF )( f )(t)).
This is true because by the definition of γ̂, we haveγ̂B ((Term0 (ΣF )/EF )( f )(t)) = γ̂B ( f (t)) = G( f )(γ̂A (t))
for any ΣF ⊢ t : A.
It is obvious to verify that γ̂ ◦ η = γ.
Lastly, we must show that γ̂ is unique. Consider a natural transformation γ̂ ′ such that γ̂ ′ ◦ η = γ. We
must show γ̂ ′A (t) = γ̂A (t) for all ΣF ⊢ t : A. This can be shown by induction on ΣF ⊢ t : A.
• Casea ∈ F(A)ΣF ⊢ a : A.
In this case, we have γ̂ ′A (a) = γ̂ ′A (ηF,A (a)) = γA (a) = γ̂A (a).
• CaseΣF ⊢ s : A ΣF ⊢ t : B
ΣF ⊢ pair(s,t) : C.

By induction hypothesis, we have γ̂ ′A (s) = γ̂A (s) and γ̂ ′B (t) = γ̂B (t). We need to showγ̂ ′A×B (pair(s,t)) = γ̂A×B (pair(s,t)) = G(pair)(γ̂A (s), γ̂B (t)) = G(pair)(γ̂ ′A (s), γ̂ ′B (t)).
This is the case because by the naturality of γ̂ ′ , we haveG(fst)(γ̂ C′ (pair(s,t))) = γ̂ ′A (fst(pair(s,t)))) = γ̂ ′A (s)andG(snd)(γ̂ C′ (pair(s,t))) = γ̂ ′B (t).
This shows that γ̂ C′ (pair(s,t)) is indeed the pair G(pair)(γ̂ ′A (s), γ̂ ′B (t)).

8On the Lambek embedding and the category of product-preserving presheaves• CaseΣF ⊢ t : A f : A → B
ΣF ⊢ f (t) : B.

By naturality of γ̂ ′ , γ̂ and the induction hypothesis, we haveγ̂ ′B ( f (t)) = G( f )(γ̂ ′A (t)) = G( f )(γ̂A (t)) = γ̂B ( f (t)).
opRemark 5.4. In the introduction, we showed that the Lambek embedding y : A → [SetA ]× preserves all
op
op
coproducts, where [SetA ]× is the subcategory of SetA consisting of product-preserving functors. This
result can easily be relativized, without changing the proof, to the case of a chosen collection of cones.
Namely, if C is a collection of product cones in Aop (or, equivalently, coproduct cones in A), then theop
Lambek embedding y : A → [SetA ]C preserves all of the coproduct cones in C . Thus, the construction
can be customized to preserve coproducts “of interest”.

6

The subcategory of limit-preserving presheaves

Our method of showing that the subcategory of C -product-preserving functors is reflective can also be
adapted to functors that preserve a given class of limits (not necessarily products). A small complicationis that, in Freyd’s terminology, the notion of general limits is not algebraic but only essentially algebraic[4]. This means that the domain of some operations is defined in terms of equations. In the following, we
sketch the proof in the case of equalizers, but the same method works for other kinds of limits as well.
Definition 6.1. Consider a small category A with a distinguished collection C of limits (we focus onequalizers for simplicity). To this, we associate a multi-sorted theory as follows. The signature ΣC hasef ,g

the same function symbols as ΣA , and additionally, for each equalizer E → A ⇒ B in C , we add a function
symboleql : A → E.
Its term formation rule is slightly different than that of other function symbols (and for this reason, theresulting theory is not strictly speaking a multi-sorted algebraic theory in the sense of Section 2, butrather what should be called a multi-sorted essentially algebraic theory):ΣC ⊢ t : A

f , g : A → B EC ⊢ f (t) ≈ g(t) : B
ΣC ⊢ eql(t) : Eef ,gThe set of equations EC has the same equations as EA , and additionally, for each equalizer E → A ⇒ B
in C , we add the following two equations:(beta)e(eql(t)) ≈ t : A, whenever ΣC ⊢ t : A and EC ⊢ f (t) ≈ g(t) : B.

(eta)

x ≈ eql(e(x)) : E, whenever x is a variable of sort E.

Note that Definition 6.1 introduces an apparent circularity, because unlike Definition 3.1 and 4.1, thewell-sortedness judgement ΣC ⊢ t : E and the set of equations EC are now defined in terms of each other.
Of course this is not an actual circularity; it just means that these two items are defined by simultaneous
induction. Similarly, the notion of a (ΣC , EC )-algebras must be adjusted so that T (eql) : T (A) → T (E)is a partial function that is defined and satisfies T (e)(T (eql)(x)) = x for those elements x ∈ T (A)satisfying T ( f )(x) = T (g)(x). With these adjustments, we have the following:P. Fu, K. Kishida, N. J. Ross, P. Selinger

9Remark 6.2. Similarly to Remark 4.2, we can show that there is a one-to-one correspondence between(ΣC , EC )-algebras and C -limit-preserving functors F : A → Set. The equations (beta) and (eta) ensure
that
F(e)

F(E) → F(A)F( f ),F(g)

⇒

F(B)

is an equalizer in Set. To show that the full subcategory [SetA ]C of C -limit-preserving functors is reflective, we first define the functor L : SetA → [SetA ]C , similarly to Definition 5.2. Then we can show that L
is a left adjoint of the inclusion functor, by adapting the proof of Theorem 5.3.

7

Conclusion

We gave a brief introduction to the Lambek embedding, a version of the Yoneda embedding that preservescoproducts (or more generally, a chosen class of distinguished coproducts or colimits). The Lambek embedding is obtained by restricting the codomain of the Yoneda embedding to a suitable full subcategory
opof SetA , namely, the full subcategory of product-preserving functors (or more generally, functors thatoppreserve the distinguished class of products or limits). This is a reflective subcategory of SetA . Like
op
SetA itself, this subcategory is complete and cocomplete, as well as monoidal closed provided that A
is monoidal. Our method uses concepts from multi-sorted algebras. In particular, we observed that there
is a one-to-one correspondence between product-preserving functors and certain multi-sorted algebras.
We gave a direct syntactic construction of the functor L and proved that it is left adjoint to the inclusion
functor.

Acknowledgements
This work was supported by the Natural Sciences and Engineering Research Council of Canada (NSERC)
and by the Air Force Office of Scientific Research under Award No. FA9550-21-1-0041.

References[1] Brian Day (1970): On closed categories of functors. In: Reports of the Midwest Category Seminar IV,
Springer Lecture Notes in Mathematics 137, pp. 1–38, doi:10.1007/BFb0060438.
[2] Brian Day (1972): A reflection theorem for closed categories. Journal of Pure and Applied Algebra 2(1), pp.
1–11, doi:10.1016/0022-4049(72)90021-7.
[3] Peter J. Freyd (1964): Abelian categories. Harper & Row New York.
[4] Peter J. Freyd (1972): Aspects of topoi. Bulletin of the Australian Mathematical Society 7(1), pp. 1–76,
doi:10.1017/S0004972700044828.
[5] Peng Fu, Kohei Kishida, Neil J. Ross & Peter Selinger (2022): A biset-enriched categorical model for ProtoQuipper with dynamic lifting. Preprint available from arXiv:2204.13039.
[6] J. F. Kennison (1968): On limit-preserving functors. Illinois Journal of Mathematics 12(4), pp. 616–619,
doi:10.1215/ijm/1256053963.
[7] Joachim Lambek (1966): Completions of categories: Seminar lectures given 1966 in Zürich. Lecture Notes inMathematics 24, Springer, doi:10.1007/BFb0077265.
[8] Octavio Malherbe (2013): Categorical Models of Computation: Partially Traced Categories and Presheaf
Models of Quantum Computation. Ph.D. thesis, University of Ottawa, Department of Mathematics and Statistics. Available from arXiv:1301.5087.

10

On the Lambek embedding and the category of product-preserving presheaves[9] Francisco Rios & Peter Selinger (2018): A categorical model for a quantum circuit description language.
Extended Abstract. In: Proceedings of the 14th International Conference on Quantum Physics and Logic,
QPL 2017, Nijmegen, Electronic Proceedings in Theoretical Computer Science 266, pp. 164–178, doi:10.
4204/EPTCS.266.11.