Theory and Applications of Categories, Vol. 24, No. 15, 2010, pp. 394–417.

A LOGIC FOR CATEGORIES

CLAUDIO PISANI

Abstract. We present a doctrinal approach to category theory, obtained by abstracting from the indexed inclusion (via discrete fibrations and opfibrations) of left and of right actions of X ∈ Cat in categories over X. Namely, a “weak temporal doctrine” consists essentially of two indexed functors with the same codomain such that the induced functors have both left and right adjoints satisfying some exactness conditions, in the spirit of categorical logic.

The derived logical rules include some adjunction-like laws involving the truth-values-enriched hom and tensor functors, which condense several basic categorical properties and display a nice symmetry. The symmetry becomes more apparent in the slightly stronger context of “temporal doctrines”, which we initially treat and which include as an instance the inclusion of lower and upper sets in the parts of a poset, as well as the inclusion of left and right actions of a graph in the graphs over it.

1. Introduction

Let X be a set endowed with an equivalence relation ∼, and let VX be the poset of closed parts, that is those subsets V of X such that x ∈ V and x ∼ y implies y ∈ V. A part P ∈ PX has both a “closure” ♢P and an “interior” □P, that is the inclusion i : VX → PX has both a left and a right adjoint:

♢ ⊣ i ⊣ □ : PX → VX

Thus the (co)reflection maps (inclusions) ε_{P} : i□P → P and η_{P} : P → i♢P induce bijections (between 0-elements or 1-elements sets):

\frac{PX(iV, i□P)}{PX(iV, P)}  ;  \frac{PX(i♢P, iV)}{PX(P, iV)}

By taking □(P ⇒ Q) as a VX-enrichment of PX(P, Q), it turns out that the above adjunctions are also enriched in VX giving isomorphisms:

\frac{□(iV ⇒ i□P)}{□(iV ⇒ P)}  ;  \frac{□(i♢P ⇒ iV)}{□(P ⇒ iV)}  (1)

Received by the editors 2009-08-02 and, in revised form, 2010-09-20. Transmitted by F. W. Lawvere. Published on 2010-09-23. 2000 Mathematics Subject Classification: 18A05, 18A30, 18A40, 18D99. Key words and phrases: Temporal doctrine; internally enriched hom, tensor and (co)limits; Frobenius

law; adjunction-like laws; quantification formulas.

\begin{matrix}c \\ ◯ \end{matrix} Claudio Pisani, 2010. Permission to copy for private use granted.

We also have the related laws:

\frac{i♢(iV × iW)}{iV × iW}  ;  \frac{i□(iV ⇒ iW)}{iV ⇒ iW}  ;  \frac{♢(i♢P × iV)}{♢(P × iV)}  (2)

the first two of them saying roughly that closed parts are closed with respect to product (intersection) and exponentiation (implication). Given a groupoid X, the same laws hold for the inclusion of the actions of X in the groupoids over X (via “covering groupoids”). The above situation will be placed in the proper general context in sections 2 and 3, where we develop some technical tools concerning enriched adjunctions and apply them to hyperdoctrines [Lawvere, 1970].

Now, let us drop the symmetry condition on ∼, that is suppose that X is a poset; then we have the poset of lower-closed parts LX and that of upper-closed parts RX. Again, the inclusions i^{ℓ} : LX → PX and i^{r} : RX → PX have both a left and a right adjoint:

♢^{ℓ} ⊣ i^{ℓ} ⊣ □^{ℓ} : PX → LX  ;  ♢^{r} ⊣ i^{r} ⊣ □^{r} : PX → RX

While the first ones of (1) and (2) hold “on each side”:

\frac{□^{ℓ}(i^{ℓ}V ⇒ i^{ℓ}□^{ℓ}P)}{□^{ℓ}(i^{ℓ}V ⇒ P)}  ;  \frac{□^{r}(i^{r}V ⇒ i^{r}□^{r}P)}{□^{r}(i^{r}V ⇒ P)}  (3)

\frac{i^{ℓ}♢^{ℓ}(i^{ℓ}V × i^{ℓ}W)}{i^{ℓ}V × i^{ℓ}W}  ;  \frac{i^{r}♢^{r}(i^{r}V × i^{r}W)}{i^{r}V × i^{r}W}  (4)

the other ones hold only in a mixed way:

\frac{□^{r}(i^{ℓ}♢^{ℓ}P ⇒ i^{ℓ}V)}{□^{r}(P ⇒ i^{ℓ}V)}  ;  \frac{□^{ℓ}(i^{r}♢^{r}P ⇒ i^{r}V)}{□^{ℓ}(P ⇒ i^{r}V)}  (5)

\frac{i^{ℓ}□^{ℓ}(i^{r}V ⇒ i^{ℓ}W)}{i^{r}V ⇒ i^{ℓ}W}  ;  \frac{i^{r}□^{r}(i^{ℓ}V ⇒ i^{r}W)}{i^{ℓ}V ⇒ i^{r}W}  (6)

\frac{♢^{ℓ}(i^{ℓ}♢^{ℓ}P × i^{r}V)}{♢^{ℓ}(P × i^{r}V)}  ;  \frac{♢^{r}(i^{r}♢^{r}P × i^{ℓ}V)}{♢^{r}(P × i^{ℓ}V)}  (7)

The laws (3) through (7) hold also for the inclusion of the left and the right actions of a category (or a reflexive graph [Lawvere, 1989]) X in categories (or graphs) over X (via discrete fibrations and opfibrations):

i^{ℓ} : Set^{X^{op}} → Cat/X  ;  i^{r} : Set^{X} → Cat/X

and, when they make sense, also for the inclusion of open and closed parts in the parts of a topological space (or, more generally, of local homeomorphisms and proper maps to a space X in spaces over X; see [Pisani, 2009]).

Abstracting from these situations, we may define a “temporal algebra” as a cartesian closed category with two reflective and coreflective full subcategories satisfying the above laws (in fact, it is enough to assume either (5) or (6) or (7)). A “temporal doctrine” is then essentially an indexed temporal algebra ⟨i_{X}^{ℓ} : LX → PX ← RX : i_{X}^{r} ; X ∈ C⟩ such that the inclusions i_{1}^{ℓ} and i_{1}^{r} over the terminal object 1 ∈ C are isomorphic and each substitution functor f^{∗} : PY → PX has a left adjoint Σ_{f} and a right adjoint Π_{f}. Temporal doctrines and their basic properties are presented in sections 4 and 5.

In Section 6 we show how the “truth-values” L1 ≅ R1 serve as values for an enriching of PX, LX and RX in which the adjunctions

Σ_{f} ⊣ f^{∗} ⊣ Π_{f} : PX → PY
♢_{X}^{ℓ} ⊣ i_{X}^{ℓ} ⊣ □_{X}^{ℓ} : PX → LX  ;  ♢_{X}^{r} ⊣ i_{X}^{r} ⊣ □_{X}^{r} : PX → RX
∃_{f}^{ℓ} ⊣ f^{ℓ} ⊣ ∀_{f}^{ℓ} : LX → LY  ;  ∃_{f}^{r} ⊣ f^{r} ⊣ ∀_{f}^{r} : RX → RY  (8)

are also enriched (where, for f : X → Y in C, ∃_{f}^{ℓ}M and ∀_{f}^{ℓ}M can be obtained as ♢_{Y}^{ℓ} Σ_{f}i_{X}^{ℓ}M and □_{Y}^{ℓ} Π_{f}i_{X}^{ℓ}M respectively). For example, the temporal doctrine of posets is two-valued while that of reflexive graphs is set-valued, by identifying sets with discrete graphs.

If C = Cat, the functors Π_{f} are not always available, and the above mentioned enrichment is only partially defined. This weaker situation will be axiomatized in Section 10, where we will see that (8) can be still enriched giving:

\frac{nat_{X}^{ℓ}(L, f^{ℓ}M)}{nat_{Y}^{ℓ} (∃_{f}^{ℓ}L, M)}  ;  \frac{nat_{X}^{ℓ}(f^{ℓ}M, L)}{nat_{Y}^{ℓ} (M, ∀_{f}^{ℓ}L)}  (9)

where

nat_{X}^{ℓ}(L, M) := end_{X}(i_{X}^{ℓ}L ⇒ i_{X}^{ℓ}M) := ∀_{X}^{ℓ}□_{X}^{ℓ}(i_{X}^{ℓ}L ⇒ i_{X}^{ℓ}M)

(and similarly for “right actions” or “right closed parts” in R). In a somewhat dual way one also obtains:

\frac{ten_{X}(f^{ℓ}M, N)}{ten_{Y} (M, ∃_{f}^{r}N)}  ;  \frac{ten_{X}(L, f^{r}N)}{ten_{Y} (∃_{f}^{ℓ}L, N)}  (10)

where one defines the tensor product by

ten_{X}(M, N) := coend_{X}(i_{X}^{ℓ}M × i_{X}^{r}N) := ∃_{X}^{ℓ}♢_{X}^{ℓ}(i_{X}^{ℓ}M × i_{X}^{r}N) ≅ ∃_{X}^{r}♢_{X}^{r}(i_{X}^{ℓ}M × i_{X}^{r}N)

(where the last isomorphism is mediated by L1 ≅ R1).

In Section 7 we show how the laws (9) and (10) allow one to derive in an effective and transparent way several basic facts of category theory, in particular concerning (co)limits, the Yoneda lemma, Kan extensions and final functors. In sections 8 and 9 other “classical” properties are obtained exploiting also a “comprehension” axiom, relating PX and C/X.

This approach also offers a new perspective on duality: we do not assume the coexistence of a (generalized) category X and its dual X^{op} (which in fact is not so obvious as it may seem at a first sight). Rather, we capture the interplay between left and right “actions” or “parts” of a category or “space” X by the above-sketched axioms concerning the inclusion of both of them in a category of more general “labellings” or “parts”.

It is remarkable that while (6) is equivalent to (5) and to (7), they underlie seemingly unrelated items. On the one hand, for a truth value V in L1 ≅ R1 the “V −complement” of M ∈ LX

