A Characterisation of Lambda Definability with Sums
via ⊤⊤-Closure Operators
Shin-ya Katsumata
Research Institute for Mathematical Sciences, Kyoto University
Kyoto, 606-8502, Japan sinya@kurims.kyoto-u.ac.jp

Abstract. We give a new characterisation of morphisms that are definable by theinterpretation of the simply typed lambda calculus with sums in any bi-Cartesianclosed category. The ⊤⊤-closure operator will be used to construct the category
in which the collection of definable morphisms at sum types can be characterised
as the coproducts of such collections at lower types.

1 Introduction
The λ-definability problem is to characterise the semantic elements that are definable bydenotational / categorical semantics of the simply typed λ-calculus. A characterisationof the λ-definable elements in full type hierarchies was first given by Plotkin using
Kripke logical relations. This result was later generalized by Jung and Tiuryn to any
Henkin model using Kripke logical predicates with varying arity [15]; its categoricalformulation was also given by Alimohamed [1].
These precursors considered the definability problem in the simply typed lambda
calculus with only arrow types (and possibly product types). The problem becomes
more subtle when sum types are added. There is a natural definition of coproducts for
Kripke predicates with varying arity, but these coproducts are not sufficient to characterise the definable elements at sum types. In [11] Fiore and Simpson overcome thisdifficulty by introducing a new concept called Grothendieck logical predicates. They
used Grothendieck topology to improve the definition of coproducts of Kripke predicates. By constructing a suitable category of worlds and topology on it, Fiore andSimpson succeeded in giving a characterisation of definable morphisms in any bi-CCC
with stable coproducts.
In this paper we approach the definability problem in the simply typed lambda calculus with sums using a different technique called ⊤⊤-closure operator. The main contribution of this paper is the following:
1. We characterise the definability predicate (=the collection of definable morphisms)
at sum types by means of the standard coproducts for Kripke predicates and thesemantic ⊤⊤-closure operator:
Def 0 = 0̇⊤⊤ ,Def(τ + τ′ ) = (Def τ +̇ Def τ′ )⊤⊤ .

This characterisation holds with respect to the interpretation of the lambda calculus
with sums in any bi-CCC. We also give a characterisation of morphisms definable

by the simply typed lambda calculus with sums by means of weak logical predicates.
2. We analyse the underlying categorical essence of the above arguments, and present
it as the restriction theorem. The statement of the theorem is the following: let P be
a logical predicate in a sufficiently rich fibration p : P → C. If P respects productand arrow types, then we can restrict P to a full reflective subcategory P⊤⊤ of P sothat P respects sum types as well.
The characterisation stated in item 1 implies that in the category K⊤⊤ of ⊤⊤-closed
objects the definability predicates at sum types are given by the coproducts of the definability predicates at lower types. By employing K⊤⊤ as a gluing category, we also showthat the inclusion from the free distributive category L0 (B) over the set B of base types
to the free bi-CCC L1 (B) over B is full. We note that this result is proved in [10], butthere a different gluing category is employed.
Preliminary We define categories and functors by the following table:
A category / functor is ...
when it has / preserves ...
Cartesian
finite products
co-Cartesianfinite coproductsbi-Cartesianfinite products and finite coproducts
Cartesian closed (CC)finite products and exponentials
bi-Cartesian closed (bi-CC) finite products, finite coproducts and exponentials

2 Definability of Calculi with Sums
We deal with the definability problem in the context of functorial semantics, wheresyntatic theories are treated as freely generated categories, and interpretations are represented by structure-preserving functors. We fix a small Cartesian category L that plays
the role of a syntactic theory, a bi-CCC C that plays the role of a semantic domain, anda strict Cartesian functor F:
F// C
Lthat gives an interpretation of the syntactic theory. We first review some basic propertiesof the definability predicate for F in this setting, then extend L and F with additional
structures (coproducts / exponentials) toward the main theorems of this paper. At thismoment we do not require that L is a freely generated category, as the freeness does notplay any role in the following discussion.
2.1 Kripke Predicates with Varying Arity
We first introduce the poset CtxL that plays the role of Kripke structure for Kripke
predicates with varying arity. The carrier of the poset is (Obj(L))∗ , the set of finite
sequences of L-objects, and these sequences are ordered by the prefix ordering (that is,τ ≤ σ if τ is a prefix of σ). Below we treat CtxL as a category.

