I am researching Topos theory and realizability, I was wondering if anyone saw or has a reference to a Topos/Tripos formalization in coq. What I am looking for specifically is the tripos to topos construction in Coq. ]]>

I am interested in Urs Schreiber’s work like “Differential cohomology in a cohesive infinity-topos”. But to study these huge works is a long-term project, I think is a good idea to study together. I recently joined one like that for Exodromy. It’s pretty nice, I learn a lot of higher topos from this. So I think we can have more like this.

Maybe some experts can give a “road map”, and learners can give talks on Zoom each week according to those materials. One benefit of holding online is it can last for a long period(year-long) so that we can have time to work on some pre-required things. And such a working group could encourage people to insistent study on this.

]]>We know Finset is a topos, but is not a model of ETCS since it does not have a natural number object.

Is there any smart way of defining product/coproduct/exponential on the subcategory of **Sets** whose collection of object is collection of all sets of natural numbers (and therefore includes itself, so it is like joining a NNO to the category of finite sets), so it becomes a model of ETCS?

If it is not possible, I simply want a smaller model of ETCS which is not the category **Sets**.

If such a model does not exists, is there any proof that relevant to the fact that there is no subtopos of **Sets** which is a model of ETCS?

It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\mathbb N\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

I think the statement of strong induction to prove is as the following.

For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

]]>I am reading the following document about Lawvere’s ETCS:

http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf

My question is about Theorem 6 in this document. The aim is to prove an equivalence relation is an equalizer. On page 29, the author says:

Finally we can assert our theorem (I think the $a_0q = a_1g$ in the link is a typo.) $a_0q = a_1q$ iff $a_0 \equiv a_1$.

And finished the proof.

That is, the author proves for every element $\langle a_0,a_1\rangle$ from the terminal object $1$, we have the split via the map which we want to prove to be an equalizer. But to prove the equalizer result, we need that we still have the factorization when $1$ is replaced by any arbitrary object. I know that $1$ is the generator in ETCS, and have trouble working out the proof that the existence of factorization for $1$ implies the existence of factorization for any $T$. I tried taking the elements of $T$, and unable to construct a factorization from $T$ from the factorization for its elements.

Any help, please? Thank you!

Note: If someone is reading the link above, then please note that the composition is written as: if $f: A \to B,g: B\to C$, then the author will write $fg$ to denote the composition of $f$ of $g$, rather than $g \circ f$.

]]>While concentrating on Category Theory as applied to the Web, I have also been following French Philosopher of technology Bernard Stiegler, as he was supportive of the creation of the Philosophy of the Web conference 10 years ago.

Recently he has been looking at the concept of locality which he argues has been repressed mostly after Aristotle, being overtaken since Plato with the notion of the Universal (The world of ideas), transferred into the Philosophers notion of God. Those philosophers who have tried to bring Locality back, such as Heiddegger with his concept of Dasein (being here), or Japanese philosopher Kitaro Nishida concept of place as a departure point, have had problematic relations with the Axis powers during the second world war. Yet Stiegler believes that since Schroedinger’s development in What is Life? of the concept of negative entropy as what fights *locally* entropy, forces us, if we are to take this seriously, to give a central position to locality. In any case the Web and the Internet create tensions between local cultures due to its creating ” a topological space without any distances” (see interview of late Michelle Serres).
I’ll see if I can find a good English paper of Stiegler that makes these connections clearly.

Now the Topos meant place in Ancient Greek (or see also Topoi on Topos: The Development of Aristotle’s Concept of Place). So I was wondering if people here who had deeper intutions about Category Theory than me, can see some insights that Category Theory can bring on these topics. Of course I bring this up here as Topos is also an essential concept in Category Theory which I believe one can summarise as the allowing one to connect logic and topology.

Perhaps modal logic captures this relation to location better. David Corefield in his published Chapter 4 on Modal HoTT writes of adjoint modalities:

]]>Choosing q equal to p, we see that a proposition sits between the images of the two operators (◻︎, p, ◇):

- necessarily true, true, possibly true following the pattern of
- everywhere, here, somewhere.

finally created *intensive and extensive* with the topos-theoretic formalization following the concise statement in the introduction of *Categories in Continuum Physics*