¬(M, V) := i_{X}^{ℓ}M ⇒ i_{X}^{r}X^{r}V

“is valued” in RX, that is factors by (6) through i_{X}^{r} (and conversely). This generalizes the open-closed duality via complementation in topology (and in particular the upperlower-sets duality for a poset) which is given by ¬(M, 0), for the initial truth value 0.

On the other hand, if we denote by {x} := Σ_{x}1 the “part” in Cat/X corresponding to the object x : 1 → X, then ♢_{X}^{ℓ}{x} = X/x corresponds to the presheaf represented by x and for N ∈ RX we can prove that ten_{X}(X/x, M) ≅ x^{r}N using (7) as follows:

ten_{X}(X/x, N) ≅ ∃_{X}^{r}♢_{X}^{r}(i_{X}^{ℓ}♢_{X}^{ℓ}{x} ×_{X} i_{X}^{r}N) ≅ ∃_{X}^{r}♢_{X}^{r}({x} ×_{X} i_{X}^{r}N) ≅
≅ ♢_{1}^{r}Σ_{X}(Σ_{X}1 ×_{X} i_{X}^{r}N) ≅ ♢_{1}^{r}Σ_{X}Σ_{x}(1 × x^{∗}i_{X}^{r}N) ≅ ♢_{1}^{r}i_{1}^{r}(x^{r}N) ≅ x^{r}N

While in any temporal doctrine we can similarly derive hom_{X}(X/x, M) ≅ x^{ℓ}M using (5), in Cat such a proof of the Yoneda lemma stumbles against the lack of Π_{x} and the related non-exponentiability of {x} (whenever x is a non-trivial retract in X). In this case, or in any (weak) temporal doctrine, one can use directly the first of (9):

nat_{X}^{ℓ}(X/x, M) ≅ nat_{X}^{ℓ}(∃_{x}^{ℓ}1, M) ≅ nat_{1}^{ℓ}(1, x^{ℓ}M) ≅ x^{ℓ}M

Similarly, using (10) one gets again:

ten_{X}(N, X/x) ≅ ten_{X}(N, ∃_{x}^{ℓ}1) ≅ ten_{1}(x^{r}N, 1) ≅ x^{r}N

The present paper is a development of previous works on “balanced category theory” (see in particular [Pisani, 2008] and [Pisani, 2009]); the doctrinal approach adopted here emphasizes the logical aspects and suggests a wider range of applications.

2. Enriching adjunctions

In this section, we make some remarks that will be used in the sequel. Along with ordinary adjunctions, Kan defined and studied what are now known as adjunctions with parameter and enriched adjunctions. In particular, we will use the following result from [Kan, 1958]:

2.1. Lemma. Given functors F, F′ : C × P → V and R, R′ : P^{op} × V → C such that there are adjunctions, for any P ∈ P,

F (−, P) ⊣ R(P, −)  ;  F′(−, P) ⊣ R′(P, −)

the natural transformations F → F′ correspond bijectively to the ones R′ → R, and this correspondence restricts to natural isomorphisms. In particular F ≅ F′ iff R ≅ R′.

The next proposition implies that a geometric morphism is naturally enriched in its codomain:

2.2. Proposition. Let F ⊣ R : C → V be an adjunction between cartesian closed categories, with F preserving finite products. Then C is enriched in V via

hom_{C}^{V}(X, Y) := R(X ⇒_{C} Y)  (11)

and there are natural isomorphisms:

hom_{C}^{V}(F V, X) ≅ hom_{V}(V, RX)  (12)

(where hom_{V}(V, W) := V ⇒_{V} W is the internal hom of V) that is the adjunction F ⊣ R is itself enriched in V. Furthermore, the natural transformations given by the arrow mappings of F and R are also enriched:

hom_{V}(V, W) → hom_{C}^{V}(F V, F W)  ;  hom_{C}^{V}(X, Y) → hom_{V}(RX, RY)

Proof. For the first part, we have

V(1, R(X ⇒ Y)) ≅ C(F 1, X ⇒ Y) ≅ C(1, X ⇒ Y) ≅ C(X, Y)

(In fact, more generally, R transfers any enriching in C to an enriching in V.) For the second part, since F (V × W) ≅ F V × F W, we can apply Lemma 2.1 to the adjunctions:

F (− × W) ⊣ W ⇒ R(−) ; F (−) × F W ⊣ R(F W ⇒ −)

For the third part, the chain of natural transformations:

V(U, V ⇒ W) ≅ V(U × V, W) → C(F (U × V), F W) ≅
≅ C(F U × F V, F W) ≅ C(F U, F V ⇒ F W) ≅ V(U, R(F V ⇒ F W))

yields the desired natural transformation, which is easily seen to enrich the arrow mapping of F. For R we similarly have:

V(U, R(X ⇒ Y)) ≅ C(F U, X ⇒ Y) ≅ C(F U × X, Y) →
→ C(F (U × RX), Y) ≅ V(U × RX, RY) ≅ V(U, RX ⇒ RY)

where the non-isomorphic step is induced by the canonical

⟨F p, εF q⟩ : F (U × RX) → F U × X  (13)

Thus, R is fully faithful, also as an enriched functor, iff (13) is an iso, that is F ⊣ R satisfies the Frobenius law. Since here we have not used the fact that F preserves all finite products, but only the terminal object (in order to obtain an enrichment of R) we get in particular a proof of Corollary 1.5.9 (i) in [Johnstone, 2002].

If F has a further left adjoint L : C → V, then it is left exact and the above proposition applies. We now show that in this case the adjunction L ⊣ F is also enriched in V iff it satisfies the Frobenius reciprocity law:

2.3. Proposition. Suppose that C and V are cartesian closed and that

L ⊣ F ⊣ R : C → V

Then the existence of the following natural isomorphisms are equivalent:

1. LX ×_{V} V ≅ L(X ×_{C} F V)

2. F (V ⇒_{V} W) ≅ F V ⇒_{C} F W

3. hom_{C}^{V}(X, F V) ≅ hom_{V}(LX, V)

Proof. By applying Lemma 2.1 to the adjunctions:

L(−) × V ⊣ F (V ⇒ −) ; L(− × F V) ⊣ F V ⇒ F (−)

one gets the well-known equivalence of 1) and 2) (see [Lawvere, 1970] or [Johnstone, 2002]); similarly, the adjunctions:

LX × − ⊣ LX ⇒ − ; L(X × F (−)) ⊣ R(X ⇒ F (−))

give the equivalence of 1) and 3).

2.4. Remark. It is well known that given adjunctions L ⊣ F ⊣ R : C → V, with F fully faithful, if C is cartesian closed then so is also V; in fact, products in V can be calculated by

1_{V} := R1_{C} ; V ×_{V} W := R(F V ×_{C} F W)

or also by

1_{V} := L1_{C} ; V ×_{V} W := L(F V ×_{C} F W)

and exponentials by

V ⇒_{V} W := R(F V ⇒_{C} F W)  (14)

Note that, following Proposition 2.2, (14) can be written

hom_{V}(V, W) ≅ hom_{C}^{V}(F V, F W)

indicating that F is fully faithful as an enriched functor, so that (12) becomes

hom_{C}^{V}(F V, X) ≅ hom_{C}^{V}(F V, F RX)  (15)

Note also that, in this case, the equivalent conditions of Proposition 2.3 can be rewritten as follows:

L(X × F V) ≅ L(F LX × F V)  (16)
F V ⇒ F W ≅ F R(F V ⇒ F W)  (17)
hom_{C}^{V}(X, F V) ≅ hom_{C}^{V}(F LX, F V)  (18)

where the isomorphisms are induced by the unit of L ⊣ F (the first and the third ones) and by the counit of F ⊣ R (the second one).

3. The logic of hyperdoctrines

We now show how some of the results of Section 2 apply to hyperdoctrines [Lawvere, 1970], giving interesting consequences. Recall that a hyperdoctrine is an indexed category ⟨PX; X ∈ C⟩ such that C and all the categories PX are cartesian closed, and such that each substitution functor f^{∗} : PY → PX has both a left and a right adjoint Σ_{f} ⊣ f^{∗} ⊣ Π_{f} for any f : X → Y in C. The logical significance of hyperdoctrines, and in particular the role of the adjoints to the substitution functors as existential and universal quantification, and that of P1 as “sentences” or “truth values”, are clearly illustrated in [Lawvere, 1970] and in other papers by the same author.

Here we also assume that the adjunctions Σ_{f} ⊣ f^{∗} satisfy the Frobenius reciprocity law, that is that (13) is an iso. On the other hand, we do not need to assume that C is cartesian closed but only that it has a terminal object.

3.1. Corollary. Let ⟨PX; X ∈ C⟩ be a hyperdoctrine and define

hom_{X}(P, Q) := Π_{X}(P ⇒ Q) : (PX)^{op} × PX → P1
meets_{X}(P, Q) := Σ_{X}(P × Q) : PX × PX → P1

where the quantification indexes denote the map X → 1. Then hom_{X} enriches PX in P1 and, for any map f : X → Y, there are natural isomorphisms:

hom_{X}(f^{∗}Q, P) ≅ hom_{Y} (Q, Π_{f}P)  ;  hom_{X}(P, f^{∗}Q) ≅ hom_{Y} (Σ_{f}P, Q)
meets_{X}(f^{∗}Q, P) ≅ meets_{Y} (Q, Σ_{f}P)  ;  meets_{X}(P, f^{∗}Q) ≅ meets_{Y} (Σ_{f}P, Q)

Proof. Propositions 2.2 and 2.3 (applied to Σ_{f} ⊣ f^{∗} ⊣ Π_{f}) and the Frobenius law itself respectively give:

Π_{X}(f^{∗}Q ⇒ P) ≅ Π_{Y} Π_{f}(f^{∗}Q ⇒ P) ≅ Π_{Y} (Q ⇒ Π_{f}P)
Π_{X}(P ⇒ f^{∗}Q) ≅ Π_{Y} Π_{f}(P ⇒ f^{∗}Q) ≅ Π_{Y} (Σ_{f}P ⇒ Q)
Σ_{X}(P × f^{∗}Q) ≅ Σ_{Y} Σ_{f}(P × f^{∗}Q) ≅ Σ_{Y} (Σ_{f}P × Q)