When L is identified as a syntactic (type) theory, the poset CtxL expresses inclusionsof typing contexts. We associate these inclusions with projections in L by the following
functor | − | : CtxL → Lop :m|τ1 · · · τn | = (· · · ((1 × τ1 ) × τ2 ) · · · ) × τn ,z }| {|τ1 · · · τn ≤ τ1 · · · τn+m | = id ◦π ◦ · · · ◦ π,

where π is the first projection for appropriate objects.
We next define the category KF of Kripke predicates with varying arity.
– An object of KF is a pair (C, X) where C is a C-object and X is a subpresheaf of thecontravariant presehaf C(F| − |, C) on CtxL .
– A morphism from (C, X) to (D, Y) is a C-morphism f : C → D such that for any
CtxL -object Γ and C-morphism g ∈ XΓ, we have f ◦ g ∈ YΓ.
The category KF is constructed as follows. Let
HF : C → [CtxL , Set] be a functor defined by
HF (C) = C(F| − |, C). Then KF is the vertex of
the change-of-base (pullback) of the subobject fibration p : Sub([CtxL , Set]) → [CtxL , Set] along
HF (Figure 1). This construction is an instance ofsubscone [22] or categorical gluing [1].

KFr// Sub([CtxL , Set])
p

q


C

Proposition 1. The leg q : KF → C of the changeof-base (Figure 1) is a strict bi-CC functor and apartial order fibration with fibred small products.



HF// [CtxL , Set]

Fig. 1. Derivation of q

Proof. Since p is a partial order fibration with fibred small products, q inherits these structures via
the change-of-base along the Cartesian functor HF . The bi-CC structure of KF , whichis strictly preserved by q, is given as follows (see also Section 1.5, [1]):1̇ = (1, {!F|Γ| }Γ )(C, X) ×˙ (D, Y) = (C × D, {h | π1 ◦ h ∈ XΓ, π2 ◦ h ∈ YΓ}Γ )0̇ = (0, ∅)(C, X) +̇ (D, Y) = (C + D, ({inl ◦ f | f ∈ XΓ} ∪ {inr ◦ f | f ∈ YΓ})Γ )˙ (D, Y) = (C ⇒ D, { f | ∀Γ ′ ≥ Γ . ∀x ∈ XΓ ′ . ev ◦ h f ◦ F|Γ ≤ Γ ′ |, xi ∈ YΓ ′ }Γ ).
(C, X) ⇒(here {· · · }Γ denotes a presheaf described by an auxiliary parameter Γ ∈ CtxL ).
We define the target of our study, the definability functor Def : L → KF , byDef τ = (τ, {Fg ∈ C(F|Γ|, Fτ) | g ∈ L(|Γ|, τ)}Γ )Def f = F f.
We call Def τ the definability predicate (of F) at τ. We refer to the presheaf part ofDef τ by Dτ; in other words, D = r ◦ Def (r is the other leg of the change-of-base).
Proposition 2. Def : L → KF is a full strict Cartesian functor, and q ◦ Def = F.

Def
// KF
···
MMM
MMM
q
MM&&  (Figure 1)
F

L MM

C

···

˙ 0̇, +̇, ⇒)˙
KF bi-CCC (1̇, ×,
C bi-CCC (1, ×, 0, +, ⇒)q strict bi-CC functor and partial orderfibration with fibered small products
L small Cartesian category
F strict Cartesian functor
Def full strict Cartesian functor

Fig. 2. Categories and Functors for the Argument of Definability

Figure 2 summarises categories and functors we have introduced so far.
One important property of the functor Def, which is implicit in the characterisationof λ-definability by Jung and Tiuryn [15], is the following:
Lemma 1. For any L-objects τ, τ′ and CtxL -object Γ, we have˙ Def τ′ )(Γ) ⇐⇒ λ−1 ( f ) ∈ Dτ′ (Γτ),
f ∈ r(Def τ ⇒(here λ−1 denotes the uncurrying operator).
2.2 A Characterisation of Definability with Sums
We next assume that the category L in Figure 2 is a distributive category (in the sense of
Walters [26, 7]) and F is a strict bi-Cartesian functor. Recall that a distributive category
C is a bi-Cartesian category such that the canonical morphism[A × inl, A × inr] : (A × B) + (A × C) → A × (B + C)
has the inverse (called distributive law) 1 :mCA,B,C : A × (B + C) → (A × B) + (A × C).
LC
We note that F strictly preserves distributive laws, that is, F(mτ,τ′ ,ρ ) = mFτ,Fτ′ ,Fρ .
The functor Def in Figure 2 is still full strict Cartesian from Proposition 2, but not
co-Cartesian. We merely have the following inequations:

Def 0 ≥ 0̇,

Def(τ + τ′ ) ≥ Def τ +̇ Def τ′ .

(1)

Interestingly, these inequations are equated when applied to the contravariant functor
˙ Def ρ).
(− ⇒Lemma 2. For any L-objects τ, τ′ , ρ, we have˙ Def ρ = 0̇ ⇒˙ Def ρDef 0 ⇒′ ˙
˙ Def ρ.
Def(τ + τ ) ⇒ Def ρ = (Def τ +̇ Def τ′ ) ⇒1

The distributive law implies that the unique map 0 → A × 0 is the isomorphism; see [7].

Proof. We leave the proof of the first equation to the reader. We show the second equation. Let τ, τ′ , ρ be L-objects. The inequation (1) implies half of the equation to be
proved. We therefore show the other half displayed below:
˙ Def ρ ≥ (Def τ +̇ Def τ′ ) ⇒˙ Def ρ.
Def(τ + τ′ ) ⇒˙ Def ρ)(Γ). The isomorphism
Let Γ be a CtxL -object and f ∈ r((Def τ +̇ Def τ′ ) ⇒˙ Def ρ  (Def τ ⇒˙ Def ρ) ×˙ (Def τ′ ⇒˙ Def ρ)(Def τ +̇ Def τ′ ) ⇒˙ Def ρ)(Γ) and λ(ev ◦ f × inr) ∈ r(Def τ′ ⇒˙implies that λ(ev ◦ ( f × inl)) ∈ r(Def τ ⇒Def ρ)(Γ). From Lemma 1, we obtain(g1 =) ev ◦ ( f × inl) ∈ Dρ(Γτ),(g2 =) ev ◦ ( f × inr) ∈ Dρ(Γτ′ ).

We thus take L-morphisms h1 : |Γτ| → ρ and h2 : |Γτ′ | → ρ such that g1 = Fh1 andg2 = Fh2 . Since F is a strict bi-Cartesian functor, we haveL
[g1 , g2 ] ◦ mCF|Γ|,Fτ,Fτ′ = F([h1 , h2 ] ◦ m|Γ|,τ,τ′ ).

The left hand side is equal to ev ◦ ( f × (Fτ + Fτ′ )):[g1 , g2 ] ◦ m = ev ◦ ( f × (Fτ + Fτ′ )) ◦ [F|Γ| × inl, F|Γ| × inr] ◦ m= ev ◦ ( f × (Fτ + Fτ′ )).
Hence ev ◦ ( f × (Fτ + Fτ′ )) ∈ Dρ(Γ(τ + τ′ )). From Lemma 1, we obtain f ∈ r(Def(τ +˙ Def ρ)(Γ).
τ′ ) ⇒
We combine this lemma and the semantic⊤⊤-closure operator [16] to extract KF ’s full reflective sub bi-CCC whose coproducts can char⊤⊤acterise the definability predicates at sum types.
88 KF _′The semantic ⊤⊤-closure operator (we may dropDef
ι
the word “semantic” thereafter) is a semantic

/
/
···
KF
L NNN Def
analogue of Pitt’s ⊤⊤-closure technique in [25],NNNand is an instance of the author’s semantic ⊤⊤NNNq
NN''  (Figure 1)
Flifting [16]. The ⊤⊤-closure operator in this sec···Ction is specialised to the argument of definability. In Section 3 it will be re-introduced in moregeneral form, together with the proofs of propo- Fig. 3. Restriction of Definability
sitions and theorems in this section.
FunctorThe ⊤⊤-closure operator is defined as follows. Let X be a KF -object above a C-object I.
For each L-object ρ, we define X ⊤⊤(ρ) to be the vertex of the following inverse image inthe fibration q : KF → C:
X ⊤⊤(ρ)// (X ⇒
˙ Def ρ) ⇒˙ Def ρKF// (I ⇒ Fρ) ⇒ Fρ


