it's in my PhD thesis

(This is exaggerated: only a small part of that in my thesis. But the part where the topology matters is.)

]]>@Toby: I’m glad you agree!

]]>The right context in which to talk about an “internal $n$-category” is a unary $(n+1)$-site, and in that case the meaning of “internal $n$-category” is “object of the $(n+1)$-exact completion”.

Yes, this is true; it’s in my PhD thesis. They’ll take my degree away if I stop believing this.

An $(n+1)$-exact $(n+1)$-category should be its

ownexact completion regarded as a unary $(n+1)$-site with its $(n+1)$-exact topology, while the free $(n+1)$-exact completion of any category corresponds to starting with a trivial topology.

This should settle all discrepancies; it’s just a question of which topology we’re using.

But it does make things more complicated.

]]>Cf. the definition of natural transformation between strict categories.

]]>So if we say “internal groupoid” means “type with atlas/type with type of objects”, then it becomes true again that “groups are equivalent to the one-objects internal groupoids” .

I’m not so sure about that. Even when we define “internal groupoids” in a 1-topos in the most classical way — which are then equivalent to 1-truncated objects of the corresponding $(\infty,1)$-topos equipped with a 0-truncated cover — and take the morphisms between them to be those that preserve the specified covers (hence internal functors in the classical sense, rather than anafunctors), no one ever requires the natural transformations between them to also preserve the covers (which would reduce them all to triviality).

]]>The discussion here suggests that the term for “smooth groupoid with xyz-structure” should be something like “0-strict smooth groupoid”.

]]>One more comment, after all (I never listen to myself, it seems ;-)

Whatever the answer is in these matters here, it’s probably good to keep in mind the case for *groups*. The fact that $Grp(\mathbf{H})$ is the collection of *pointed* connected objects is of course related to those atlases: that point is the “minimal” atlas of a connected object.

So if we say “internal groupoid” means “type with atlas/type with type of objects”, then it becomes true again that “groups are equivalent to the one-objects internal groupoids” .

Not sure what this implies. Last thought for tonight on this.

]]>re #19: thanks for taking the time to share this. I sure appreciate the reasoning there. What I am not sure yet is to which extent this answers the question of what an internal anything is *in homotopy type theory* or just reformulates that in different terms.

I’ll like to continue discussing this. It’s clearly of profound importance. But for tonight I should stop. I badly need to look into something else right now.

]]>I have no problem with the idea that being “etale” is a structure rather than a property.

Not sure what to make of that. Need to think about whether I would agree with this.

But let’s look at Lie differentiation, where the case is more clear-cut: what is called a “bisection” of a Lie gorupoid is – the atlas $U \to X$ understood – an equivalence

$\array{ U &&\stackrel{\simeq}{\to}&& U \\ & \searrow &\swArrow& \swarrow \\ && X }$The “Lie-Rinehart”-presentation of the Lie algebroid of $X$ (hence really of $U \to X$) is the pair $(U, Aut(U)_X)$.

(Also in the more popular description of Lie algebroids via vector bundles over $U$, this $U$ is fixed).

So Lie differntiation of a Lie groupid means and always meant (though people don’t say this): of a Lie groupoid with atlas.

With your proposal, there would be no way to say “To a smooth groupoid we can associate its Lie algebroid.” Instead we would have to say “To each way of equipping a smooth groupoid with xyz-structure we can assign a Lie algebroid.”

(Having said all this: of course I myself kept and keep saying “smooth $\infty$-groupoid” for an object of $Sh_\infty(SmthMfd)$. But I feel something needs to be done about the terminology. Smooth homotopy type is probably better.)

]]>Re: #17, I have no problem with the idea that being “etale” is a structure rather than a property.

]]>I would argue that in an $(\infty,2)$-topos, the right notion of “internal $(\infty,1)$-category” *would* be just “object”. It’s only when our ambient category is insufficiently endowed with higher morphisms that we have to recourse to building things more explicitly.