Say that a map f : X → Y is “surjective” if Σ_{f}⊤_{X} ≅ ⊤_{Y}, where ⊤_{X} denotes a terminal object of PX.

3.2. Corollary. If f : X → Y is surjective map then

Π_{X}(f^{∗}Q) ≅ Π_{Y} Q  ;  Σ_{X}(f^{∗}Q) ≅ Σ_{Y} Q

Proof. For the first one we have:

Π_{X}(f^{∗}Q) ≅ hom_{X}(⊤_{X}, f^{∗}Q) ≅ hom_{Y} (Σ_{f}⊤_{X}, Q) ≅ hom_{Y} (⊤_{Y} , Q) ≅ Π_{Y} Q

The proof of the second one follows the same pattern:

Σ_{X}(f^{∗}Q) ≅ meets_{X}(⊤_{X}, f^{∗}Q) ≅ meets_{Y} (Σ_{f}⊤_{X}, Q) ≅ meets_{Y} (⊤_{Y} , Q) ≅ Σ_{Y} Q

Note that for ⟨PX; X ∈ Set⟩, Corollary 3.2 becomes the fact that the inverse image functor along a surjective mapping f : X → Y preserves non-emptiness and reflects maximality: if P ⊆ Y is non-empty so it is f^{−1}P and if f^{−1}P = X then P = Y.

There are three canonical ways to get a “truth value” in P1 from P ∈ PX, namely quantifications along X : X → 1 and evaluation at a point x : 1 → X:

Π_{X}P  ;  Σ_{X}P  ;  x^{∗}P

In the proof of Corollary 3.2 we have used the fact that quantifications along X are “represented” (by ⊤_{X}):

Π_{X}P ≅ hom_{X}(⊤_{X}, P) ; Σ_{X}P ≅ meets_{X}(⊤_{X}, P)

Now we show that the same is true for evaluation; namely, evaluation at x is “represented” by the “singleton”:

{x} := Σ_{x}⊤_{1}

3.3. Corollary. Given a point x : 1 → X there are isomorphisms

x^{∗}P ≅ hom_{X}({x}, P)  ;  x^{∗}P ≅ meets_{X}({x}, P)

natural in P ∈ PX.

Proof. hom_{X}(Σ_{x}⊤_{1}, P) ≅ hom_{1}(⊤_{1}, x^{∗}P) ≅ Π_{1}(x^{∗}P) ≅ x^{∗}P

meets_{X}(Σ_{x}⊤_{1}, P) ≅ meets_{1}(⊤_{1}, x^{∗}P) ≅ Σ_{1}(x^{∗}P) ≅ x^{∗}P

(Note that the quantification index 1 is the identity on 1 ∈ C.)

3.4. Remark. Suppose that C has pullbacks, so that we also have the doctrine ⟨C/X; X ∈ C⟩, with f_{!} ⊣ f^{−1} : C/Y → C/X for f : X → Y. Suppose also that ⟨PX; X ∈ C⟩ satisfies the comprehension axiom [Lawvere, 1970] c_{X} ⊣ k_{X} : PX → C/X. Then the set-valued “external evaluation” of P ∈ PX at x : 1 → X can be expressed in various ways:

P1(⊤_{1}, x^{−1}P) ≅ PX({x}, P) ≅ PX(c_{X}x, P) ≅
≅ C/X(x, k_{X}P) ≅ C/X(x_{!}1, k_{X}P) ≅ C(1, x^{−1}k_{X}P)

3.5. Corollary. [formulas for quantifications] Given P ∈ PX, a map f : X → Y and a point y : 1 → Y, there are isomorphisms

y^{∗}Π_{f}P ≅ hom_{X}(f^{∗}{x}, P)  ;  y^{∗}Σ_{f}P ≅ meets_{X}(f^{∗}{x}, P)

natural in P ∈ PX.

Proof. y^{∗}Π_{f}P ≅ hom_{Y} ({y}, Π_{f}P) ≅ hom_{X}(f^{∗}{y}, P)

y^{∗}Σ_{f}P ≅ meets_{Y} ({y}, Σ_{f}P) ≅ meets_{X}(f^{∗}{y}, P)

Note that for ⟨PX; X ∈ Set⟩, Corollary 3.5 gives the classical formula for the coimage of a part along a mapping f, and a (less classical) formula for the image: y is in the image Σ_{f}P iff its inverse image meets P.

4. Temporal doctrines

A temporal doctrine ⟨i_{X}^{ℓ} : LX → PX ← RX : i_{X}^{r} ; X ∈ C⟩ consists of two indexed functors with the same codomain, satisfying the axioms listed below.

We denote the substitution functors along a map f : X → Y in C by

f^{ℓ} : LY → LX  ;  f^{r} : RY → RX  ;  f^{∗} : PY → PX

Thus we have (coherent) isomorphisms:

(gf)^{ℓ} ≅ f^{ℓ}g^{ℓ} ;  (gf)^{r} ≅ f^{r}g^{r}  ;  (gf)^{∗} ≅ f^{∗}g^{∗}

(and similarly for identities) and also

i_{X}^{ℓ}f^{ℓ} ≅ f^{∗}i_{Y}^{ℓ}  ;  i_{X}^{r}f^{r} ≅ f^{∗}i_{Y}^{r}

We denote by BX the indexed pullback LX×_{PX} RX, by j_{X}^{ℓ} and j_{X}^{r} its indexed projections to LX and RX respectively, and

b_{X} := i_{X}^{ℓ}j_{X}^{ℓ} = i_{X}^{r}j_{X}^{r} : BX → PX

The first group of axioms requires the existence of some adjoint functors:

1. The indexing category has a terminal object: 1 ∈ C.

2. The categories of PX are cartesian closed. Thus, for any X ∈ C, we have a terminal object 1_{X} ∈ PX, products P ×_{X} Q and exponentials P ⇒_{X} Q.

3. The substitution functors f^{∗} : PY → PX have both left and right adjoints:

Σ_{f} ⊣ f^{∗} ⊣ Π_{f}

4. The functors i_{X}^{ℓ} : LX → PX and i_{X}^{r} : RX → PX have both left and right adjoints:

♢_{X}^{ℓ} ⊣ i_{X}^{ℓ} ⊣ □_{X}^{ℓ}  ;  ♢_{X}^{r} ⊣ i_{X}^{r} ⊣ □_{X}^{r}

5. The doctrine PX satisfies the comprehension axiom [Lawvere, 1970]: the canonical functors c_{X} : C/X → PX (sending f : T → X to Σ_{f}1_{T}) have right adjoints:

c_{X} ⊣ k_{X} : PX → C/X

The second group of axioms imposes some exactness condition on these functors:

1. The functors i_{X}^{ℓ} and i_{X}^{r} are fully faithful:

♢_{X}^{ℓ}i_{X}^{ℓ} ≅ id_{LX}  ;  □_{X}^{ℓ}i_{X}^{ℓ} ≅ id_{LX}

(and similarly for i_{X}^{r}).

2. The doctrine PX satisfies the Frobenius law:

Σ_{f}P ×_{Y} Q ≅ Σ_{f}(P ×_{X} f^{∗}Q)  (19)

for any f : X → Y (naturally in P ∈ PX and Q ∈ PY).

3. The adjunctions ♢_{X}^{ℓ} ⊣ i_{X}^{ℓ} and ♢_{X}^{r} ⊣ i_{X}^{r} satisfy the “mixed Frobenius laws”, that is their units induce isomorphisms

♢_{X}^{ℓ}(P ×_{X} i_{X}^{r}N) ≅ ♢_{X}^{ℓ}(i_{X}^{ℓ}♢_{X}^{ℓ}P ×_{X} i_{X}^{r}N)  (20)
♢_{X}^{r}(P ×_{X} i_{X}^{ℓ}M) ≅ ♢_{X}^{r}(i_{X}^{r}♢_{X}^{r}P ×_{X} i_{X}^{ℓ}M)  (21)

(natural in P ∈ PX, N ∈ RX and M ∈ LX).

4. The projections j_{1}^{ℓ} : B1 → L1 and j_{1}^{r} : B1 → R1 are isomorphisms.

5. The comprehension functors k_{X} : PX → C/X are fully faithful:

c_{X}k_{X}P = Σ_{k_{X}P} 1_{X_{!}(k_{X}P)} ≅ P  (22)

(where we use the notations of Remark 3.4, so that X_{!} is the domain projection C/X → C. Note that the index k_{X}P of Σ is an object of C/X, so that it should be more exactly be replaced by X_{!}(k_{X}P), where now k_{X}P denote the map to the terminal in C/X).

4.1. Examples.

1. Any hyperdoctrine ⟨PX; X ∈ C⟩ (see Section 3) with a fully faithful comprehension functor gives rise to a (rather trivial) temporal doctrine:

⟨ id : PX → PX ← PX : id ; X ∈ C ⟩

Thus the results of Section 3 can be seen as particular cases of those we will obtain for temporal doctrines.

2. ⟨i_{X}^{ℓ} : LX → PX ← RX : i_{X}^{r} ; X ∈ Pos⟩, where ⟨PX; X ∈ Pos⟩ is the doctrine of all the parts of a poset, while LX and RX are the subdoctrines of lower-closed and upper-closed parts of X.

3. ⟨i_{X}^{ℓ} : LX → Grph/X ← RX : i_{X}^{r} ; X ∈ Grph⟩, where Grph is the category of reflexive graphs, while LX and RX are the categories of left and right actions of X (or of the free category generated by it; see [Lawvere, 1989]).

4. Sets endowed with an equivalence relation give rise, as sketched in the introduction, to a “symmetrical” temporal doctrine: all the projections j_{X}^{ℓ} and j_{X}^{r} are isomorphisms (so that LX ≅ RX ≅ BX as subobjects of PX). Note that, since the axioms are symmetrical, each temporal doctrine has a dual obtained by exchanging the left and the right side (that is i^{ℓ} and i^{r}); while a symmetrical temporal doctrine is clearly self-dual (that is isomorphic to its own dual) the same is true also for Grph, via the “opposite” functor Grph → Grph.

