The n-Category Café

I don’t think there’s a definitive place he treats extensive quantities, but you can catch a discussion here. If you haven’t read Lawvere before, you may be in for a shock.

Anders Koch has been working on extensive quantities in Lawvere’s sense.

Regarding mereology, one would first look to subobjects, and then toposes. No need to expect the Boolean property in general.

Jeff,

Thank you for your interesting comments. Speaking as someone who was competely unaware of measurement theory until your posts, it looks to me that measurement theory could use some category theory.

For example, we learn on p. 3 of Measurement, theory of that

“A key concept in the theory of measurement is that of a representation, which is defined to be a structure preserving map…”

Sounds like “representation” is a functor, doesn’t it.

VV theory about fiber sequences is here:
https://github.com/vladimirias/Foundations/blob/master/Generalities/uu0.v

The double fibration is there too.

VV theory about fiber sequences is here:

https://github.com/vladimirias/Foundations/blob/master/Generalities/uu0.v

Thanks! I have added a link to it at nLab:fiber sequence.

(By the way, for both browser on my machine, when I point to this file, they crash…)

As for the question you pose, since this data gives us an adjunction between the discrete objects and the codiscrete ones (the left adjoint being the restriction of conc and the right adjoint the restriction of flat),

I thought that’s what is missing in the code currently, an axiom that makes conc and flat be related in any way. We want them to form an adjunction, yes, but it seems to me that this information still needs to be added to the Coq code in some way.

an axiom that makes conc and flat be related in any way. We want them to form an adjunction, yes, but it seems to me that this information still needs to be added to the Coq code in some way.

We have a coreflective subcategory $Disc$, with flat the coreflector, and a reflective subcategory $Codisc$, with conc the reflector. (What does conc stand for, by the way? My initial impulse was to call that functor coarse.) So we have a composite adjunction

$$Disc \;\underset{flat}{\rightleftarrows}\; \mathbf{H} \;\overset{conc}{\rightleftarrows}\; Codisc$$

no?

no?

Now I understand what you mean, sorry for being slow.

And maybe I am still slow: certainly we want it be implied that this composite adjunction is an equivalence. But why is that sufficient for the condition that I denoted $\Gamma \simeq \tilde \Gamma$?

What does conc stand for, by the way?

It was supposed to mean “concrete”. Because the image factorization of the corresponding unit is concretification. But I keep looking for a better term. Maybe coarse is indeed better. I wish I had a term that would harmonize more with “$\Pi$” and “$\flat$”, though.

But why is that sufficient for the condition that I denoted $\Gamma\simeq \tilde{\Gamma}$?

Well, I think there’s an inaccuracy in the diagram you drew back here: nothing we have so far guarantees that the category $\mathbf{B}$ occurring in the functors $\Pi$, $Disc$, and $\Gamma$ is the same as the category $\mathbf{B}$ occurring in the functors $coDisc$ and $\tilde{\Gamma}$. Asking that the composite adjunction be an equivalence gives us a canonical way to identify these two categories, and under that identification, I believe it should be the case that $\Gamma \simeq \tilde{\Gamma}$.

I wish I had a term that would harmonize more with “$\Pi$” and “$\flat$”, though.

Well, the obvious dual of $\flat$ is $\sharp$…

Oops! My bad. You’re right, there is another condition necessary.

For any type $X$, we have a canonical composite map $$\flat X \to X \to \sharp X.$$ Under the adjunction $$(\text{discrete objects}) \underoverset{\flat}{\sharp}{\rightleftarrows} (\text{codiscrete objects})$$ this corresponds to maps $\flat X \to \flat \sharp X$ and $\sharp\flat X\to \sharp X$. The necessary condition is that these two maps always be equivalences.

(The condition that the above adjunction is an equivalence is equivalent to saying that these two maps are equivalences when $X$ is discrete or codiscrete—or that for any $X$, one is an equivalence iff the other one is.)

Well, the obvious dual of $\flat$ is $\sharp$…

Good point. I like that.

The necessary condition is that these two maps always be equivalences.

I see now. That looks good.

It’s too late for me tonight. But hopefully tomorrow I find a free minute to use this to complete the HoTT formulation of the axioms in the $n$Lab entry. Thanks!

Hi Mike,

thanks for these replies. I’ll get back to them a little later when I have more time. For the moment just a quick question/comment on this one here:

I proved this because it was part of what I needed to identify $\Omega S^1 = \mathbb{Z}$

I was looking for your Coq file with the proof of this the other day, since I thought I might learn a bit of HoTT coding from staring at it. But I didn’t find the file. Could you post the url again, for convenience?

I did go to

https://github.com/HoTT/HoTT

and looked for the file, but this page did leave me a bit puzzled.