Quickly generated free topos. Mostly references.

]]>Some while ago we discussed using the English terms “little topos” and “big topos” when writing in English instead of the French “petit” and “gros”. I don’t recall any objections being raised, so I took the initiative to move petit topos to big and little topos as I did some expansion of it. (The floor is still open for objections, of course.)

]]>I was in the differential cohesion group at the HOTT MRC last week and one thing we struggled with was that we only knew one model (sheaves over formally thickened Cartesian space) which is pretty complicated to construct. Also this specific model has extra properties so not all of the axiomatics can really be explained with just one model, for instance Felix told me that every object in this topos is formally smooth.

Plain cohesion, on the other hand, has some very elementary toy models like reflexive graphs and the sierpinski topos that are very nice for getting intuition.

Do we have any analogous toy models for differential cohesion? All the better if they are “thickenings” of sierpinski or reflexive graphs. Ideas are also welcome, I’d be happy to work through some details myself.

]]>It’s well known that the category of points of the presheaf topos over $Ring_{fp}^{op}$, the dual of the category of finitely presented rings, is the category of all rings (without a size or presentation restriction). In fact this holds for any algebraic theory, not only for the theory of commutative rings. One can learn about this in our entries on *Gabriel-Ulmer duality*, *flat functors*, and Moerdijk/Mac Lane.

But what if we don’t restrict the site to consist only of the compact objects? What are the points of the presheaf topos over the large category $Ring^{op}$, to the extent that the question is meaningful because of size-related issues? What are the points of the presheaf topos over $Ring_{\kappa}^{op}$, the dual of the category of rings admitting a presentation by $\lt \kappa$ many generators and relations, where $\kappa$ is a regular cardinal? (The category $Ring_{\kappa}^{op}$ is essentially small, so the question is definitely meaningful.)

The question can be rephrased in the following way: What is an explicit description of the category of *finite* limit preserving functors $F : Ring_{\kappa}^{op} \to Set$? Any such functor gives rise to a ring by considering $F(\mathbb{Z}[X])$, but unlike in the case $\kappa = \aleph_0$ such a functor is not determined by this ring.

This feels like an extremely basic question to me; it has surely been studied in the literature. I appreciate any pointers! Of course I’ll record any relevant thoughts in the lab.

]]>FYI. Interesting suggestion on MO to collect references about the elephant part 3 on the nlab.

]]>The (0,1)-category page says that a (0,1)-category “with the structure of a Grothendieck topos” is a locale, and a (0,1)-category “with the structure of an elementary topos” is a (complete?) Heyting algebra.

I am trying to understand the formal content of these statements. By the Giraud characterization of Grothendieck toposes, I could believe that (0,1)-categories which happen to be “Giraud toposes” (i.e., Grothendieck toposes) are locales. Running through the Giraud axioms, we have:

- “a locally small category with a small generating set” - should be true for any (0,1)-category
- “with all finite limits” - this means all finite meets for a (0,1)-category, which locales have
- “with all small coproducts, which are disjoint, and pullback stable” - for a (0,1) category, all small coproducts are small/infinitary disjunctions, and pullback stability corresponds to the “frame distributivity” rule which holds for locales, which says that binary meets distribute over joins. I’m not sure about the “disjoint” condition, though.
- “where all congruences have effective quotient objects, which are also pullback-stable.” I don’t understand.

But it does not seem that a (0,1)-category which is also an elementary topos is a complete Heyting algebra. The issue is that there is no subobject classifier. One reasons that the subobject classifier must be the terminal object of the cHa (it would be necessary to have a map into the subobject classifier from any object), but then since the pullback of every iso is an iso, every object must be the terminal object (Top), so the category is made only of terminal objects.

Is it in fact the case that a (0,1)-category which is a Grothendieck topos is a locale? And is there any *formal* way to view complete Heyting algebras as decategorified elementary toposes?