5. Any strong balanced factorization category ⟨ C; E, M; E′, M′⟩ (see [Pisani, 2008] and [Pisani, 2009]) such that C is locally cartesian closed and M/X and M′/X are coreflective in C/X, gives rise to the temporal doctrine

⟨i_{X}^{ℓ} : M/X → C/X ← M′/X : i_{X}^{r} ; X ∈ C⟩

6. Given a temporal doctrine on a category C and any subcategory C′ of C such that 1 ∈ C′, one gets by restriction another temporal doctrine on C′.

4.2. Remark. The name “temporal doctrine” is clearly suggested by the functors ♢^{ℓ}, □^{ℓ}, ♢^{r} and □^{r}, which can be seen as modal operators acting in the two directions of time.

A categorical approach to modal and tense logic was developed in the eighties by Ghilardi and Meloni and independently by Reyes et al. Not being here specifically concerned with these logics, we just note that the temporal doctrine of posets mentioned in the examples above is also an instance of temporal doctrine in the sense of [Ghilardi & Meloni, 1991].

Let me also acknowledge that it was Prof. Giancarlo Meloni, the supervisor of my PhD thesis, who introduced me to categorical logic showing in particular how adjunctions can be an effective tool for doing calculations.

5. Basic properties

5.1. terminology. Since a (weaker form of) temporal doctrine is mainly intended to model the situation ⟨Set^{X^{op}} → Cat/X ← Set^{X} ; X ∈ Cat⟩, the objects of C should be thought of as generalized categories. In fact in the sequel we will freely borrow terminology from category theory, whenever opportune. However, the interior (□^{ℓ} and □^{r}) and closure (♢^{ℓ} and ♢^{r}) operators suggest that it also make sense to consider the objects of C as a sort of spaces, so that we will also borrow some terminology from topology; in fact, the links with that subject can be taken quite seriously as sketched in [Pisani, 2009], where it is discussed also the significance of the “closure” reflection in “open parts” (or “local homeomorphisms”). Anyway, if X is a topological space and i_{X}^{ℓ} and i_{X}^{r} are the inclusion of open and closed parts respectively in PX, the mixed Frobenius laws (and their equivalent ones in Proposition 5.2 below) hold true when they make sense, that is when only the operators □_{X}^{ℓ} and ♢_{X}^{r} are involved.

Thus we sometimes refer to objects and arrows of C as “spaces” and “maps”; to the objects of PX as “parts” of X and to those of LX and RX as “left closed” and “right closed” parts of X, respectively. The reflections ♢_{X}^{ℓ} and ♢_{X}^{r} are the “left” and “right” closure operators respectively, while □_{X}^{ℓ} and □_{X}^{r} are the “left” and “right” interior operators.

To summarize the definition, apart from the axioms concerning the comprehension adjunctions, a temporal doctrine is a hyperdoctrine PX (in the sense of Section 3) with two reflective and coreflective indexed subcategories LX and RX such that L1 and R1 are isomorphic as subcategories of P1; furthermore, and most importantly, we assume the mixed Frobenius laws (20) and (21), which are rich of important consequences. The reason of their name follows by Remark 2.4: they look like the Frobenius laws for ♢_{X}^{ℓ} ⊣ i_{X}^{ℓ} and ♢_{X}^{r} ⊣ i_{X}^{r}, except that i_{X}^{ℓ} and i_{X}^{r} are exchanged in the second factors. In fact, we have the corresponding mixed equivalent conditions:

5.2. Proposition. The following laws hold in a temporal doctrine, and each of them can be used in the definition in place of (20) and (21):

i_{X}^{r}N ⇒ i_{X}^{ℓ}M ≅ i_{X}^{ℓ}□_{X}^{ℓ}(i_{X}^{r}N ⇒ i_{X}^{ℓ}M) ; i_{X}^{ℓ}M ⇒ i_{X}^{r}N ≅ i_{X}^{r}□_{X}^{r}(i_{X}^{ℓ}M ⇒ i_{X}^{r}N) (23)

□_{X}^{r}(P ⇒ i_{X}^{ℓ}M) ≅ □_{X}^{r}(i_{X}^{ℓ}♢_{X}^{ℓ}P ⇒ i_{X}^{ℓ}M) ; □_{X}^{ℓ}(P ⇒ i_{X}^{r}N) ≅ □_{X}(i_{X}^{r}♢_{X}^{r}P ⇒ i_{X}^{r}N)

(24)

Furthermore

□_{X}^{ℓ}(i_{X}^{ℓ}M ⇒ P) ≅ □_{X}^{ℓ}(i_{X}^{ℓ}M ⇒ i_{X}^{ℓ}□_{X}^{ℓ}P) ; □_{X}^{r}(i_{X}^{r}N ⇒ P) ≅ □_{X}^{r}(i_{X}^{r}N ⇒ i_{X}^{r}□_{X}^{r}P)

Proof. The isomorphism (20) induce two families of natural isomorphisms,

♢_{X}^{ℓ}(− ×_{X} i_{X}^{r}N) ≅ ♢_{X}^{ℓ}(i_{X}^{ℓ}♢_{X}^{ℓ}(−) ×_{X} i_{X}^{r}N) : PX → LX  (25)
♢_{X}^{ℓ}(P ×_{X} i_{X}^{r}(−)) ≅ ♢_{X}^{ℓ}(i_{X}^{ℓ}♢_{X}^{ℓ}P ×_{X} i_{X}^{r}(−)) : RX → LX  (26)

Then, as in Proposition 2.3, their right adjoint with parameter give the first ones of (23) and (24); the other ones clearly follow symmetrically from (21). For the last statement, recall (15).

From (23) we immediately get:

5.3. Corollary. If the part P ∈ PX is left closed and Q ∈ PX is right closed (that is P ≅ i_{X}^{ℓ}M and Q ≅ i_{X}^{r}N) then P ⇒ Q is itself right closed.

As already mentioned in the Introduction, we so have an “explanation” of the fact that the complement of an upper-closed part of a poset is lower-closed (and conversely).

5.4. Corollary. The categories BX are themselves cartesian closed, with the “same” exponential as PX:

b_{X}B ⇒ b_{X}C ≅ b_{X}(B ⇒_{BX} C)

5.5. Proposition. ⟨LX; X ∈ C⟩ and ⟨RX; X ∈ C⟩ are themselves hyperdoctrines, with a fully faithful comprehension adjoint.

Proof.

1. As in Remark 2.4, the categories LX and RX are cartesian closed, with exponentials

given by

□_{X}^{ℓ}(i_{X}^{ℓ}L ⇒ i_{X}^{ℓ}M) ; □_{X}^{r}(i_{X}^{r}N ⇒ i_{X}^{r}O)

We denote products in LX and RX by

⊤_{X}^{ℓ}  ;  L ∧_{X}^{ℓ} M  ;  ⊤_{X}^{r}  ;  N ∧_{X}^{r} O

2. The substitution functors for left and right closed parts have both left and right

adjoints:

∃_{f}^{ℓ} ⊣ f^{ℓ} ⊣ ∀_{f}^{ℓ}  ;  ∃_{f}^{r} ⊣ f^{r} ⊣ ∀_{f}^{r}

where

∃_{f}^{ℓ} ≅ ♢_{Y}^{ℓ} Σ_{f} i_{X}^{ℓ}  ;  ∀_{f}^{ℓ} ≅ □_{Y}^{ℓ} Π_{f} i_{X}^{ℓ}  (27)

(and similarly for ∃_{f}^{r} and ∀_{f}^{r}). Note that these satisfy:

∃_{f}^{ℓ}♢_{X}^{ℓ} ≅ ♢_{Y}^{ℓ} Σ_{f}  ;  ∀_{f}^{ℓ}□_{X}^{ℓ} ≅ □_{Y}^{ℓ} Π_{f}  (28)

(and similarly for ∃_{f}^{r} and ∀_{f}^{r}).

3. The canonical functors C/X → LX send f : T → X to

∃_{f}^{ℓ}⊤_{T}^{ℓ} ≅ ♢_{X}^{ℓ}Σ_{f} i_{X}^{ℓ}⊤_{T}^{ℓ} ≅ ♢_{X}^{ℓ}Σ_{f}1_{T} ≅ ♢_{X}^{ℓ}c_{X}f

that is factor through the corresponding ones for PX. Thus, they have the functors k_{X}i_{X}^{ℓ} : LX → C/X as fully faithful right adjoints (and similarly for RX; we leave it to the reader to check the above factorization for the arrow mapping).

The fact that the adjunctions ♢_{X}^{ℓ} ⊣ i_{X}^{ℓ} and ♢_{X}^{r} ⊣ i_{X}^{r} satisfy the mixed Frobenius laws implies a restricted form of the Frobenius law for each of them and also for ∃_{f}^{ℓ} ⊣ f^{ℓ} and ∃_{f}^{r} ⊣ f^{r}, which will be used in the sequel:

5.6. Proposition. [restricted Frobenius laws] For any X ∈ C, there are natural isomorphisms:

♢_{X}^{ℓ}(P ×_{X} i_{X}^{ℓ}j_{X}^{ℓ}B) ≅ ♢_{X}^{ℓ}P ∧_{X}^{ℓ} j_{X}^{ℓ}B

For any f : X → Y in C, there are natural isomorphisms:

∃_{f}^{ℓ}(M ∧_{X}^{ℓ} f^{ℓ}j_{Y}^{ℓ} B) ≅ ∃_{f}^{ℓ}M ∧_{Y}^{ℓ} j_{Y}^{ℓ} B  ;  ∃_{f}^{r}(N ∧_{X}^{r} f^{r}j_{Y}^{r} B) ≅ ∃_{f}^{r}N ∧_{Y}^{r} j_{Y}^{r} B