C

q

I

′
ηFρ
I =λ(ev◦hπ ,πi)⊤⊤where ηFρ, the ⊤⊤-closure
I is the unit of the continuation monad. We then define X
of X by^X ⊤⊤ =X ⊤⊤(ρ) .
ρ∈Obj(L)Proposition 3. The assignment X 7→ X ⊤⊤ extends to a monad over KF whose unit andmultiplication are vertical (c.f. Proposition 7).
Below we call the assignment (semantic) ⊤⊤-closure operator. It indeed gives an idempotent closure operator at every fibre, as unit and multiplication are vertical.
Corollary 1. We have X ≤ X ⊤⊤ and (X ⊤⊤ )⊤⊤ = X ⊤⊤ , and the monad is idempotent (c.f.
Corollary 2).
We then consider KF ’s full reflective subcategory K⊤⊤
F consisting of ⊤⊤-closed objects(that is, objects X such that X ⊤⊤ = X); see Figure 3. Some calculation shows that ⊤⊤closed objects form an exponential ideal. Therefore we obtain the following:
Proposition 4. The category K⊤⊤
F is a bi-CCC and q ◦ ι is a strict bi-CC functor (c.f.
Theorem 4).
The CC structure in K⊤⊤
F is inherited from KF , while the co-Cartesian structure is given
by 0̇⊤⊤ and (X +̇ Y)⊤⊤ . That the ⊤⊤-closure operator is defined in terms of the definability predicates themselves implies the following important property:
Proposition 5. For every L-object ρ, Def ρ is ⊤⊤-closed (c.f. Proposition 8).
Thus functor Def can be restricted to the full Cartesian functor (Def ′ in Figure 3) toK⊤⊤
F . Furthermore, from Lemma 2 we obtain a characterisation of the definability predicates at sum types (c.f. Theorem 5-2):
Def 0 = (Def 0)⊤⊤ = 0̇⊤⊤′′

Def(τ + τ ) = (Def(τ + τ ))

(2)
⊤⊤

′ ⊤⊤

= (Def τ +̇ Def τ ).

(3)This is equivalent to saying that Def ′ is a strict co-Cartesian functor. To summarise:
Theorem 1 (Restriction Theorem for Definability Functor). In Figure 3, assume
that L is a small distributive category and F is a strict bi-Cartesian functor. Then Def ′is a full strict bi-Cartesian functor.
We next let L be a small bi-CCC and F : L → C be a strict bi-CC functor. Under thissituation, the restriction of the definability functor to K⊤⊤
F becomes a bi-CC functor.
Since any bi-CCC is a distributive category, Def ′ in Figure 3 is full bi-Cartesian fromthe restriction theorem. Moreover, as shown in [1] (c.f. [15]), the functor Def (and Def ′ )strictly preserves exponentials. Therefore we obtain the following theorem:
Theorem 2. In figure 3, assume that L is a small bi-CCC and F is a strict bi-CC functor.
Then Def ′ in Figure 3 is a full strict bi-CC functor.