Did “you” (those of you who maintain the site) think about adding some summary and explanation on this page? Coming from the outside I am missing here some text that tells me something like: “Go here for this code and there for that code. If you are new here you need to first read this, then that.” Of course I understand that this is probably not meant to be read by any outsiders. But maybe eventually if would be useful if it were.

Need to rush off now. More substantial messages later…

I was looking for your Coq file with the proof of this the other day

It’s in the “Coq” subdirectory, in the further “HIT” subdirectory for Higher Inductive Types: https://github.com/HoTT/HoTT/blob/master/Coq/HIT/Pi1S1.v.

some summary and explanation on this page?

More summary and explanation somewhere would be nice; I’m not sure whether that page is the right place for it.

in the further “HIT” subdirectory

Ah, thanks. I had clicked around here and there, but never on that one.

More summary and explanation somewhere would be nice; I’m not sure whether that page is the right place for it.

The README-file on that Coq-directory page would be the canonical place.

Curses!!! You’re right! Back to the old drawing board.

Hmm… this makes it much harder.

Back to the old drawing board.

Okay. It’s the same problem that bit me in the other thread here when I was trying to see if Guillaume’s proposed HoTT code for effective epimorphisms did capture the HTT that it was supposed to capture: do we use external or internal homs to characterize universal properties. So we need to get back to this drawing board anyway.

I won’t have much time for this today, but here is a quick thought that might be helpful:

at least for cohesive $\infty$-toposes that have an ∞-cohesive site of definition, we have for every representable $U$ that $\mathbf{\Pi}(U) \simeq \ast$ and $\mathbf{\Pi}(X \times U) \simeq \mathbf{\Pi}(X) \times \mathbf{\Pi}(U) \simeq \mathbf{\Pi}(X)$.

This implies that whenever $A$ is discrete, the internal homs into $A$ already coincide with the re-internalized external homs: for all $X$ we have

$$\flat [X, A] \simeq [X, A] \,.$$

(For the record and for other readers: this is because the internal hom of $\infty$-stacks is the $\infty$-stack which sends $[X,A] : U \mapsto \mathbf{H}(X \times U , A)$ and by the above $\mathbf{H}(X \times U, \flat A) \simeq \mathbf{H}(\mathbf{\Pi}(X \times U), A) \simeq \mathbf{H}(X, A)$.)

This means for instance that over an $\infty$-cohesive site our current HoTT coding of the reflection $(\Pi \dashv Disc)$ happens to be correct after all.

Moreover, for the coreflection $(Disc \dashv \Gamma)$ it means that it would be sufficient to say in HoTT that the map

$$[X, \flat A] \to [X,A]$$

from a discrete $X$, while not an equivalence, factors through $\flat [X, A] \to [X,A]$ by an equivalence.

I’m now worried about a different issue, which I should have been worried about as soon as Steve Awodey pointed us back to his paper with Lars Birkedal: pullback-stability. When we say

flat : Type -> Type

we actually mean that $\flat$ is an endomorphism of the object classifier. That means that not only do we have an operation acting on the core of $\mathbf{H}$, we have operations acting on the cores of all its slice categories $\mathbf{H}/X$ which commute with pullback.

This is not a problem for $\sharp$, I think, since the codiscrete objects are a subtopos and sheafification does commute with pullback. But I am worried about $\flat$. Perhaps we should axiomatize $\sharp$ first and then say

flat : sharp Type -> sharp Type

? That seems like it would get painful quickly….

I was thinking how we might define simplicial objects inductively, and came up with the following, perhaps misguided, attempt. I make to guarantees about the following working :)

The goal is to inductively define simplicial objects and the decalage functor simultaneously.

Start with an internal reflective graph i.e. a 1-truncated simplicial object $sk_1 X$ (at present this is just notation saying that this thing is 1-truncated, not that it is the truncation of anything - but you see where I’m headed). If we are given another 1-truncated simplicial object over $sk_1 X$, $p:sk_1 D X \to sk_1 X$, such that the collection of 0-simplices of $sk_1 D X$ is isomorphic to the collection of 1-simplices of $sk_1 X$ (hmm, yes, issue there with saying things are isomorphic perhaps), $p$ is split, and other identities that are satisfied by the 1-truncation of the map $Dec^1 Y \to Y$ for a simplicial set $Y$.

We then define a 2-truncated simplicial object to be the data we can extract from this setup: the collection of 2-simplices is the collection of 1-simplicies of $sk_1 D X$, and we get all the relevant face/degeneracy maps from the structure we have at hand. This is the induction step.

I suppose we also need to define, as part of this inductive definition what a map of $n$-truncated simplicial objects is.

I don’t know enough about Coq to say this is formalisable therein, or even if this really is any different to how one might naively try to define simplicial objects in Coq. In any case, it all seems to need extensional equality - do we really want this when talking about simplicial objects in an $(\infty,1)$-category?

Indeed, I was thinking of the property to be cohesive over another ∞-topos.