Proof. For the first one, by the mixed Frobenius law we get:

♢_{X}^{ℓ}(P ×_{X} i_{X}^{ℓ}j_{X}^{ℓ}B) ≅ ♢_{X}^{ℓ}(P ×_{X} i_{X}^{r}j_{X}^{r}B) ≅ ♢_{X}^{ℓ}(i_{X}^{ℓ}♢_{X}^{ℓ}P ×_{X} i_{X}^{r}j_{X}^{r}B) ≅
≅ ♢_{X}^{ℓ}(i_{X}^{ℓ}♢_{X}^{ℓ}P ×_{X} i_{X}^{ℓ}j_{X}^{ℓ}B) ≅ ♢_{X}^{ℓ}i_{X}^{ℓ}(♢_{X}^{ℓ}P ∧_{X}^{ℓ} j_{X}^{ℓ}B) ≅ ♢_{X}^{ℓ}P ∧_{X}^{ℓ} j_{X}^{ℓ}B

For the second one, we then have:

∃_{f}^{ℓ}(M ∧_{X}^{ℓ} f^{ℓ}j_{Y}^{ℓ} B) ≅ ♢_{Y}^{ℓ} Σ_{f}i_{X}^{ℓ}(M ∧_{X}^{ℓ} f^{ℓ}j_{Y}^{ℓ} B) ≅
≅ ♢_{Y}^{ℓ} Σ_{f}(i_{X}^{ℓ}M ×_{X} i_{X}^{ℓ}f^{ℓ}j_{Y}^{ℓ} B) ≅ ♢_{Y}^{ℓ} Σ_{f}(i_{X}^{ℓ}M ×_{X} f^{∗}i_{Y}^{ℓ} j_{Y}^{ℓ} B) ≅
≅ ♢_{Y}^{ℓ} (Σ_{f}i_{X}^{ℓ}M ×_{Y} i_{Y}^{ℓ} j_{Y}^{ℓ} B) ≅ (♢_{Y}^{ℓ} Σ_{f}i_{X}^{ℓ}M) ∧_{Y}^{ℓ} j_{Y}^{ℓ} B ≅ ∃_{f}^{ℓ}M ∧_{Y}^{ℓ} j_{Y}^{ℓ} B

6. Functors valued in truth values

In the sequel, a major role will be played by the “truth values” category B1. We denote by true its terminal object, so that

j_{1}^{ℓ}true ≅ ⊤_{1}^{ℓ} ; j_{1}^{r}true ≅ ⊤_{1}^{r}

The functors X^{∗}b_{1} : B1 → PX can be factorized in various ways:

i_{X}^{ℓ}X^{ℓ}j_{1}^{ℓ} = X^{∗}i_{1}^{ℓ}j_{1}^{ℓ} = X^{∗}i_{1}^{r}j_{1}^{r} = i_{X}^{r}X^{r}j_{1}^{r}

(where X denotes also the map X → 1). Thus their left and right adjoints can be factorized as:

(j_{1}^{ℓ})^{−1}∃_{X}^{ℓ}♢_{X}^{ℓ} ≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X} ≅ (j_{1}^{r})^{−1}♢_{1}^{r}Σ_{X} ≅ (j_{1}^{r})^{−1}∃_{X}^{r}♢_{X}^{r}  (29)
(j_{1}^{ℓ})^{−1}∀_{X}^{ℓ}□_{X}^{ℓ} ≅ (j_{1}^{ℓ})^{−1}□_{1}^{ℓ}Π_{X} ≅ (j_{1}^{r})^{−1}□_{1}^{r}Π_{X} ≅ (j_{1}^{r})^{−1}∀_{X}^{r}□_{X}^{r}  (30)

We refer to (any one of) these as the “coend” and “end” functors at X, respectively:

coend_{X} ⊣ X^{∗}b_{1} ⊣ end_{X} : PX → B1

This terminology is justified by the fact that, for a bifunctor H : X^{op} × X → Set, one can easily construct an object h of Cat/X such that end_{X}h gives the usual end of H, while coend_{X}h gives the coend of H in the sense of strong dinaturality, which in most relevant cases reduces to the usual one as well (see [Pisani, 2007]).

Next we define the functors

meets_{X} : PX × PX → B1 ; hom_{X} : (PX)^{op} × PX → B1

meets_{X}(P, Q) := coend_{X}(P × Q) ; hom_{X}(P, Q) := end_{X}(P ⇒ Q) and their restrictions

ten_{X} : RX × LX → B1
nat_{X}^{ℓ} : (LX)^{op} × LX → B1 ; nat_{X}^{r} : (RX)^{op} × RX → B1
ten_{X}(M, N) := meets_{X}(i_{X}^{ℓ}M, i_{X}^{r}N)
nat_{X}^{ℓ}(L, M) := hom_{X}(i_{X}^{ℓ}L, i_{X}^{ℓ}M) ; nat_{X}^{r}(N, O) := hom_{X}(i_{X}^{r}N, i_{X}^{r}O)

For instance, in the temporal doctrine of posets B1 ≅ P1 ≅ {false ⊢ true} and

meets_{X}(P, Q) = true

iff P and Q have a non-empty intersection (and similarly for ten_{X}(M, N)). Of course, hom_{X}(P, Q) = true iff P ⊆ Q (and similarly for nat_{X}^{ℓ}(L, M) and nat_{X}^{r}(N, O)). In the temporal doctrine of reflexive graphs, P1 ≅ Grph while B1 ≅ Set; the coend of P : T → X in Grph/X is given by the components of T, while its end is the set of sections X → T.

Note that while hom_{X} and meets_{X} are valued in B1 rather than in P1 as in Section 3, the notation becomes consistent for the first example in 4.1.

6.1. The enriched adjunction laws. In the following proposition we show that the adjunctions which define a temporal doctrine can be internalized, that is they are enriched in the truth values category B1. Furthermore, some of them have an exact counterpart in a similar law, with the “meets” or “tensor” functors in place of the “hom” or “nat” functors; the proofs are also nicely symmetrical.

6.2. Proposition. The functors hom_{X}, nat_{X}^{ℓ} and nat_{X}^{r} enrich PX, LX and RX respectively in B1 and, for any space X ∈ C or map f : X → Y, there are natural isomorphisms:

hom_{X}(f^{∗}Q, P) ≅ hom_{Y} (Q, Π_{f}P)  ;  hom_{X}(P, f^{∗}Q) ≅ hom_{Y} (Σ_{f}P, Q) (31)
meets_{X}(f^{∗}Q, P) ≅ meets_{Y} (Q, Σ_{f}P) ; meets_{X}(P, f^{∗}Q) ≅ meets_{Y} (Σ_{f}P, Q) (32)
nat_{X}^{ℓ}(M, □_{X}^{ℓ}P) ≅ hom_{X}(i_{X}^{ℓ}M, P)  ;  nat_{X}^{r}(N, □_{X}^{r}P) ≅ hom_{X}(i_{X}^{r}N, P) (33)
nat_{X}^{ℓ}(♢_{X}^{ℓ}P, M) ≅ hom_{X}(P, i_{X}^{ℓ}M)  ;  nat_{X}^{r}(♢_{X}^{r}P, N) ≅ hom_{X}(P, i_{X}^{r}N) (34)
ten_{X}(♢_{X}^{ℓ}P, N) ≅ meets_{X}(P, i_{X}^{r}N) ; ten_{X}(M, ♢_{X}^{r}P) ≅ meets_{X}(i_{X}^{ℓ}M, P) (35)
nat_{X}^{ℓ}(f^{ℓ}M, L) ≅ nat_{Y}^{ℓ} (M, ∀_{f}^{ℓ}L)  ;  nat_{X}^{r}(f^{r}O, N) ≅ nat_{Y}^{r} (O, ∀_{f}^{r}N)  (36)
nat_{X}^{ℓ}(L, f^{ℓ}M) ≅ nat_{Y}^{ℓ} (∃_{f}^{ℓ}L, M)  ;  nat_{X}^{r}(N, f^{r}O) ≅ nat_{Y}^{r} (∃_{f}^{r}N, O)  (37)
ten_{X}(L, f^{r}N) ≅ ten_{Y} (∃_{f}^{ℓ}L, N)  ;  ten_{X}(f^{ℓ}M, N) ≅ ten_{Y} (M, ∃_{f}^{r}N) (38)

Proof. For the first part, see Proposition 2.2. For (31) and (32), recall Corollary 3.1 and note that the present “hom” and “meets” functors factor through the ones there.

Equations (33), (34) and (35) follow from Proposition 5.2 and the other factorizations of the coend and the end functors in (29) and (30). Recalling (27), we obtain the remaining ones by composition of (enriched) adjoints. Alternatively, one can explicitly derive them as we exemplify for (37) and (38):

(j_{1}^{ℓ})^{−1}□_{1}^{ℓ}Π_{X}(i_{X}^{ℓ}L ⇒ i_{X}^{ℓ}f^{ℓ}M) ≅ (j_{1}^{ℓ})^{−1}□_{1}^{ℓ}Π_{Y} Π_{f}(i_{X}^{ℓ}L ⇒ f^{∗}i_{Y}^{ℓ} M)
≅ (j_{1}^{ℓ})^{−1}□_{1}^{ℓ}Π_{Y} (Σ_{f}i_{X}^{ℓ}L ⇒ i_{Y}^{ℓ} M) ≅ (j_{1}^{r})^{−1}∀_{Y}^{r} □_{Y}^{r} (Σ_{f}i_{X}L ⇒ i_{Y}^{ℓ} M)
≅ (j_{1}^{r})^{−1}∀_{Y}^{r} □_{Y}^{r} (i_{Y}^{ℓ} ♢_{Y}^{ℓ} Σ_{f}i_{X}^{ℓ}L ⇒ i_{Y}^{ℓ} M)
(j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X}(i_{X}^{ℓ}f^{ℓ}M × i_{X}^{r}N) ≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{Y} Σ_{f}(f^{∗}i_{Y}^{ℓ} M × i_{X}^{r}N)
≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{Y} (i_{Y}^{ℓ} M × Σ_{f}i_{X}^{r}N) ≅ (j_{1}^{r})^{−1}∃_{Y}^{r} ♢_{Y}^{r} (i_{Y}^{ℓ} M × Σ_{f}i_{X}^{r}N)
≅ (j_{1}^{r})^{−1}∃_{Y}^{r} ♢_{Y}^{r} (i_{Y}^{ℓ} M × i_{Y}^{r} ♢_{Y}^{r} Σ_{f}i_{X}^{r}N)