2.3 Fullness of Free Distributive Categories in Free Bi-CCCs
As an application of the restriction theorem, we show that the canonical inclusion fromthe free distribute category to the free bi-CCC is full. We note that this result (andfaithfulness) is proved in [10] using a different gluing category.
We fix the set B of base types and regard it as a discrete category. In this paper, by
the free distributive category (L0 (B), η0 : B → L0 (B)) over B, we mean the distributive
category with the following universal property: for any distributive category C and afunctor F : B → C, there exists a unique strict bi-Cartesian functor F : L0 (B) → C
such that F ◦ η0 = F. We also define the free bi-CCC (L1 (B), η1 : B → L1 (B)) overB as the one having the similar universal property. Such free categories arise as termcategories of the simply typed (lambda) calculus with sums. We omit the detail of theconstruction of free categories due to lack of space; see e.g. [18].
We instantiate Figure 3 with the following data:
1. L = L0 (B), the free distributive category over B.
2. C = L1 (B), the free bi-CCC over B.
3. F = η1 : L0 (B) → L1 (B), the strict bi-Cartesian functor derived from the universal
property of L0 (B).
Lafont applied categorical gluing to show that any small Cartesian category C can be
fully embedded into the CCC that is relatively free with respect to C [17]. We apply
his proof technique to the show that η1 is full. Here we use K⊤⊤
F as a substitute for thegluing category.
Theorem 3. The strict bi-Cartesian functor η1 : L0 (B) → L1 (B) is full.
Proof. Below we write F for η1 . From Theorem 1 we obtain a full strict bi-Cartesian⊤⊤functor Def ′ : L0 (B) → K⊤⊤
F . From Proposition 4, KF is a bi-CCC; hence we obtain astrict bi-CC functor J = Def ′ ◦η0 : L1 (B) → K⊤⊤
F . Furthermore, q ◦ ι is a strict bi-CCfunctor, so q◦ι◦ J = Id by the universal property of L1 (B). This implies that J is faithful.
L1 (B)
n77
n
J
n

nnn
// K⊤⊤
L0 (B) P Def ′
F
PPP
PPP
PP''  q◦ιF
L1 (B)
F nnn

In the above diagram, the upper half of the triangle commutes from the universal property of L0 (B). The lower half of the triangle also commutes from Figure 3. We now showthat F is full. Let f : Fτ → Fσ be a L1 (B)-morphism. We seek for a L0 (B)-morphism
g such that f = Fg. We first have J f : Def ′ τ → Def ′ σ. Since Def ′ is full, there exists
a L0 (B)-morphism g : τ → σ such that J f = Def ′ g = J(Fg). Since J is faithful, we
obtain f = Fg.

3 ⊤⊤-Closure Operators and the Restriction Theorem
In this section we focus on the general scheme that underlies in the derivation of therestriction theorem (Theorem 1), and re-establish it in more general form.
We first identify the class of fibrations in which we can consider ⊤⊤-closure operators. If a functor U : P → C satisfies the following conditions:˙ 0̇, +̇, ⇒,˙ ˙!, π̇, π̇′ , λ̇, ev,
P bi-CCC (1̇, ×,
˙ ···)
C bi-CCC (1, ×, 0, +, ⇒, !, π, π′, λ, ev, · · · )U strict bi-CC functor and partial orderfibration with fibered small products

P
U


C

we say that U admits ⊤⊤-closure operators. Below we give a sufficient condition for
ensuring that a fibration admits ⊤⊤-closure operators.
Proposition 6. Let p : E → B be a partial order bifibration such that B is a bi-CCC,
p has fibred small products, fibred finite coproducts, fibred exponentials and simple
products (see e.g. Jacobs [14]). Then p admits ⊤⊤-closure operators.
3.1 ⊤⊤-Closure Operators
We fix a fibration U : P → C which admits ⊤⊤-closure operators. Each ⊤⊤-closure
operator takes a P-object as a parameter called closure parameter. Let S be a closure
parameter. For a P-object X, we define X ⊤⊤(S ) to be the vertex of the following inverse
image:// (X ⇒˙ S)⇒
˙ SPX ⊤⊤(S )
U

UX

′
ηUS
UX =λ(ev◦hπ ,πi)C// (UX ⇒ US ) ⇒ US

We note that the C-morphism ηUS
UX is the unit of the continuation monad (− ⇒ US ) ⇒US . This construction exactly coincides with the semantic ⊤⊤-lifting [16] of the identity monad.
Proposition 7. [16] Let S be a closure parameter. The assignment X 7→ X ⊤⊤(S ) extends to an endofunctor (−)⊤⊤(S ) : P → P such that U ◦ (−)⊤⊤(S ) = U. Furthermore,
there exists vertical natural transformations η⊤⊤(S ) and µ⊤⊤(S ) that make the triple((−)⊤⊤(S ) , η⊤⊤(S ) , µ⊤⊤(S ) ) a monad.
Corollary 2. Let S be a closure parameter. For any P-object X, we have
X ≤ X ⊤⊤(S ) ,(X ⊤⊤(S ) )⊤⊤(S ) = X ⊤⊤(S ) ,S = S ⊤⊤(S ) .

Proof. In this proof we simply write ⊤⊤ for ⊤⊤(S ). The first two (in)equations are
immediate consequences of the previous lemma. To show S ⊤⊤ = S , it is sufficient toshow S ⊤⊤ ≤ S . We consider the following diagram:S ⊤⊤// (S ⇒˙ S) ⇒˙ S

US// (US ⇒ US ) ⇒ US

// S

P

// US


C