Let $\mathbf{C}$ be a small category and let $\mathbf{E}$ be a locally small and cocomplete category. For the purposes of this discussion, I am defining a **flat functor** to be a functor $A : \mathbf{C} \to \mathbf{E}$ such that the induced functor $(-) \otimes_\mathbf{C} A : \widehat{\mathbf{C}} \to \mathbf{E}$ is left exact. Now, when $\mathbf{E} = \mathbf{Set}$, I know this is equivalent to the definition given in the nLab article flat functor: the comma category $(1 \downarrow A)$ is cofiltered if and only if $A$ is flat in the above sense (and I guess this extends without problems to the case $(E \downarrow A)$ for a general set $E$). This is Theorem 3 in [*Sheaves and Geometry and Logic*, Ch. VII, §6]. The article also asserts that, when $\mathbf{E}$ is a topos, if $A$ is representably flat, then $A$ is flat in the above sense. This seems dubious, since we should at least take $\mathbf{E}$ to be a locally small and cocomplete topos (e.g. a Grothendieck topos). Regardless, assuming $\mathbf{E}$ is a sufficiently nice topos, is the converse true? That is, if $A$ is flat, is $A$ representably flat? For some reason Mac Lane and Moerdijk phrase everything internally in terms of $\mathbf{E}$ in [Ch. VII, §8], and the claim that comes closest is Lemma 4.

Ultimately though, what I want to know is this: when $\mathbf{C}$ is a finitely complete category and $\mathbf{E}$ is a locally small cocomplete topos, are

- $A$ being a flat functor
- $A$ being a representably flat functor
- $A$ being left exact

all equivalent? For the case $\mathbf{E} = \mathbf{Set}$, Mac Lane and Moerdijk prove (1) ⇒ (3) ⇒ (2) ⇔ (1), and I can see that (1) ⇒ (3) ⇒ (2) hold even when $\mathbf{E}$ is only assumed to be a locally small and cocomplete *category*. The troublesome step is (2) ⇒ (1), which the nLab article asserts is true but gives no reference for…

I have listed today’s arXiv preprint

- Marco Benini, Alexander Schenkel,
*Poisson algebras for non-linear field theories in the Cahiers topos*, arxiv/1602.00708

at variational calculus despite the title, as it seems that the construction of presymplectic current after Zuckerman’s idea on geometry of variational calculus is very central to the paper.

]]>Here’s a question (possibly naive) I have about the smooth infinity topos, which I’ll call $E$. (I guess I could ask this on MathOverflow, but anyone who is likely to know is probably here.)

I’ll write $T$ for infinity-groupoids, and $\Pi\colon E\to T$ for the functor left adjoint to the one sending a space $X$ to the constant simplicial sheaf with value $X$. I’ll identify the category $Man$ of smooth manifolds with a full subcategory of $E$; thus, $\Pi$ sends a manifold to its homotopy type.

Being an infinity topos, $E$ has (derived) internal function objects, which I’ll write as $[X,Y]$. The question is: if $M$ and $N$ are manifolds, is $\Pi[M,N] \approx [\Pi M,\Pi N]$, the latter being the derived mapping space in $T$?

It’s certainly true if $M=\mathbb{R}^k$, since $[\mathbb{R}^k,N]$ is “$\mathbb{R}$-homotopy equivalent” to $N$, and $\Pi$ inverts $\mathbb{R}$-homotopy equivalence.

]]>There’s quite a bit on the $n$-lab about effective epimorphisms in $\infty$-toposes, so maybe I’m just not putting it together correctly, but I’m wondering if anyone here knows if there’s a characterization (in print somewhere, preferably) of effective epimorphisms for $A_\infty$-ring spectra. In particular, I suspect there should be some kind of statement like: For $f:A\to B$, a morphism of connected $A_\infty$-ring spectra, we can recover $A$ from the Amitsur complex (dually, the Cech nerve) of $f$ as long as $\pi_0(f)$ is an isomorphism and $\pi_1(f)$ is a surjection.

This sort of statement is proven by Gunnar Carlsson in the context of what he calls “derived completion” but he works with the $S$-algebra framework of Elmendorf, Kriz, May and Mandell, and it seems like it should be a much more general topos theoretic statement for an $\infty$-topos. Incidentally, has anyone written down anything about the topos of $A_\infty$-ring spectra at all? At first glance it seems like most of Lurie’s work on the subject is for $E_\infty$-rings.