7. Limits, colimits and Yoneda properties

As we will see in Section 10, the laws in Proposition 6.2 still hold for weak temporal doctrines (at least to the extent that hom is defined), which include the motivating instance ⟨Set^{X^{op}} → Cat/X ← Set^{X} ; X ∈ Cat⟩. Thus, with the same technique exploited in Section 3, we begin to draw some consequences which in fact hold in the weaker context as well. Accordingly, we mainly maintain the policy of using terms which reflect the case C = Cat just mentioned.

We define the (internally enriched) “limit” and “colimit” functors by restricting the end and the coend functors to (left or right) closed parts:

lim_{X}^{ℓ} := end_{X}i_{X}^{ℓ} ≅ (j_{1}^{ℓ})^{−1}∀_{X}^{ℓ} : LX → B1

lim_{X}^{r} := end_{X}i_{X}^{r} ≅ (j_{1}^{r})^{−1}∀_{X}^{r} : RX → B1

colim_{X}^{ℓ} := coend_{X}i_{X}^{ℓ} ≅ (j_{1}^{ℓ})^{−1}∃_{X}^{ℓ} : LX → B1

colim_{X}^{r} := coend_{X}i_{X}^{r} ≅ (j_{1}^{r})^{−1}∃_{X}^{r} : RX → B1

Say that f : X → Y is “final” (resp. “initial”) if ∃_{f}^{ℓ}⊤_{X}^{ℓ} ≅ ⊤_{Y}^{ℓ} (resp. ∃_{f}^{r}⊤_{X}^{r} ≅ ⊤_{Y}^{r}).

7.1. Corollary. [final maps preserve (co)limits] If f : X → Y is final then

lim_{X}^{ℓ}(f^{ℓ}M) ≅ lim_{Y}^{ℓ} M  ;  colim_{X}^{r}(f^{r}N) ≅ colim_{Y}^{r} N  (39)

and if f : X → Y is initial then

colim_{X}^{ℓ}(f^{ℓ}M) ≅ colim_{Y}^{ℓ} M  ;  lim_{X}^{r}(f^{r}N) ≅ lim_{Y}^{r} N

Proof. For the first one of (39), using (37) we have:

lim_{X}^{ℓ}(f^{ℓ}M) ≅ nat_{X}^{ℓ}(⊤_{X}^{ℓ}, f^{ℓ}M) ≅ nat_{Y}^{ℓ} (∃_{f}^{ℓ}⊤_{X}^{ℓ}, M) ≅ nat_{Y}^{ℓ} (⊤_{Y}^{ℓ} , M) ≅ lim_{Y}^{ℓ} M

For the second one of (39), we follow exactly the same pattern using (38) instead:

colim_{X}^{r}(f^{r}N) ≅ ten_{X}(⊤_{X}^{ℓ}, f^{r}N) ≅ ten_{Y} (∃_{f}^{ℓ}⊤_{X}^{ℓ}, N) ≅ ten_{Y} (⊤_{Y}^{ℓ} , N) ≅ colim_{Y}^{r} N

The other ones are proved in the same way.

There are three canonical ways of obtaining a truth value in B1 from a closed part, namely the limit or the colimit functors and “evaluation” at a point x : 1 → X:

lim_{X}^{ℓ}M  ;  colim_{X}^{ℓ}M  ;  (j_{1}^{ℓ})^{−1}(x^{ℓ}M)
lim_{X}^{r}N  ;  colim_{X}^{r}N  ;  (j_{1}^{r})^{−1}(x^{r}N)

In the proof of Corollary 7.1 we have used the fact that limits and colimits over X are “represented” (by ⊤_{X}^{ℓ} or ⊤_{X}^{r}). Now we show that the same is true for evaluation; namely, evaluation at x is “represented” by the left and right “slices”:

X/x := ∃_{x}^{ℓ}⊤_{1}^{ℓ} ;  x\X := ∃_{x}^{r}⊤_{1}^{r}  (40)

Note that slices can be obtained as the (left or right) closure of the “singletons” {x} = Σ_{x}1_{1} = c_{X}x of Section 3:

X/x = ♢_{X}^{ℓ}{x} ; x\X = ♢_{X}^{r}{x}

7.2. Corollary. [Yoneda properties] Given a point x : 1 → X in C, there are isomorphisms

(j_{1}^{ℓ})^{−1}(x^{ℓ}M) ≅ nat_{X}^{ℓ}(X/x, M)  ;  (j_{1}^{ℓ})^{−1}(x^{ℓ}M) ≅ ten_{X}(M, x\X)

natural in P ∈ PX (and dually for right closed parts). Proof.

nat_{X}^{ℓ}(∃_{x}^{ℓ}⊤_{1}^{ℓ}, M) ≅ nat_{1}^{ℓ}(⊤_{1}^{ℓ}, x^{ℓ}M) ≅ lim_{1}^{ℓ}(x^{ℓ}M) ≅ (j_{1}^{ℓ})^{−1}∀_{1}^{ℓ}(x^{ℓ}M) ≅ (j_{1}^{ℓ})^{−1}(x^{ℓ}M)

ten_{X}(M, ∃_{x}^{r}⊤_{1}^{r}) ≅ ten_{1}(x^{ℓ}M, ⊤_{1}^{r}) ≅ colim_{1}^{ℓ}(x^{ℓ}M) ≅ (j_{1}^{ℓ})^{−1}∃_{1}^{ℓ}(x^{ℓ}M) ≅ (j_{1}^{ℓ})^{−1}(x^{ℓ}M)

The evaluation at points of quantified parts can be obtained as follows:

7.3. Corollary. [formulas for quantifications, interior and closure] Given a map f : X → Y and a point y : 1 → Y in C, there are isomorphisms

(j_{1}^{ℓ})^{−1}(y^{ℓ}∀_{f}^{ℓ}M) ≅ nat_{X}^{ℓ}(f^{ℓ}Y/y, M)  ;  (j_{1}^{ℓ})^{−1}(y^{ℓ}∃_{f}^{ℓ}M) ≅ ten_{X}(M, f^{r}y\Y)

natural in M ∈ LX (and dually for right closed parts). There are isomorphisms

(j_{1}^{ℓ})^{−1}(x^{ℓ}□_{X}^{ℓ}P) ≅ hom_{X}(i_{X}^{ℓ}X/x, P)  ;  (j_{1}^{ℓ})^{−1}(x^{ℓ}♢_{X}^{ℓ}P) ≅ meets_{X}(P, i_{X}^{r}x\X)

natural in P ∈ PX (and dually for right closure).

Proof. Using Corollary 7.2 and (36), (38), (33) and (35) respectively, we get: (j_{1}^{ℓ})^{−1}(y^{ℓ}∀_{f}^{ℓ}M) ≅ nat_{Y}^{ℓ} (Y/y, ∀_{f}^{ℓ}M) ≅ nat_{X}^{ℓ}(f^{ℓ}Y/y, M) (j_{1}^{ℓ})^{−1}(y^{ℓ}∃_{f}^{ℓ}M) ≅ ten_{Y} (∃_{f}^{ℓ}M, y\Y) ≅ ten_{X}(M, f^{r}y\Y, M) (j_{1}^{ℓ})^{−1}(x^{ℓ}□_{X}^{ℓ}P) ≅ nat_{X}^{ℓ}(X/x, □_{X}^{ℓ}P) ≅ hom_{X}(i_{X}^{ℓ}X/x, P) (j_{1}^{ℓ})^{−1}(x^{ℓ}♢_{X}^{ℓ}P) ≅ ten_{X}(♢_{X}^{ℓ}P, x\X) ≅ meets_{X}(P, i_{X}^{r}x\X)

8. Exploiting comprehension

In this section and in the next one we present some consequences of the comprehension adjunction c_{X} ⊣ k_{X} : PX → C/X and of the assumption that it is fully faithful.

8.1. The components functor. We define the “components” functor π_{0} : C → B1 by:

π_{0}X := coend_{X}1_{X} = colim_{X}^{ℓ}⊤_{X}^{ℓ} = colim_{X}^{r}⊤_{X}^{r}

8.2. Remarks. Note that X is connected, that is π_{0}X ≅ true, iff X → 1 is final (or initial). Note also that the components functor

π_{0}X = coend_{X}1_{X} = (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X}1_{X} = (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}c_{1}X = (j_{1}^{r})^{−1}♢_{1}^{r}c_{1}X

is left adjoint to the full inclusion k_{1}b_{1} : B1 → C. Coherently, we say that a space X ∈ C is “discrete” if X ≅ k_{1}b_{1}V, for a truth value V ∈ B1, so that π_{0} yields in fact the reflection in discrete spaces.

Conversely, the coend functor can be reduced to components or to a colimit by

coend_{X}P ≅ π_{0}X_{!}k_{X}P ≅ colim_{X_{!}k_{X}P}^{ℓ} ⊤_{X_{!}k_{X}P}^{ℓ}  (41)

Indeed we have:

coend_{X}P ≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X}P ≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X}c_{X}k_{X}P ≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X}Σ_{k_{X}P} 1_{X_{!}k_{X}P} ≅

≅ (j_{1}^{ℓ})^{−1}♢_{1}^{ℓ}Σ_{X_{!}k_{X}P} 1_{X_{!}k_{X}P} ≅ coend_{X_{!}k_{X}P} 1_{X_{!}k_{X}P} ≅ π_{0}X_{!}k_{X}P