Let me try to be more precise about what I think is going on. I would argue that in an $(n+1)$-exact $(n+1)$-category, the right notion of “internal $n$-category” is “object”. (Here $n$ could be $1$, $2$, $(\infty,1)$, $(\infty,2)$, etc.) But if you happen to *not* be in an $(n+1)$-exact $(n+1)$-category, then this doesn’t make sense. So what people often do is pass to the *free* $(n+1)$-exact $(n+1)$-category generated by whatever category you started with (a.k.a. its $(n+1)$-exact completion), and call the objects of *that* “internal $n$-categories” in the category you started from.

In particular, the objects of the free 1-exact 1-category generated by a regular 1-category are precisely the internal equivalence relations, and the objects of the free 1-exact 1-category generated by a 1-category with finite limits are the ’pseudo-equivalence relations’ (equivalence ’relations’ that might not be monic). The latter, by the way, are I believe what people working in MLTT usually call ’setoids’, not the former. This is logical because in the absence of bracket types, the category of contexts in type theory is not regular.

Unfortunately, the formal theory of $n$-exact completion for $n\gt 1$ doesn’t exist yet. But I am pretty confident that, for instance, the objects of the free 2-exact 2-category generated by a 1-exact category will be the internal categories therein, in the classical sense. (Its morphisms will be anafunctors.)

Of course there is a problem that if you start with an $(n+1)$-exact $(n+1)$-category, then you get two different notions of “internal $n$-category” according to whether you remember that it *was* $(n+1)$-exact, or whether you forget that and take its free $(n+1)$-exact completion. But fortunately, there should also be a more general framework which keeps track of this sort of thing. The right context in which to talk about an “internal $n$-category” is a unary $(n+1)$-site, and in that case the meaning of “internal $n$-category” is “object of the $(n+1)$-exact completion”. An $(n+1)$-exact $(n+1)$-category should be its *own* exact completion regarded as a unary $(n+1)$-site with its $(n+1)$-exact topology, while the free $(n+1)$-exact completion of any category corresponds to starting with a trivial topology.

Also the right notion of internal Lie algebroid of an internal groupoid requires the atlas. The “Lie-Rinehart pair”-description of Lie algebroids makes that manifest: we have a base space and a Lie algebra paraeterized over it. This is the differential version of having an atlas $U \to X$ and the group $Equiv(U)_X$.

]]>There are more reasons to stick to the convention that a *groupoid in* an $\infty$-topos is not just an object $X$, but an object $X$ with an effective epimorporphism $U \to X$ (an atlas):

several standard notions in structured groupoid theory, such as etale groupoid mandatorily assume that the atlas $U \to X$ is part of the data. Etaleness is with respect to that atlas, otherwise there is no such notion.

Similarly, in an cohesive $\infty$-topos with infinitesimal cohesion we can say what it means for a morphism to be a formally etale morphism. It turns out (Stephan Spahn will have something out on this soon) that in the smooth context an *etale $\infty$-groupoid* is an effective epi $U \to X$ such that this morphism is formally etale.

(cancel)

]]>The thing was that there is no such ambiguity in “internal $\infty$-category” – and when that is restricted to the invertible case one gets conguences/internal groupoids and not just objects.

]]>But there is a better general concept of internal set (particularly in a category viewed as a universe), which can more unambiguously be called ‘internal setoid’.

I’m not sure I entirely understand what’s being said here, but I strongly disagree with the idea that an object equipped with an internal equivalence relation is a *better* notion of “set” internal to a category. It all depends on how you intend to regard the objects of that category. If your category is a 1-topos, for instance, then *usually* you want to regard its objects *as sets* in which case they are the good notion of internal set. But if the objects of your category are, say, assemblies, or types in a type theory that lacks quotient types, then you may want to regard its objects instead as presets.

The same thing is at play in higher dimensions. I would argue that when working internally to an $(\infty,1)$-topos we *usually* want to regard its objects *as $\infty$-groupoids* internal to its world.

I agree that the fact that we currently say “internal $\infty$-groupoid in an $(\infty,1)$-category” to mean something other than simply “object” would suggest, if we were inventing mathematics out of whole cloth, that “internal set” ought to mean an object equipped with an equivalence relation. However, I think that actually using terminology in that latter way would be *extremely confusing*, and I would prefer to change it in the other way: say something like “$(\infty,1)$-congruence” rather than “internal $\infty$-groupoid”.

