The n-Category Café

Hi David,

if possible, let’s look at a bunch of baby-examples to get a feeling for what internal $(\infty,1)$-logic is like. I have currently little idea, beyond some vague general statements.

A while ago, I started spelling out at internal logic – In $Set$ the following baby exercise in ordinary internal logic:

Baby exercise. Rephrase all of standard logic from the internal point of view as the logic internal to the topos $Set$.

I didn’t take the time to drive this very far there, just stated very explicitly for the record how the primitive logical operations arise from limits, colimits and internal homs in $Set$. This is tautological to everyone who ever thought about it, but not to everyone who never thought about it. So it’s good to think about it once. :-)

If possible, let’s do the following: let’s go step-by-step through the notes as at the above link, and translate it all into the analogous constructions with $Set$ replaced by $\infty Grpd$. What the abstract constructions in terms of limits, colimits and internal homs are is clear, but let’s think a bit about what this now means as we look at it from the point of view of $\infty$-logic.

Then when we have discussed the $(1 \mapsto (\infty,1))$-translation of the stuff at the above link, let’s go further and look at the corresponding translation of more nontrivial constructions in internal logic.

$(\infty,1)$-Baby exercise. Translate step-by-step the above baby exercise from the 1-topos $Set = (0,0)Cat$ to the $(\infty,1)$-topos $\infty Grpd = (\infty,0)Cat$.

Here is a piece of scratch paper for everyone who wants to give it a try.

Does that sound like a good plan to get a foot on the ground here?

As we said, the next thing we want to get hold of is the object classifier in $\infty Grpd$

I have now added the relevant definitions and propositions to object classifier.

Then in the query box there, I develop a bit further the thoughts about the object classifier in $\infty Grpd$ for given cardinality bound $\kappa$.

I think we had stated the basic idea several times before, as archived for instance at generalized universal bundle as well as at stuff, structure, property:

the (relatively $\kappa$-compact) object classifier in $\infty Grpd$ is the corresponding universal op-fibration in $\infty$-groupoids

$$\array{ Core(Z|_{\infty Grpd_{\leq \kappa}}^{op}) \\ \downarrow \\ Core(\infty Grpd_{\leq \kappa}) }$$

I’ll suppress the core in the following, notationally.

Now, by the $(\infty,1)$-Grothendieck construction we know that $\infty$-functors $X \to \infty Grpd$ classify $\infty$-Grothendieck op-fibrations in $\infty$-groupoids over $X$.

But since $X$ is itself an $\infty$-groupoid, every $\infty$-functor out of another $\infty$-groupoid into it will be such. Use for instance HTT, prop. 3.3.1.8, which says that every coCartesian fibration over a Kan complex – and our op-fibration in $\infty$-groupoids = left Kan fibration is one – is equivalently a categorical fibration: but every morphism of simp-sets $E \to X$ factors as an equivalence followed by a categorical fibration.

I prefer to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing subobjects. For instance, limits and colimits, exponentials, and object classifiers belong to the type theory, while images, dual images, intersections, unions, and subobject classifiers belong to the logic.

Some further explanation of this distinction is at type theory, along with remarks on the natural semantics. The semantics of (extensional) type theory naturally lies in a category with certain category-theoretic structure like limits, colimits, and exponentials, while the semantics of logic over that type theory naturally lies in some indexed poset over that category. We commonly take the indexed poset to consist of the subobjects in the category in question, in which case additional “logical” structure on the category is required.

In an elementary 1-topos, all of the “logical” structure is not usually included in the definition, because it comes for free once you have power objects. But I don’t know whether object classifiers are as powerful as power objects in this respect – I suspect not. So I think that for purposes of studying the internal logic (and not just the internal type theory) of an $(\infty,1)$-topos, we should include both the type-theoretic structure and the logical structure, and in particular we should consider both the object classifier and the subobject classifier. I’ll write more about how I think these should go in a bit.

(Confusing the whole issue is the “propositions as types” viewpoint according to which one uses objects to describe logic as well as type theory. Categorically, this corresponds to studying the logic of a free exact completion.)

I think talking about “logic of space” is a bit misleading, since the use of “space” in a statement like “spaces model $\infty$-groupoids” is fairly different from its use in, for instance, the theory of “space and quantity.” For instance, to take your example, the interval $[0,\infty)$ is contractible, and thus as an $\infty$-groupoid it is the same as the terminal object. So the internal logic of $\infty Gpd$ won’t tell you much about temperature. You could look at an $(\infty,1)$-topos of sheaves on some space, but you could also look at a 1-topos of sheaves on the same space, and you might learn just as much about temperature from the latter.

I have now added most of what I know and think about type theory and logic in an $(\infty,1)$-topos to the nLab page internal logic of an (∞,1)-topos.

I’ve been trying to think of things we could say in $(\infty,1)$-logic that would have a useful meaning in an $(\infty,1)$-topos, but at the moment I’m kind of blocked by not yet knowing enough about what one does in an $(\infty,1)$-topos. This is entirely my own fault and something I can and should rectify.

But for the moment, starting by analogy, one of the most basic things about 1-logic in a 1-topos is that a morphism $f\colon A\to B$ is an epimorphism if and only if the statement “for every $b\in B$ there exists an $a\in A$ with $f(a)=b$” is true in the internal logic. Similarly, in a 2-topos, $f$ is a “strong 1-epic” iff the statement “for every $b\in B$ there exists an $a\in A$ with $f(a)\cong b$” is true in the internal 2-logic. I presume something similar will be true in an $(\infty,1)$-topos for the appropriate sort of epimorphism.

We also have a similar characterization of monomorphisms: $f$ is monic in a 1-topos iff “whenever $f(a_1)=f(a_2)$, then $a_1=a_2$” is true internally. Similarly, in a 2-topos we can characterize the 1-monics, aka fully-faithful maps, by “every arrow $f(a_1)\to f(a_2)$ is the image of a unique arrow $a_1\to a_2$”. But I’m less sure about the right thing to say in an $(\infty,1)$-topos; here it seems like we might need infinitely many statements in the internal logic to characterize the monomorphisms.

I’m also starting to worry about whether hypercompleteness, or lack thereof, is going to rear its head at some point.