Thanks! Jon

]]>I changed the definition at logical functor, as it said that such a thing was a cartesian functor that preserved power objects. The page cartesian functor says

A strong monoidal functor between cartesian monoidal categories is called a cartesian functor.

which really is only about finite products, not finite limits as Johnstone uses, which I guess is where the definition of logical functor was lifted from. So logical functor now uses the condition ’preserves finite limits’.

So I added a clarifying remark to cartesian functor that the definition there means finite-product-preserving, and that the Elephant uses a different definition.

However, people may wish to have cartesian functor changed, and logical functor put back how it was. I’m ok with this, but I don’t like the terminology cartesian (and I’m vaguely aware this was debated to some extent on the categories mailing list, so I am happy to go with whatever people feel strongest about).

]]>I have noticed the following error in the categorification of a local homeomorphism of spaces into a concept of a local homeomorphism of <latex>n</latex>-topoi. I have a suspicion that it must have been noticed before (at least for <latex>1</latex>-topoi), and if this is true, please view this discussion, in particular, as a reference request.

**Background**

For a topological space <latex>X,</latex> if <latex>F</latex> is a sheaf, it has an \‘etal\‘e space <latex>Y_F \to X</latex> which is a local homeomorphism over <latex>X,</latex> and sections of it are exactly the sheaf <latex>F.</latex> The \‘etal\‘e space construction yields an equivalence of categories

<latex>Sh\left(X\right) \simeq Et/X</latex> between the category of sheaves on <latex>X</latex> and the category of local homeomorphisms over <latex>X.</latex> Moreover, assuming <latex>X</latex> is sober, since sober topological spaces embed fully faithfully into topoi, for a sheaf <latex>F,</latex> <latex>Y_F \to X</latex> corresponds to a geometric morphism <latex>Sh(Y_F) \to Sh(X)</latex> and there turns out to be an equivalence of topoi <latex>Sh(Y_F) \simeq Sh(X)/F</latex> under which this geometric morphism is equivalent to the one induced by slicing: <latex>Sh(X)/F \to Sh(X).</latex>

Using this as an example, topos theorists said that a geometric morphism of <latex>1</latex>-topoi <latex>\mathcal{F} \to \mathcal{E}</latex> is **\‘etale** if it is equivalent to one of the form <latex>\mathcal{E}/E \to \mathcal{E},</latex> and this was to be a ``local homeomorphism’‘ of <latex>1</latex>-topoi.

**The Problem**

Define an \‘etale geometric morphism of <latex>n</latex>-topoi the same way, i.e.

<latex>\mathcal{F} \to \mathcal{E}</latex> is **\‘etale** if it is equivalent to one of the form <latex>\mathcal{E}/E \to \mathcal{E}.</latex>

Now let <latex>X</latex> be a (sober) topological space. In particular, it is a locale, hence a <latex>0</latex>-topos in the sense of Lurie. Lets write this <latex>0</latex>-topos by <latex>O(X)</latex> (as it is in fact the lattice of opens of <latex>X.</latex>) The maps of locales that are induced by slicing are exactly those which correspond to inclusions of open sublocales. So, an \‘etale map of <latex>0</latex>-topoi does not correspond to a local homeomorphism (but it is a particular kind of local homeomorphism).

You might ask: So what? Maybe this is just a defect for <latex>n=0.</latex>

No, this persists. An <latex>\infty</latex>-topos <latex>\mathcal{X}</latex> is **<latex>n</latex>-localic** if it is equivalent to <latex>\infty</latex>-sheaves on an <latex>n</latex>-site. There is a functor from <latex>n</latex>-topoi to <latex>\infty</latex>-topoi which is fully faithful and whose essential image is <latex>n</latex>-localic <latex>\infty</latex>-topoi, and if <latex>\mathcal{X}</latex> is an <latex>n</latex>-localic, the <latex>n</latex>-topos which is corresponds to is the <latex>\left(n,1\right)</latex>-category of <latex>\left(n-1\right)</latex>-truncated objects of <latex>\mathcal{X}.</latex>