Yes, in these rows, it’s often unclear what should be in which column. I just figured that completely presented set was better than set, and you had set in the same column on the next row, while you had preset in a different column in the same row. Since ‘completely presented set’ isn’t simply a synonym for ‘preset’ (although they do correspond in a way), it’s good to have them listed separately (but in the same row); however, which column holds which words is not really clear that far down in the table!

]]>at types and logic - table where it seemed to be needed.

Ah, thanks. I was wondering what to put there. I decided that maybe in the left column the distinction hadn’t been made.

So how do you decide where to put this? Is the table right that “completely presented set” is a notion in “logic” while “preset” is one in type theory? Maybe we should move “preset” also to the “logic”-column?

It’s more a question about history than about facts. There were a few other entries in the table where I was hesitating about whether they sit in the right column. (On the other hand that’s of course part of the point of this table, to show that the distinction between the columns is artificial.)

]]>Yes, I agree with the remark at h-set.

BTW, I threw in a link to completely presented set (which however currently just redirects to preset) at types and logic - table where it seemed to be needed.

]]>Hi Toby,

yes, thanks. I understand where you both were coming from, I am aware of the different traditions. It was just that I came from all this discussion of Bishop sets, the predicative topos that they form, the tight relation to the question of $\infty$-category theory internal to homotopy type theory, etc; maybe about half a dozen related threads here. So I thought it was clear which context I am speaking in. But I understand that I should have made it clearer. I should have base changed you to the context in which I was making judgements, first. ;-)

So this preset/set things is a subtle issue. I find it striking how close it in nature to the subtleties that we were discussing a few months back in the thread on internal $\infty$-categories. There, too, one runs into these subtle shades of notions, where one needs to distinguish “internal pre-$\infty$-categories” from the “complete” ones, etc.

I think it’s closely related, that’s why I made that remark in h-set, please check if you haven’t yet, to see if we can agree on this.

I think this may be relevant: in Benno’s article somewhere he mentions that Bas once asked whether h-sets in HoTT also form a predicative topos. I am not sure about that question, but I think it points to the following important point:

we know now that the types in HoTT form an $\infty$-topos (at least a locally cartesian closed category with universe and as many inductive objects as to care to add). But the next central question will be: what do the internal $\infty$-categories form? I guess they will form a **predicative $\infty$-topos**.

The problem here is that the language of the word ‘internal’ has always been geared towards the category of sets (where sets are, of course, objects) when presets are the more basic concept. So any treatment of categories and higher categories that wants to get at such basic concepts will run into trouble with that language.

]]>The usual term used in place of ‘internal set’ is ‘object’ (in a 1-category).

In fact, no. That’s the whole point: an object in 1 -category is just an internal preset or h-set.

That’s a good point.

Actually, what I said is true: the *usual* concept of internal set in a $1$-category is simply an object. (Compare other internal notions, such as internal monoid.) But there is a *better* general concept of internal set (particularly in a category viewed as a universe), which can more unambiguously be called ‘internal setoid’.

And this is what you wanted in your list, so (despite writing a true sentence) I was wrong.

So in constructive foundations in type theory a type is called a preset, a type with an equivalence relation on it is a set.

Be careful; *sometimes* this terminology is used, but other times the words ‘set’ and ‘setoid’ are used in place of ‘preset’ and ‘set’. (There are other combinations, such as ‘type’ and ‘setoid’.) For example, in Coq, `Set`

is really a type of presets.

I see. Sorry, then.

]]>I am not sure if we are all discussing the same thing.

So in constructive foundations in type theory a type is called a preset, a type with an equivalence relation on it is a set. People say this, you can see it in the references at *Bishop set*.

So this is what I am talking about. Now Toby passed to the categorical semantics and claimed that set goes to object. But what goes to objects is the types, hence the presets.

And as I tried to point out in that remark now at h-set, in fact only the latter terminology is consistent with the more general terminology of internal higher groupoids.

]]>