But I still do not really understand what you are trying to do. When you say that you can do physics in a cohesive ∞-topos, don’t you need it to be cohesive over ∞Gpd? Can you do something interesting with an ∞-topos cohesive over itself via the identity?

Moreover, if find the Axiom is_discrete : Type -> Type. part a bit misleading.
For me an axiom is something that you should not be able to prove, and in this case you can take the proposition always true for is_discrete and take the identity for pi and flat.

Perhaps something like Parameter is_discrete : Type -> Type. would be better? (it means exactly the same thing for Coq, but tells the human reader that this is not an axiom but a parameter, and I think this is what you want in this case)

When you say that you can do physics in a cohesive ∞-topos, don’t you need it to be cohesive over ∞Gpd?

No, it may be over a different base $\infty$-topos. For instance supergeometric cohesion and hence supersymmetric physics is not over discrete $\infty$-groupoids, but over discrete super ∞-groupoids.

Indeed, the point of these internal constructions is that they make sense in any cohesive $\infty$-topos.

But in some models of the axioms the constructions may be more interesting than in others. For instance…

Can you do something interesting with an ∞-topos cohesive over itself via the identity?

Indeed, the physics in a topos of discrete cohesion is mostly trivial. Still, as I mentioned in my previous comment, it is useful not to exclude discrete cohesion from the picture.

Compare to this: the empty set in itself is not interesting. But it is nevertheless very useful to include the empty set in the collection of all sets. This is a common pattern in mathematics. It is useful to include the degenerate cases in the general theory.

Perhaps something like Parameter is_discrete : Type -> Type. would be better? (it means exactly the same thing for Coq, but tells the human reader that this is not an axiom but a parameter, and I think this is what you want in this case)

Could you point me to some documentation that explains how Parameter and Axiom two should be used in Coq?

When you say that you can do physics in a cohesive ∞-topos, don’t you need it to be cohesive over ∞Gpd?

Well, part of the point of topos theory is that any topos can perfectly well “pretend” to be the topos of sets, so that we can then do all sorts of mathematics “over” that topos. (From a foundational point of view, “the” topos of sets isn’t particularly special anyway.) Similarly, any $(\infty,1)$-topos can pretend to be $\infty Gpd$. So if we have an $(\infty,1)$-topos which is cohesive over another one, we can always pretend the latter one is $\infty Gpd$.

Perhaps something like Parameter is_discrete : Type -> Type. would be better?

Sure. I actually find it kind of confusing that Coq has two words Axiom and Parameter (and also Conjecture!) that mean exactly the same thing—especially because they don’t mean (quite) the same thing as Hypothesis and Variable, and I can never remember without looking it up which word is the same as which word and different from which other word and what the difference is. But if Parameter makes you happier than Axiom, that’s fine with me.

In reaction to Guillaume Brunerie’s various comments, I have done the following to the $n$Lab:

• added an entry base (∞,1)-topos ;

• at cohesive (∞,1)-topos in the section Definition - Externally I have added a remark saying the following:

“As always in topos theory and higher topos theory, such definitions can be made sense of over any base . Here: over any base (∞,1)-topos.

Over the canonical base ∞Grpd of ∞-groupoids, the definition of a cohesive (∞,1)-topos is equivalently the following: […]

Often we will tacitly assume to work over ∞Grpd. But most statements and constructions have straightforward generalizations to arbitrary bases.

In particular, below in the internal definition of cohesion, it takes more effort to fix the base topos than to leave it arbitrary.”

Hey Guillaume,

right, the $n$Lab entries mostly work over $\infty Grpd$, currently. Somebody should generalize them.

You may notice that the discussion of generalization to arbitrary base $\infty$-toposes is more pressing when we formulate the theory – as we just start doing now – in HoTT, where we cannot easily say: let the sub-$\infty$-topos of discrete objects be $\infty Grpd$.

Just to be sure, when you say “discrete something ∞-groupoid”, this is exactly the same thing as a “something ∞-groupoid” and the word “discrete” is just there to emphasize that what you are really interested in is an ∞-topos cohesive over the ∞-topos of “something ∞-groupoids”, right?

The word “discrete cohesion” refers to cohesion induced by the identity functors.

Over the canonical base $\infty$-topos, “discrete $\infty$-groupoid” just means “$\infty$-groupod”. Also topological spaces are “discrete $\infty$-groupoids”, in the sense of homotopy theory, because the functors that exhibit $Top$ as being cohesive over $\infty Grpd$ are equivalences.

If we choose a different base $\infty$-topos $\mathbf{B}$ then the objects of $\mathbf{B}$ are equipped with “discrete cohesion relative to $\mathbf{B}$”. Any $\infty$-topos equivalent to $\mathbf{B}$ exhibits discrete cohesion relative to $\mathbf{B}$.