Moreover, if <latex>X</latex> is an object of an <latex>\mathcal{X},</latex> then <latex>\mathcal{X}/X</latex> is also <latex>n</latex>-localic **if and only if** <latex>X</latex> is <latex>n</latex>-truncated. So let <latex>X</latex> be an object of <latex>\mathcal{X}</latex> which is <latex>n</latex>-truncated but not <latex>\left(n-1\right)</latex>-truncated. Then the \‘etale map of <latex>\infty</latex>-topoi <latex>\mathcal{X}/X \to \mathcal{X}</latex> is a morphism between <latex>n</latex>-localic <latex>\infty</latex>-topoi. Let <latex>\mathcal{F}</latex> denote the <latex>n</latex>-topos associated to <latex>\mathcal{X}/X</latex> and <latex>\mathcal{E}</latex> the one associated to <latex>\mathcal{X}.</latex> Since <latex>n</latex>-topoi embed fully faithfully into <latex>\infty</latex>-topoi as <latex>n</latex>-localic <latex>\infty</latex>-topoi, this \‘etale map induced by <latex>X</latex>

must correspond to a geometric morphism <latex>\mathcal{F} \to \mathcal{E}.</latex> However, it cannot be an \‘etale map of <latex>n</latex>-topoi, since the object <latex>X</latex> is not <latex>\left(n-1\right)</latex>-truncated. Nonetheless, such a geometric morphism is the “correct” notion of a local homeomorphism since if we let <latex>n=0</latex>, this is a local homeomorphism of locales, in the usual sense.

Any comments? Has this been noticed for <latex>1</latex>-topoi and is there a name for such geometric morphisms (and is there a characterization of them internal to <latex>1</latex>-topoi?)

]]>This question on MO made me realize that I don’t even know the right definition of surjective geometric morphism for $(\infty,1)$-toposes. For 1-toposes, it is equivalent for $f^*$ to be (1) comonadic, (2) conservative, and (3) faithful. Of course (2)⇔(3) doesn’t categorify (what does faithfulness even mean for (∞,1)-categories?). But I don’t see that (1)⇔(2) categorifies either, because the (∞,1)-comonadicity theorem (unlike the 1-categorical one) is not about *finite* limits, but $f^*$ is still only assumed to preserve finite limits.

Of course we want a (surjection, inclusion) factorization. For that, it seems almost certain that $f^*$ being conservative is the right definition, at least if we take the obvious definition of “inclusion” as $f_*$ being fully faithful. We can then produce the desired factorization of $f: \mathcal{F} \to \mathcal{E}$ by localizing $\mathcal{E}$ at the class of morphisms inverted by $f^*$.

But what happens if instead we construct the category of coalgebras of the comonad $f^* f_*$? Is the category of coalgebras of an (accessible) lex comonad on an $(\infty,1)$-topos again an $(\infty,1)$-topos? If so, what sort of factorization does this produce?

]]>Let $\mathcal{Z}$ be the Zariski topos, in the sense of the classifying topos for local rings. I was wondering whether there might be any connection between $\mathbf{Sh}(\operatorname{Spec} \mathbb{Z})$ and $\mathcal{Z}$. Certainly, there is a geometric morphism $\mathcal{Z} \to \mathbf{Sh}(\operatorname{Spec} \mathbb{Z})$, and there’s also a geometric inclusion $\mathbf{Sh}(\operatorname{Spec} \mathbb{Z}) \to \mathcal{Z}$. On the other hand, there’s no chance of $\mathcal{Z}$ itself being localic, since it has a proper class of (isomorphism classes of) points. Let’s write $L \mathcal{Z}$ for the localic reflection of $\mathcal{Z}$; the first geometric morphism I mentioned then corresponds to a locale map $L \mathcal{Z} \to \operatorname{Spec} \mathbb{Z}$. But what is $L \mathcal{Z}$ itself?