8.3. The limit and colimit formulas for nat and ten. Since coend_{X} can be reduced to a colimit by (41), the same is true for the functors meets_{X} and ten_{X}. In fact we can do better, by reducing ten_{X}(M, N) to a colimit over the space corresponding to i_{X}^{r}N (or to i_{X}^{ℓ}M), rather than to i_{X}^{r}N ×_{X} i_{X}^{ℓ}M; similarly, nat_{X} can be reduced to a limit:

8.4. Proposition. [(co)limit formulas for ten and nat]

meets_{X}(P, Q) ≅ coend_{X_{!}k_{X}Q}(k_{X}Q)^{∗}P ≅ coend_{X_{!}k_{X}P} (k_{X}P)^{∗}Q  (42)
ten_{X}(M, N) ≅ colim_{X_{!}k_{X}i_{X}^{r}N}^{ℓ}(k_{X}i_{X}^{r}N)^{ℓ}M ≅ colim_{X_{!}k_{X}i_{X}^{ℓ}M}^{r}(k_{X}i_{X}^{ℓ}M)^{r}N  (43)
hom_{X}(P, Q) ≅ end_{X_{!}k_{X}Q}(k_{X}Q)^{∗}P ≅ end_{X_{!}k_{X}P} (k_{X}P)^{∗}Q  (44)
nat_{X}^{ℓ}(L, M) ≅ lim_{X_{!}k_{X}i_{X}^{ℓ}L}^{ℓ}(k_{X}i_{X}^{ℓ}L)^{ℓ}M ; nat_{X}^{r}(N, O) ≅ lim_{X_{!}k_{X}i_{X}^{r}N}^{r}(k_{X}i_{X}^{r}N)^{r}O (45)

Proof. For (42), by applying (32) of Proposition 6.2 we get

meets_{X}(P, Q) ≅ meets_{X}(P, Σ_{k_{X}Q}1_{X_{!}k_{X}Q}) ≅
≅ meets_{X_{!}k_{X}Q}((k_{X}Q)^{∗}P, 1_{X_{!}k_{X}Q}) ≅ coend_{X_{!}k_{X}Q}(k_{X}Q)^{∗}P

For (43), recalling Proposition 5.5 and using (38) of Proposition 6.2 we get:

ten_{X}(M, N) ≅ ten_{X}(M, ∃_{k_{X}i_{X}^{r}N}⊤_{X_{!}k_{X}i_{X}^{r}N}) ≅
≅ ten_{X}((k_{X}i_{X}^{r}N)^{ℓ}M, ⊤_{X_{!}k_{X}i_{X}^{r}N}) ≅ colim_{X_{!}k_{X}i_{X}^{r}N}^{ℓ}(k_{X}i_{X}^{r}N)^{ℓ}M

Similarly, the last two equations are obtained by applying (31) and (37):

hom_{X}(P, Q) ≅ hom_{X}(Σ_{k_{X}P} 1_{X_{!}k_{X}P} , Q) ≅
≅ hom_{X_{!}k_{X}P} (1_{X_{!}k_{X}P} , (k_{X}P)^{∗}Q) ≅ end_{X_{!}k_{X}P} (k_{X}P)^{∗}Q
nat_{X}^{ℓ}(L, M) ≅ nat_{X}^{ℓ}(∃_{k_{X}i_{X}^{ℓ}L}⊤_{X_{!}k_{X}i_{X}^{ℓ}L}, M) ≅
≅ nat_{X}^{ℓ}(⊤_{X_{!}k_{X}i_{X}^{ℓ}L}, (k_{X}i_{X}^{ℓ}L)^{ℓ}M) ≅ lim_{X_{!}k_{X}i_{X}^{ℓ}L}^{ℓ}(k_{X}i_{X}^{ℓ}L)^{ℓ}M

By applying (43) or (45) to the formulas for quantifications along a map f : X → Y of Corollary 7.3, we obtain a colimit and a limit formula for evaluation at y : 1 → Y of ∃_{f}^{ℓ}M (or ∃_{f}^{r}N) and ∀_{f}^{ℓ}M (or ∀_{f}^{r}N), respectively.

Say that a part P ∈ PX is “left dense” if its left closure is terminal: ♢_{X}^{ℓ}P ≅ ⊤_{X}^{ℓ}; right density is of course defined dually.

8.5. Proposition. A part P ∈ PX is left dense iff k_{X}P is final. A map f : X → Y in C is final iff c_{Y} f is left dense in Y. A space X ∈ C is connected iff Σ_{X}1_{X} is dense.

Proof. (Note that we implicitly use the canonical bijection between the objects of C/X and maps in C with codomain X.) For the first one we have:

♢_{X}^{ℓ}P ≅ ♢_{X}^{ℓ}Σ_{k_{X}P} 1_{X_{!}k_{X}P} ≅ ♢_{X}^{ℓ}Σ_{k_{X}P} i_{X_{!}k_{X}P}^{ℓ} ⊤_{X_{!}k_{X}P}^{ℓ} ≅ ∃_{k_{X}P}^{ℓ} ⊤_{X_{!}k_{X}P}^{ℓ}

and for the second one: ∃_{f}^{ℓ}⊤_{X}^{ℓ} ≅ ♢_{Y}^{ℓ} Σ_{f}1_{X} ≅ ♢_{Y}^{ℓ} c_{Y} f For the last one, see Remarks 8.2.

9. The sup and inf reflections

For X ∈ C, let \overline{X}^{ℓ} (resp. \overline{X}^{r}) be the full subcategory of LX (resp. RX) generated by the left (resp. right) slices (40), and denote the inclusion functors by

h_{X}^{ℓ} : \overline{X}^{ℓ} → LX  ;  h_{X}^{r} : \overline{X}^{r} → RX

The partially defined left adjoints to i_{X}^{ℓ}h_{X}^{ℓ}, i_{X}^{r}h_{X}^{r}, k_{X}i_{X}^{ℓ}h_{X}^{ℓ} and k_{X}i_{X}^{r}h_{X}^{r} are denoted respectively by:

sup_{X} : PX → \overline{X}^{ℓ} ; inf_{X} : PX → \overline{X}^{r}  ;  Sup_{X} : C/X → \overline{X}^{ℓ} ; Inf_{X} : C/X → \overline{X}^{r}

9.1. Remark. Of course, Sup_{X}f exists iff sup_{X}c_{X}f does, and in that case they are the same. Note also that the sup (resp. inf) of a part depends only on its left (resp. right) closure: sup_{X}P exists iff ♢_{X}^{ℓ}P has a reflection in \overline{X}^{ℓ}.

9.2. Proposition. The following are equivalent for a space X ∈ C:

1. X has a final point x : 1 → X;

2. there is a left dense part of X with a sup;

3. there is a final map T → X with a Sup;

4. id_{X} : X → X has a Sup.

Proof. By Proposition 8.5 and Remark 9.1, the last three conditions are equivalent. Since any point x : 1 → X has the slice X/x as its Sup, 1) implies 3).

Suppose conversely that a left dense part P ∈ PX has a sup; then by Remark 9.1 ♢_{X}^{ℓ}P ≅ ⊤_{X}^{ℓ} has a reflection X/x in \overline{X}^{ℓ}. By general well-known facts about reflections, it follows that also X/x ≅ ⊤_{X}^{ℓ}, that is the point x : 1 → X is final.

9.3. Proposition. [final maps preserve sups] Let t : S → T be a final map in C; then f : T → X has a Sup iff ft : S → X does, and in that case they coincide.

Proof. By Remark 9.1, it is enough to show that ♢_{X}^{ℓ}c_{X}ft ≅ ♢_{X}^{ℓ}c_{X}f:

♢_{X}^{ℓ}c_{X}ft ≅ ∃_{ft}^{ℓ}⊤_{S}^{ℓ} ≅ ∃_{f}^{ℓ}∃_{t}^{ℓ}⊤_{S}^{ℓ} ≅ ∃_{f}^{ℓ}⊤_{T}^{ℓ} ≅ ♢_{X}^{ℓ}c_{X}f

10. The logic of categories

Now we weaken the axioms for temporal doctrines so to include the motivating instance

⟨Set^{X^{op}} → Cat/X ← Set^{X} ; X ∈ Cat⟩

and show that most of the laws in Proposition 6.2 still hold. By restricting to groupoids we get another important instance of (symmetrical) weak temporal doctrine.

10.1. Weak temporal doctrines. Weak temporal doctrines are defined as temporal doctrines except that:

1. We do not require the existence of the Π_{f}, right adjoint to f^{∗}; instead we do require, for any map f : X → Y, the existence of

∀_{f}^{ℓ} : LX → LY  ;  ∀_{f}^{r} : RX → RY

right adjoint to f^{ℓ} and f^{r} respectively.

2. We do not assume that the categories of parts PX are cartesian closed, but only that they are cartesian and that the left or right closed parts are exponentiable therein, that is

i_{X}^{ℓ}M ⇒ P  ;  i_{X}^{r}N ⇒ P

always exist in PX.

In a weak temporal doctrine we still have the coend_{X} and end_{X} functors as in Section 6, left and right adjoint to:

i_{X}^{ℓ}X^{ℓ}j_{1}^{ℓ} = X^{∗}i_{1}^{ℓ}j_{1}^{ℓ} = X^{∗}i_{1}^{r}j_{1}^{r} = i_{X}^{r}X^{r}j_{1}^{r}

with the difference that, among the factorizatons of end_{X} in (30), only

(j_{1}^{ℓ})^{−1}∀_{X}^{ℓ}□_{X}^{ℓ} ≅ (j_{1}^{r})^{−1}∀_{X}^{r}□_{X}^{r} : PX → B1  (46)

are always available. We also define

meets_{X} : PX × PX → B1 ; hom_{X} : (PX)^{op} × PX → B1
ten_{X} : LX × RX → B1
nat_{X}^{ℓ} : (LX)^{op} × LX → B1 ; nat_{X}^{r} : (RX)^{op} × RX → B1

as in Section 6, but now the hom_{X} may be only partially defined, depending on whether the exponential P ⇒ Q exists or does not exist. On the contrary, the above axiom on exponentials assures that the nat_{X} are always defined.