ev◦hid,˙λ̇(π̇′ )◦˙!i

U
ηUS
US

ev◦hid,λ(π′ )◦!i

The composite of morphisms in C is the identity. Hence S ⊤⊤ ≤ S holds.
We next generalise ⊤⊤-closure operators to take multiple closure parameters. Let S ={S i }i∈I be a set-indexed family of closure parameters. We define (−)⊤⊤(S) by^
X ⊤⊤(S) =X ⊤⊤(S i )
i∈I

V

where
denotes the fibred product. Below we only consider set-indexed family ofclosure parameters.
Proposition 8. Let S = {S i }i∈I be a family of closure parameters. The mapping X 7→
X ⊤⊤(S) extends to a monad over P whose unit and multiplication are vertical. Furthermore, for any P-object X, we have
X ≤ X ⊤⊤(S) ,(X ⊤⊤(S) )⊤⊤(S) = X ⊤⊤(S) ,S i = S i⊤⊤(S) (i ∈ I).

3.2 Full Reflective Subcategory of ⊤⊤-Closed Objects
We investigate the structure of the full reflective subcategory of ⊤⊤-closed objects. Let
S be a family of closure parameters. We write P⊤⊤(S) for P’s full reflective subcategory
consisting of ⊤⊤(S)-closed objects (that is, objects X such that X ⊤⊤(S) = X). We write ι
for the inclusion functor from P⊤⊤(S) to P.
Since P is bi-Cartesian, P⊤⊤(S) is also bi-Cartesian (see e.g. Proposition 3.5.3 and3.5.4, [6]). The Cartesian structure is inherited from P, while the co-Cartesian structure
is given by the following diagram:
X

˙
inl
//

X +̇ Y≤˙// (X +̇ Y)⊤⊤(S) oo ≥ X +̇ Y oo inr
Y(4)

We next show that ⊤⊤(S)-closed objects form an exponential ideal.
Lemma 3. Let S = {S i }i∈I be a family of closure parameters. Then for any P-object X
˙ Y)⊤⊤(S) = X ⇒˙ Y.
and Y above I and J respectively, Y ⊤⊤(S) = Y implies (X ⇒˙ Y)⊤⊤(S) ≤ X ⇒˙ Y; the other direction is clear as
Proof. Below we only show (X ⇒⊤⊤(S)
˙ Y)⊤⊤(S) → (((X ⇒˙ Y) ⇒˙(−)
is a closure operator. Let i ∈ I. We define ẇ : (X ⇒˙S i ) ⇒ S i ) to be the composite of P-morphisms in the following diagram:˙ Y)⊤⊤(S)
(X ⇒
≤


˙ Y)⊤⊤(S i )(X ⇒// ((X ⇒˙ Y) ⇒
˙ S i) ⇒˙ SiP// ((I ⇒ J) ⇒ US i ) ⇒ US i


C

U

I⇒J

US

ηI⇒Ji

i
˙
˙
From the diagram, ẇ is above ηUSI⇒J . We also define a P-morphism ċ : X × (Y ⇒ S i ) →˙ Y) ⇒
˙ S i by(X ⇒ċ = λ̇(ev˙ ◦ (id ×˙ ev)
˙ ◦ hπ̇′ ◦ π̇, hπ̇′ , π̇ ◦ π̇ii),

which is above the following C-morphism c : I × (J ⇒ US i ) → (I ⇒ J) ⇒ US i :c = λ(ev ◦ (id × ev) ◦ hπ′ ◦ π, hπ′ , π ◦ πii).
By combining these, we obtain a P-morphism
˙ Y)⊤⊤(S) ×˙ X → (Y ⇒˙ S i) ⇒˙ Siλ̇(ev˙ ◦ (ẇ ×˙ ċ) ◦ ȧ) : (X ⇒
above
i
i
ηUS
◦ evI,J = λ(ev ◦ (ηUSJ
I⇒J × c) ◦ a) : (I ⇒ J) × I → (J ⇒ US i ) ⇒ US i(where a and ȧ are associativity morphisms in C and P respectively). This implies thatthe following inequation holds for every i ∈ I in the fibre over (I ⇒ J) × I:˙ Y)⊤⊤(S) ×˙ X 6 ev∗I,J (Y ⊤⊤(S i ) ).
(X ⇒Therefore we have˙ Y)⊤⊤(S) ×˙ X 6(X ⇒^ev∗I,J (Y ⊤⊤(S i ) ) = ev∗I,J (Y ⊤⊤(S) ).

i∈I

Now the composite, say v̇, of P-morphisms in the following diagram is above evI,J :˙ Y)⊤⊤(S) ×˙ X
(X ⇒
≤


ev∗I,J (Y ⊤⊤(S) )// Y ⊤⊤(S)P(I ⇒ J) × I

// J


C

U
evI,J

˙ Y)⊤⊤(S) → X ⇒˙ Y ⊤⊤(S) is above λ(evI,J ) = id. Hence (X ⇒˙ Y)⊤⊤(S) ≤so λ̇(v̇) : (X ⇒
⊤⊤(S)
˙
˙
X⇒Y
= X ⇒ Y.
Theorem 4. For any family S of closure parameters, ⊤⊤(S)-closed objects form a fullreflective sub bi-CCC P⊤⊤(S) of P, and U ◦ ι : P⊤⊤(S) → C is a faithful strict bi-CCfunctor.
Proof. That P⊤⊤(S) is a bi-CCC follows from Lemma 3 and Day’s reflection theorem [8].
The CC structure on P⊤⊤(S) is inherited from P; so ι is a strict CC functor. In general, ι
is not a co-Cartesian functor, but the coproduct diagram in (4) is strictly mapped to the
coproduct diagram in C by U ◦ ι. Hence U ◦ ι is a strict bi-CC functor. The faithfulness
is obvious.
3.3 Restriction Theorem
We next consider a small category L and functors F : L → C and P : L → P such thatU ◦ P = F (see the lower half of the commutative diagram in Figure 4). The functor P
specifies a family of closure parameters P = {Pτ}τ∈Obj(L) .

P′

L OOO

˙ 0̇, +̇, ⇒)˙
bi-CCC (1̇, ×,
bi-CCC (1, ×, 0, +, ⇒)strict bi-CC functor and partial orderfibration with fibred small productsLsmall category
P, F functors
P⊤⊤(P) bi-CCC of ⊤⊤(P)-closed objects
ι
strict CC inclusion functor

P
C
U

⊤⊤(P)
77 P  _
ι


// P

OOOP
OOO
U
F
OO'' 
C

Fig. 4. Restriction of P to ⊤⊤(P)-Closed Objects

Proposition 9. The functor P : L → P restricts to P⊤⊤(P) (see P′ in Figure 4).
Proof. From Proposition 8, (Pτ)⊤⊤(P) = Pτ holds for any L-object τ, that is, Pτ is anobject in the full subcategory P⊤⊤(P) of P. Hence P restricts to P⊤⊤(P) .
Theorem 5 (Restriction Theorem). In the commutative diagram in Figure 4,
1. If L is a Cartesian (closed) category and F and P are strict Cartesian (closed)
functors, then P′ is also a strict Cartesian (closed) functor.
2. If F is a strict co-Cartesian functor and P satisfies
˙ Pρ = (Pτ +̇ Pτ′ ) ⇒˙ Pρ
P(τ + τ′ ) ⇒˙ Pρ = 0̇ ⇒
˙ Pρ,
P0 ⇒

then P′ is a strict co-Cartesian functor.
3. If L is a bi-CCC, F is a strict bi-CC functor and P is a strict CC functor, then P
satisfies the above equations (hence P′ is a strict bi-CC functor).
Proof. 1. The Cartesian (closed) structure in P⊤⊤(P) is the restriction of that in P to
P⊤⊤(P) . Since P strictly preserves Cartesian (closed) structure, so does P′ .
˙ Pρ = (Pτ +̇ Pτ′ ) ⇒˙ Pρ. From the definition of ⊤⊤(P), we have
2. Suppose P(τ + τ′ ) ⇒P(τ + τ′ ) = P(τ + τ′ )⊤⊤(P)
^
∗
′ ˙
˙
=
(ηFρ
Fτ+Fτ′ ) ((P(τ + τ ) ⇒ Pρ) ⇒ Pρ)ρ∈Obj(L)

=

^

∗
′ ˙
˙
(ηFρ
Fτ+Fτ′ ) (((Pτ +̇ Pτ ) ⇒ Pρ) ⇒ Pρ)ρ∈Obj(L)= (Pτ +̇ Pτ′ )⊤⊤(P) .
One can similarly show P0 = (P0)⊤⊤(P) .
3. We show that the equations in 2 holds for each strict CC functor P such that U ◦ P =F. In any bi-CCC D there is an isomorphism
αDA,B,C(A + B) ⇒ C ooβDA,B,C// (A ⇒ C) × (B ⇒ C)

which is preserved by strict bi-CC functors. Consider the following diagram:
˙ Pρ
P(τ + τ′ ) ⇒′P((τ + τ′ ) ⇒ ρ)˙ Pρ oo(Pτ +̇ Pτ′ ) ⇒,ρP(ατ,τ
)L′

βPPτ,Pτ ,Pρ// P((τ ⇒ ρ) × (τ′ ⇒ ρ))P˙ Pρ) ×˙ (Pτ′ ⇒
˙ Pρ)
(Pτ ⇒

U

// (Fτ ⇒ Fρ) × (Fτ′ ⇒ Fρ)


C

′

′

(Fτ + Fτ ) ⇒ Fρ oo

αCFτ,Fτ ,Fρ′βCFτ,Fτ ,Fρ′′,ρ
From U ◦ P = F, the morphism P(ατ,τ) is above αCFτ,Fτ ,Fρ . Therefore the comL′
Fτ,Fτ′ ,Fρposition of morphisms in P is above βC◦ αCFτ,Fτ ,Fρ = id. Thus we obtain
˙ Pρ ≤ (Pτ +̇ Pτ′ ) ⇒˙ Pρ. The other direction, P(τ + τ′ ) ⇒˙ Pρ ≥
P(τ + τ′ ) ⇒′ ˙(Pτ +̇ Pτ ) ⇒ Pρ, follows from a similar argument.
˙ Pρ = 0̇ ⇒˙ Pρ to the reader.
We leave the proof of P0 ⇒Theorem 1 is an instance of this general restriction theorem. In Figure 4 we instantiate
U with q : KF → C, L with a small distributive category, F with a bi-Cartesian functor
and P with the definability functor of F. From Proposition 2, Lemma 2 and Theorem
5-2, we obtain Theorem 1.
3.4 A Characterisation of Definable Morphisms by Weak Logical Predicates
We finally give a characterisation of morphisms definable by the simply typed lambda
calculus with sums by means of weak logical predicates. Let B be the set of base types,
F : L1 (B) → C be a bi-CC functor and U : P → C be a fibration admitting ⊤⊤closure operators. An Obj(L1 (B))-indexed family P of P-objects is called weak logicalpredicate (with respect to F and U) if the following holds for any L1 (B)-objects τ, τ′ , ρ:
– Pτ is above Fτ,˙ Pτ′ , and– P(τ × τ′ ) = Pτ ×˙ Pτ′ , P1 = 1̇, P(τ ⇒ τ′ ) = Pτ ⇒′˙ Pρ = P((τ + τ ) ⇒ ρ), 0̇ ⇒˙ Pρ = P(0 ⇒ ρ); (c.f. Theorem 5-2).
– (Pτ +̇ Pτ) ⇒We say that a C-morphism f : Fτ → Fτ′ is invariant under P if there exists a (necessarily unique) P-morphism g : Pτ → Pτ′ above f .
Lemma 4 (Basic Lemma for Weak Logical Predicates). Let P be a weak logicalpredicate with respect to a bi-CC functor F : L1 (B) → C and a fibration U : P → C
admitting ⊤⊤-closure operators. Then for any L1 (B)-morphism f : τ → σ, F f isinvariant under P.
Theorem 6. Let C be a bi-CCC and F : L1 (B) → C be a bi-CC functor. Then a Cmorphism f is definable by F (i.e. f is in the image of F) if and only if f is invariant
under any weak logical predicate with respect to any fibration U : P → C admitting⊤⊤-closure operators.

// ClSubK ([C, _ Set])G(C, K, _ a)
ll66
l
l
lll

lll
L1 (B) R
Ka
RRR
RRR
RRR
F
RR(( 
Def F

C


// Sub([C, Set])

Ha// [C, Set]

Fig. 5. Construction of the Category of Grothendieck Predicates

Proof. If f is invariant under any weak logical predicate, then it should be so under Def
with respect to F and q in Section 2. Since Def is full, f is definable by F. The converse
is immediate from Lemma 4.

4 Related Work
4.1 Grothendieck Logical Predicates
We briefly review Fiore and Simpson’s Grothendieck logical predicates [11]. They area further refinement of Jung and Tiuryn’s Kripke predicates with varying arity using
Grothendieck topology. Let C be a small category, K be a Grothendieck topology on C
and a : C → C be a functor called arity functor. The topology K induces an idempotent monad K over the category Sub([Cop , Set]) of subpresheaves [4], and one obtains
the full reflective subcategory ClSubK ([C, Set]) → Sub([C, Set]) of K-closed subobjects. One can verify that ClSubK ([C, Set]) is a bi-CCC, and the composite of functors
ClSubK ([C, Set]) → Sub([C, Set]) → [C, Set] strictly preserves the bi-CC structure.
We then take the pullback of the composite along Ha : C → [Cop , Set] defined by
Ha (C) = C(a−, C). This yields the category G(C, K, a) of Grothendieck predicates,
which is also a bi-CCC (see Figure 5). Every Grothendieck logical predicate is thenformulated as a bi-CC functor from L1 (B) (the free bi-CCC over the set B of basetypes) to G(C, K, a).
Let C be a bi-CCC whose coproducts are stable and F : L → C be a strict bi-CCfunctor. For the characterisation of the morphisms definable by F, Fiore and Simpson
instantiated C with a syntactically constructed category of constrained contexts, K witha suitable topology on C and a with the interpretation of contexts by F. They showedthat the functor Def : L1 (B) → G(C, K, a) that captures the morphisms definable by F
is a bi-CC functor, that is, a Grothendieck logical predicate.
We give an informal comparison of their approach and our approach.
1. In our approach the parameter category for Kripke predicates is the partial order
CtxL of context inclusions, while in [11] a non-partial order category of constrained
contexts and renamings is used (although it can be switched to the partial ordercalled Diaconescu cover without affecting the result; see Section 5, [11]).

2. The closure operator K can be restricted to the one K|Ka over Ka , and G(C, K, a)
can be seen as the full reflective subcategory of the K|Ka -closed subobjects. In
our approach we derived the (⊤⊤-)closure operator over KF from the definability
predicates itself, and considered the full reflective subcategory K⊤⊤
F of ⊤⊤-closed
subobjects. Both approaches perform a similar categorical construction to obtainthe category for characterising the definability predicates, but with different closure
operators.
3. One drawback of our characterisation is that the definability predicates at sum types
are not inductively characterised, although they are coproducts of the definability
predicates at lower types. This is because the ⊤⊤-closure operator used in equations(2) and (3) refers to the definability predicates at every type. On the other hand, inFiore and Simpson’s work the definability predicates at sum types are completely
determined by those at lower types.
4. One advantage of our characterisation is that it holds for any interpretation of thesimply typed lambda calculus with sums in any bi-CCC.
4.2 Other Related Work
Pitts introduced ⊤⊤-closure operator for capturing the concept of admissible relationsin the syntactic study of a polymorphic functional language [24]. Operators that are
similar to the ⊤⊤-closure had already appeared in various forms: the duality operator
in the phase-space semantics of linear logic [13] and Parigot’s technique of the strong
normalisation of the second order classical natural deduction [23] are such instances.
The notion of ⊤⊤-closure operators also appears in other studies [21, 5].
Hinted from Pitts’ ⊤⊤-closure operator, Lindley and Stark introduced a new technique called ⊤⊤-lifting for extending the strong normalisation proof using computability predicate technique to Moggi’s computational metalanguage [20, 19]. Their ⊤⊤lifting was later categorically formulated as a method to lift strong monads on the basecategory of a fibration to the one on its total category [16] by the author. There, ⊤⊤closure operators are formulated as the ⊤⊤-lifting of the identity monad.
It is widely recognised that re-establishing properties that hold in the lambda calculus with only arrow types is difficult under the presence of sum types. For instance, thedesign of a confluent and strongly normalising rewriting system (with β-reduction andη-expansion) for the simply typed lambda calculus with sums [12] and the proof of thecompleteness of the equational theory of the lambda calculus with sums in Set [9] exhibits the intrinsic difficulty in handling sums. In this stream of research Grothendiecklogical predicates are shown to be an effective tool in reasoning about the lambda calculus with sums. They are applied to the correctness of the normalisation-by-evaluation
algorithm [2] and the proof of the extensional normalisation [3] for the lambda calculus
with sums.
Acknowledgement
The author is grateful to anonymous reviewers for their constructive comments. The
author thank Masahito Hasegawa, Kazushige Terui, Susumu Nishimura, Jacques Garrigue, Ichiro Hasuo and the members of RIMS computer science group for valuable
discussions.

References
1. M. Alimohamed. A characterization of lambda definability in categorical models of implicit
polymorphism. Theor. Comput. Sci., 146(1&2):5–23, 1995.
2. T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott. Normalization by evaluation for typed
lambda calculus with coproducts. In LICS, pages 303–310, 2001.
3. V. Balat, R. Di Cosmo, and M. Fiore. Extensional normalisation and type-directed partial
evaluation for typed lambda calculus with sums. In N. Jones and X. Leroy, editors, POPL,
pages 64–76. ACM, 2004.
4. M. Barr and C. Wells. Toposes, Triples and Theories. Splinger-Verlag, 1998.
5. N. Benton. A typed, compositional logic for a stack-based abstract machine. In Proc. APLAS’05, volume 3780 of LNCS, pages 364–380. Springer-Verlag, 2005.
6. F. Borceux. Handbook of Categorical Algebra 1, volume 50 of Encyclopedia of Mathematics
and Its Applications. Cambridge University Press, 1994.
7. J. Cockett. Introduction to distributive categories. Mathematical Structures in Computer
Science, 3(3):277–307, 1993.
8. B. Day. A reflection theorem for closed categories. Journal of pure and applied algebra,
2(1):1–11, 1972.
9. D. Dougherty and R. Subrahmanyam. Equality between functionals in the presence of coproducts. In LICS, pages 282–291. IEEE Computer Society, 1995.
10. M. Fiore, R. Di Cosmo, and V. Balat. Remarks on isomorphisms in typed lambda calculi
with empty and sum types. In LICS, pages 147–157. IEEE Computer Society, 2002.
11. M. Fiore and A. Simpson. Lambda definability with sums via grothendieck logical relations.
In Proc. TLCA ’99, volume 1581 of LNCS, pages 147–161. Springer, 1999.
12. N. Ghani. βη-equality for coproducts. In Mariangiola Dezani-Ciancaglini and Gordon D.
Plotkin, editors, TLCA, volume 902 of LNCS, pages 171–185. Springer, 1995.
13. J.-Y. Girard. Linear logic. Theor. Comp. Sci., 50:1–102, 1987.
14. B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.
15. A. Jung and J. Tiuryn. A new characterization of lambda definability. In Proc. TLCA ’93,
volume 664 of LNCS, pages 245–257. Springer, 1993.
16. S. Katsumata. A semantic formulation of ⊤⊤-lifting and logical predicates for computational
metalanguage. In Proc. CSL ’05, volume 3634 of LNCS, pages 87–102. Springer, 2005.
17. Y. Lafont. Logiques, Categóries et Machines. PhD thesis, Universit‘’e Paris VII, 1988.
18. J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridgestudies in advanced mathematics. CUP, 1986.
19. S. Lindley. Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh, 2004.
20. S. Lindley and I. Stark. Reducibility and ⊤⊤-lifting for computation types. In TLCA, pages
262–277, 2005.
21. P.-A. Melliès and J. Vouillon. Recursive polymorphic types and parametricity in an operational framework. In Proc. LICS ’05, pages 82–91. IEEE Computer Society, 2005.
22. J. Mitchell. Representation independence and data abstraction. In Proc. POPL ’86, pages
263–276, 1986.
23. M. Parigot. Proofs of strong normalisation for second order classical natural deduction.
Journal of Symbolic Logic, 62(4):1461–1479, 1997.
24. A. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in
Computer Science, 10(3):321–359, 2000.
25. A. Pitts and I. Stark. Operational reasoning for functions with local state. In A. D. Gordon
and A. M. Pitts, editors, Higher Order Operational Techniques in Semantics, Publications of
the Newton Institute, pages 227–273. Cambridge University Press, 1998.
26. R.F.C. Walters. Categories and Computer Science. Cambridge Computer Science Texts.
Cambridge University Press, 1992.