The open objects in $\mathcal{Z}$ can be identified with certain saturated cosieves on $\mathcal{Z}$ in the category of finitely-presented commutative rings, and so may be identified with certain sets of isomorphism classes of finitely-presented commutative rings. If I’m not mistaken, every finitely-presented commutative ring gives rise to an open object in $\mathcal{Z}$. This suggests that $L \mathcal{Z}$ might be some kind of (non-spatial) union of all isomorphism classes of affine schemes of finite type over $\mathbb{Z}$, which is an incredibly mind-boggling thing to think about. It’s not clear to me whether other kinds of open objects exist. For example, does every not-necessarily-affine open subset of $\operatorname{Spec} A$, for every finitely-presented ring $A$, also show up…?

]]>I’m a little confused by the remarks about induced coverages in Section C2.2 of the Elephant. Consider the poset $\{ a, b, c, d \}$ with $b \lt a$, $c \lt a$, $d \lt a$, $d \lt c$, and let $J$ be the Grothendieck topology given by:

$J(a) = \{ \{ b \}, \{ b, d \}, \{ b, c, d \}, \{ a, b, c, d \} \}$ $J(b) = \{ \{ b \} \}$ $J(c) = \{ \emptyset, \{ d \}, \{ c, d \} \}$ $J(d) = \{ \emptyset, \{ d \} \}$Now, consider the non-full subcategory with the same objects but only the relations $b \lt a$, $c \lt a$, $d \lt a$. As I understand it, the induced coverage $K$ takes the form below:

$K(a) = \{ \{ b \}, \{ b, d \}, \{ b, c, d \}, \{ a, b, c, d \} \}$ $K(b) = \{ \{ b \} \}$ $K(c) = \{ \emptyset, \{ c \} \}$ $K(d) = \{ \emptyset, \{ d \} \}$But this is not a Grothendieck topology, since K(a) fails to be a filter. Have I misunderstood something?

It seems that some care is required when constructing the induced topology when the subcategory is non-full: in this case, what happens is that every sieve on $a$ in the parent category either contains both $c$ and $d$ or not at all, but there are sieves on $a$ on the subcategory which only contain one of $c$ or $d$ but not both.

]]>Every category – indeed, every simplicial set – admits a homotopy final functor into it out of a Reedy category, namely its category of simplices (HTT 4.2.3.14). This makes me wonder: can every $(\infty,1)$-topos be presented as a localization of an $(\infty,1)$-topos of presheaves on a Reedy category?

]]>There seems to be a small mistake in the current article for the Mitchell-Bénabou language. At the moment, it states

the

variablesof type $A$ are the morphisms $x : 1 \to A$ in $E$;

I’m not claiming to fully understand the matter, but I think this is mistaken:

- What if $A$ has no global elements? For instance, $A$ could be a strict subobject of $1$ in the topos of sheaves over a topological space.
- But ignoring the issue of having enough global elements, this seems to be
*identifying*variables with (generalised) elements of an object. Shouldn’t variables simply be formal symbols, which are interpreted as, well, varying elements? My main point is that we would like an unlimited supply of variables for each type and directly identifying variables with elements hinders this. (On the other hand, I think the quote, exactly as it stands, is a perfectly good definition of a*constant*.) - Finally, an appeal to authority: Mac Lane and Moerdijk [1994, p. 298] say that variables of type $X$ are to be interpreted as the identity arrow $1 : X \to X$.

Having broached the topic, I’d like to ask for some opinions on a couple of matters:

Firstly, is it worth trying to separate the syntactic and semantic sides of the Mitchell–Bénabou language? At the moment the article, like the corresponding section of *Sheaves in Geometry and Logic*, develops the formal language and its ‘canonical’ semantics (if I may coin a term) simultaneously. I feel this is confusing. (The first time I read about the Mitchell–Bénabou language, I got the impression that the canonical semantics were the *only* way to interpret it. This led to problems when I tried to play with even the simplest of non-trivial examples.)

Secondly, where *should* the division between the Mitchell–Bénabou language and Kripke–Joyal semantics be? The point of Kripke–Joyal semantics, as I understand it, is that it is easier to work with than the canonical semantics but is otherwise equivalent to it. Again, I don’t quite agree with the way Mac Lane and Moerdijk treat the subject: I think that the conclusions of Theorem VI.6.1 should be presented as *definitions* (with additions so as to give a fully inductive definition from the atomic terms), if only so that the definition of the ‘forcing’ relation $\Vdash$ would not have to be given in terms of canonical semantics.