The functors lim_{X}^{ℓ}, lim_{X}^{r}, colim_{X}^{ℓ} and colim_{X}^{r} are defined as in Section 7, and sup_{X}, Sup_{X}, inf_{X} and Inf_{X} as in Section 9.

That ⟨Cat/X; X ∈ Cat⟩, with the subdoctrines of discrete fibrations and discrete opfibrations (or, equivalently, of left and right actions), form indeed a weak temporal doctrine follows in particular from the following facts:

• Discrete (op)fibrations over X ∈ Cat are both reflective and coreflective in Cat/X (see [Pisani, 2007]).

• The reflections satisfy the mixed Frobenius laws, as a consequence of the reciprocal stability of the comprehensive factorization systems (as explained in [Pisani, 2008] and [Pisani, 2009]).

In this case, the sup (resp. inf) reflections give the colimit (resp. limit) of the corresponding functor. Thus Proposition 9.3 can be seen as the “external” correspective of Corollary 7.1.

10.2. Proposition. The functors nat_{X}^{ℓ} and nat_{X}^{r} enrich LX and RX respectively in B1 and, for any space X ∈ C or map f : X → Y, there are natural isomorphisms:

meets_{X}(f^{∗}Q, P) ≅ meets_{Y} (Q, Σ_{f}P) ; meets_{X}(P, f^{∗}Q) ≅ meets_{Y} (Σ_{f}P, Q) (47)
nat_{X}^{ℓ}(M, □_{X}^{ℓ}P) ≅ hom_{X}(i_{X}^{ℓ}M, P)  ;  nat_{X}^{r}(N, □_{X}^{r}P) ≅ hom_{X}(i_{X}^{r}N, P) (48)
ten_{X}(♢_{X}^{ℓ}P, N) ≅ meets_{X}(P, i_{X}^{r}N) ; ten_{X}(M, ♢_{X}^{r}P) ≅ meets_{X}(i_{X}^{ℓ}M, P) (49)
nat_{X}^{ℓ}(f^{ℓ}M, L) ≅ nat_{Y}^{ℓ} (M, ∀_{f}^{ℓ}L)  ;  nat_{X}^{r}(f^{r}O, N) ≅ nat_{Y}^{r} (O, ∀_{f}^{r}N)  (50)
nat_{X}^{ℓ}(L, f^{ℓ}M) ≅ nat_{Y}^{ℓ} (∃_{f}^{ℓ}L, M)  ;  nat_{X}^{r}(N, f^{r}O) ≅ nat_{Y}^{r} (∃_{f}^{r}N, O)  (51)
ten_{X}(L, f^{r}N) ≅ ten_{Y} (∃_{f}^{ℓ}L, N)  ;  ten_{X}(f^{ℓ}M, N) ≅ ten_{Y} (M, ∃_{f}^{r}N) (52)

Proof. The proofs of (47), (48), (49) and (52) are as in Proposition 6.2. For the other ones one can not use the technique of Proposition 6.2, since the functors Π_{f} are not always available. We get (50) by applying Proposition 2.2 to f^{ℓ} ⊣ ∀_{f}^{ℓ} and recalling that exponentials in LX are given by □_{X}^{ℓ}(i_{X}^{ℓ}L ⇒ i_{X}^{ℓ}M):

nat_{X}^{ℓ}(f^{ℓ}M, L) ≅ end_{X}(i_{X}^{ℓ}f^{ℓ}M ⇒ i_{X}^{ℓ}L) ≅ (j_{1}^{ℓ})^{−1}∀_{X}^{ℓ}□_{X}^{ℓ}(i_{X}^{ℓ}f^{ℓ}M ⇒ i_{X}^{ℓ}L) ≅

≅ (j_{1}^{ℓ})^{−1}∀_{Y}^{ℓ} ∀_{f}^{ℓ}□_{X}^{ℓ}(i_{X}^{ℓ}f^{ℓ}M ⇒ i_{X}^{ℓ}L) ≅ (j_{1}^{ℓ})^{−1}∀_{Y}^{ℓ} □_{Y}^{ℓ} (i_{Y}^{ℓ} M ⇒ i_{Y}^{ℓ} ∀_{f}^{ℓ}L) ≅ nat_{Y}^{ℓ} (M, ∀_{f}^{ℓ}L)

For (51), since we have adjunctions (with parameter L ∈ LX)

∃_{f}^{ℓ}(L ∧_{X}^{ℓ} X^{ℓ}j_{1}^{ℓ}(−)) ⊣ nat_{X}^{ℓ}(L, f^{ℓ}(−)) ; ∃_{f}^{ℓ}L ∧_{Y}^{ℓ} Y^{ℓ}j_{1}^{ℓ}(−) ⊣ nat_{Y}^{ℓ} (∃_{f}^{ℓ}L, −)

and since, by the restricted Frobenius law of Proposition 5.6,

∃_{f}^{ℓ}(L ∧_{X}^{ℓ} X^{ℓ}j_{1}^{ℓ}V) ≅ ∃_{f}^{ℓ}(L ∧_{X}^{ℓ} f^{ℓ}Y^{ℓ}j_{1}^{ℓ}V) ≅ ∃_{f}^{ℓ}L ∧_{Y}^{ℓ} Y^{ℓ}j_{1}^{ℓ}V

the result follows from Lemma 2.1.

10.3. Proposition. Whenever they are defined, there are natural isomorphisms:

hom_{X}(f^{∗}Q, P) ≅ hom_{Y} (Q, Π_{f}P)  ;  hom_{X}(P, f^{∗}Q) ≅ hom_{Y} (Σ_{f}P, Q) (53)
nat_{X}^{ℓ}(♢_{X}^{ℓ}P, M) ≅ hom_{X}(P, i_{X}^{ℓ}M)  ;  nat_{X}^{r}(♢_{X}^{r}P, N) ≅ hom_{X}(P, i_{X}^{r}N) (54)

Proof. We proceed as for (51), by showing that their left adjoints are isomorphic; for instance, for the second one of (53) we have adjunctions (with parameter P ∈ PX):

Σ_{f}(P ×i_{X}^{ℓ}X^{ℓ}j_{1}^{ℓ}(−)) ⊣ (j_{1}^{ℓ})^{−1}∀_{X}^{ℓ}□_{X}^{ℓ}(P ⇒ f^{∗}(−)) ; Σ_{f}P ×i_{Y}^{ℓ} Y^{ℓ}j_{1}^{ℓ}(−) ⊣ (j_{1}^{ℓ})^{−1}∀_{Y}^{ℓ} □_{Y}^{ℓ} (Σ_{f}P ⇒ −)

and using the Frobenius law:

Σ_{f}(P × i_{X}^{ℓ}X^{ℓ}j_{1}^{ℓ}V) ≅ Σ_{f}(P × X^{∗}i_{1}^{ℓ}j_{1}^{ℓ}V) ≅ Σ_{f}(P × f^{∗}Y^{∗}i_{1}^{ℓ}j_{1}^{ℓ}V) ≅ Σ_{f}P × i_{Y}^{ℓ} Y^{ℓ}j_{1}^{ℓ}V

Similarly, for (54) one uses the restricted Frobenius law.

10.4. Conclusions. All we have proved in sections 7, 8 and 9 depended only on the comprehension axiom and on the laws in Proposition 6.2. In propositions 10.2 and 10.3 we have seen that the same laws hold for weak temporal doctrines as well, as far as the functors hom_{X} involved are defined.

Thus, except for (44) of Proposition 8.4, in which hom_{X}(P, Q) may be not defined, those results hold in any weak temporal doctrine. (Note that the hom in the interior formula of Corollary 7.3 do exist, since the required exponentials are provided by the axioms for weak temporal doctrines).

In particular we get, for “generalized categories”, the Yoneda properties, the formulas for quantifications (or “Kan extensions”), the formulas for the (co)reflection in (left or right) “closed parts” (or “actions”), and the properties of final or initial maps with respect to (co)limits, both “internally” (Corollary 7.1) and “externally” (Proposition 9.3).

Thus we maintain that the logic of weak temporal doctrines well deserves to be called “a logic for categories”, in fact

1. being summarized by a few adjunction-like laws, it lends itself to effective and transparent calculations; furthermore, along with the obvious “left-right” symmetry, there is a far more interesting sort of duality: in many cases laws and proofs on the “hom-side” correspond exactly to those on the “tensor-side”;

2. this calculus allows one to easily derive some basic non-trivial categorical facts;

3. it is “autonomous”, providing its own truth values;

4. suitable natural strengthenings or weakenings can be considered, so to obtain more refined properties or a wider range of applications; some of them will be considered in a forthcoming work.

References

S. Ghilardi, G. Meloni (1991), Relational and Topological Semantics for Temporal and Modal Predicative Logics, Atti del Congresso: Nuovi problemi della Logica e della Filosofia della Scienza (Viareggio), CLUEB Bologna, 59-77.

P.T. Johnstone (2002), Sketches of an Elephant: A Topos Theory Compendium, Oxford Science Publications.

D.M. Kan (1958), Adjoint Functors, Trans. Amer. Math. Soc. 87, 294-329.

F.W. Lawvere (1970), Equality in Hyperdoctrines and the Comprehension Scheme as an Adjoint Functor, Proceedings of the AMS Symposium on Pure Mathematics, XVII, 1-14.

F.W. Lawvere (1989), Qualitative Distinctions between some Toposes of Generalized Graphs, Proceedings of the AMS Symposium on Categories in Computer Science and Logic, Contemporary Mathematics, vol. 92, 261-299.

C. Pisani (2007), Components, Complements and the Reflection Formula, Theory and Appl. Cat. 19, 19-40.

C. Pisani (2008), Balanced Category Theory, Theory and Appl. Cat. 20, 85-115.

C. Pisani (2009), Balanced Category Theory II, preprint, arXiv:math.CT/0904.1790v3.

via Gioberti 86, 10128 Torino, Italy.

Email: pisclau@yahoo.it

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/24/15/24-15.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Cuill Inc.: valeria@cuill.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Glasgow, Tom.Leinster@glasgow.ac.uk Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca