Michael,

please, it’s good to discuss this, and given that apparently the $n$Lab entries didn’t convey this, we should strive to edit them.

I am a bit too busy with something else to edit right now. But to the extent that you feel you gained information here that wasn’t on the $n$Lab pages then you are invited, I’d even say *urged* and would like to say: *compelled*, to add it in. Please do, to the extent that you feel certain.

To the extent that you don’t feel certain yet, just open another thread here dedicated to the issue!

]]>Agreed that there is no objective way in which terminology is correct or incorrect. I was not sure I understood the idea behind the terminology, but I think it’s clear now.

Your last sentence, on the other hand, gives me new food for thought :) But I don’t want to hijack this thread any longer.

]]>Michael, maybe you are taking a casual choice of terminology more serious than it ought to. It being terminology, there is no way it could be “correct” or “incorrect”.

I would say that $B \to Type$ is the name of all of $X$ and its restrictions along any $\ast \to B \to Type$ are the names of the fibers. But if you don’t like that choice of wording, that’s fine, too.

Over at propositional extensionality this issue is dealt with by quotation marks. For $P$ a proposition, then $'P'$ is its name (this $P$ is $X$ from before, just a different symbol, same idea). I think it makes very good sense.

If you feel idealistic, you might call $'P'$ the inner reflection of the outer $P$. :-)

]]>Thanks again. Concerning the diagram in #15, with an arbitrary $B$ which is not necessarily the terminal object, wouldn’t it be more “correct” to say: “the images of $B\to Type$ are the names of the fibers of $X\to B$”.

This could be nitpicking or just a lack of understanding from my part :)

]]>I’m not sure I do know good references. You can find internal universes in pretoposes used in Algebraic Set Theory for instance (see the monograph by Joyal and Moerdijk).

]]>I didn’t make up this terminology, it is used in circles of category theorists, but the circle that uses it may not be huge. You see it for instance in the first line here. I agree that it would be good to have this better documented on the $n$Lab. If anyone has time and energy, please do.

Todd Trimble is likely to know references. If he doesn’t see this here, maybe email him.

]]>Thanks for the explanation. Is the terminology standard? I couldn’t find it on the other page you linked to.

Is there a similar terminology for the upper horizontal arrow in your last diagram and the object $\widehat {Type}$?

]]>The univalent type universe $Type$ aka object classifier in an infinity-topos has the property that every map $X \to B$ with sufficiently small homotopy fiber sits in a homotopy pullback of the form

$\array{ X &\longrightarrow& \widehat {Type} \\ \downarrow && \downarrow \\ B &\longrightarrow& Type }$Here the bottom horizontal map, which “classifies” or “modulates” $X$ is “the name of $X$”.

]]>Yes!

]]>Re #1: I’m trying to understand what

the name of V in the type universe U

means.

Is it the arrow $f:1\to U$ corresponding to $V\to1$ as described in universe in a topos? A quick search didn’t lead to any other reference explaining the terminology.

]]>Here I’d like to rephrase the method in #3 in terms of homotopy fibers again, using

$\begin{aligned} \mathbf{Aut}_{B_1}(X_1) &\coloneqq \underset{B_1}{\prod} \mathbf{Aut}(\phi) \\ &\simeq fib(\mathbf{Aut}(X_1)\stackrel{\phi\circ(-)}{\longrightarrow} [X_1,B_1]) \end{aligned}$because that makes it easier to adopt this to the case where this group needs to be differentially concretified before acting, which happens to be the case that I really need.

Then the following should be a solution: we observe the pasting composite

$\array{ \mathbf{Aut}_{B_1}(X_1) \times X_1 &\longrightarrow& \mathbf{Aut}(X_1) \times X_1 &\stackrel{ev}{\longrightarrow}& X_1 \\ \downarrow^{\mathrlap{p_2}} && \downarrow^{\mathrlap{(\phi\circ(-),id)}} && \downarrow^{\phi} \\ X_1 &\stackrel{(\vdash\phi,id)}{\longrightarrow}& [X_1,B_1] \times X_1 &\stackrel{ev}{\longrightarrow}& B_1 \\ \downarrow^{\mathrlap{\phi}} && && \downarrow^{\mathrlap{id}} \\ B_1 &=& B_1 &=& B_1 }$where the top left square is the image under $(-)\times X_1$ of the pullback square that exhibits the homotopy fiber just mentioned, and where the right square is the Hom-adjunct of a trivially commuting square expressing postcomposition with $\phi$.

Now we base change the outer diagram along $B_2\to B_1$ to get an action morphism

$\mathbf{Aut}_{B_1}(X_1) \times X_2 \longrightarrow X_2$together with a square that exhibits this action as being over $B_2$.

]]>Great! Is the internal description I gave in #3 sufficient for you to extrarct a diagrammatic answer?

]]>Okay, good, using this I have a formalization of the concept of BPS charges for branes without tensor multiplets (now section 5.3.13 here). Now to generalize further and have BPS charges for branes with tensor multiplets I need a similar diagrammatic answer for the second question in #2.

But first some lunch now.

]]>Ah, or rather I should take also the right square to be (the horizontal reverse of) that left square, and that then gives the conjugation action that you indicated.

$\left( \array{ \mathbf{Aut}_{Grp}(V) \times V \\ \downarrow \\ V } \right) \;\;= \;\; lim \left( \array{ \mathbf{Aut}_{Grp}(V) &\longrightarrow& \mathbf{Aut}_{Grp}(V) \times \mathbf{B}V &\longleftarrow& \mathbf{Aut}_{Grp}(V) \\ \downarrow && \downarrow && \downarrow \\ \ast &\longrightarrow& \mathbf{B}V &\longleftarrow& \ast } \right)$ ]]>Thanks. Here is what I have now come up with:

Consider the squares

$\array{ \mathbf{Aut}_{Grp}(V) &\longrightarrow& \mathbf{Aut}_{Grp}(V) \times \mathbf{B}V &\longleftarrow& \ast \\ \downarrow && \downarrow && \downarrow \\ \ast &\longrightarrow& \mathbf{B}V &\longleftarrow& \ast }$where the left one is obtained from factoring the defining pullback square of $\mathbf{Aut}_{Grp}(V) \simeq \mathbf{Aut}(\mathbf{B}V) \underset{\mathbf{B}V}{\times} \ast$ as

$\array{ \mathbf{Aut}_{Grp}(V) &\longrightarrow& \mathbf{Aut}(\mathbf{B}V) \\ \downarrow && \downarrow \\ \mathbf{Aut}_{Grp}(V) \times \mathbf{B}V &\longrightarrow& \mathbf{Aut}(\mathbf{B}V) \times \mathbf{B}V \\ \downarrow && \downarrow^{\mathrlap{ev}} \\ \ast &\longrightarrow& \mathbf{B}V }$Then forming homotopy limits over the horizontal cospans in the first two squares yields a map

$\mathbf{Aut}_{Grp}(V) \times V \longrightarrow V$The adjunct of that might factor through the map $\mathbf{Aut}_{Grp}(V) \to \mathbf{Aut}(V)$ that I am after.

Hm, this needs more checking. But I need to quit now.

]]>Yes, I know that sometimes we really do need to extract a diagrammatic statement from the internal reasoning. (That’s why I put a smiley on my comment.) I don’t have time to do the extraction right now, but if you’re willing to do it, here’s a formula: given $(e,t) : \sum_{e:B V \simeq B V} (e(pt) = pt)$, we define $\Omega e : \Omega B V \to \Omega B V$ by $\Omega e (p) = t^{-1} \cdot ap_e(p) \cdot t$. Here $p : pt =_{B V} pt$, so $ap_e(p) : e(pt) = e(pt)$, and conjugating it by $t$ brings it back to $pt = pt$ again, i.e. $\Omega B V$.

]]>Oh, it’s just so much easier to think internally… (-:

I certainly see that, it is indeed much easier, indeed it’s close to being effortless, in that to a large extent one just makes the naive statements. It’s beautiful.

But either I am missing something, or I really do need the translation of this effortless language to diagrams, because as a second step after having the internal formulation of something, I need to extract some actual maps of stacks out of it.

Concretely, right now I am chewing on the following: I have an abstract internal construction of a class of higher groups which externalizes to the super-groups Lie integrating the M-theory super Lie algebra with its degree-2 extension (we have an article on that essentially done, details should be available in a short while).

But the full M-theory super Lie algebra involves also a degree-5 extension piece. I think I know which internal construction gives that, too. But to check, I need to translate that to an actual universal construction of super stacks, and work out if it comes out as it should.

Maybe I am being dense, but it seems to me for that I really need some universal pullback diagram of sorts that constructs for me that map of group stacks $\mathbf{Aut}_{Grp}(V) \to \mathbf{Aut}(V)$.

Now I know how to translate any actual formula that you write in homotopy type theory into such universal constructions. But I don’t know what to do concretely in this respect when you say infromal things like

]]>you just observe that any map between pointed types that preserves basepoints induces a map between loop spaces.

Oh, it’s just so much easier to think internally… (-:

]]>Thanks, Mike, but wait:

A simpler way to get $Aut_{Grp}(V)$ is as $\sum_{e:B V \simeq B V} (e(pt) = pt)$.

That translates semantically to the homotopy fiber of $\mathbf{Aut}(\mathbf{B}V) \stackrel{(-) \circ pt}{\longrightarrow} [\ast, \mathbf{B}V]$, which is what I recognize as the stabilizer group of $pt$ under the canonical $\mathbf{Aut}(\mathbf{B}V)$-action on $[\ast,\mathbf{B}V]$. So this I am happy with, but I have trouble formalizing this sentence:

To get the map to $Aut(V)$ you just observe that any map between pointed types that preserves basepoints induces a map between loop spaces.

Of course I know that this is so, externally, but which universal construction gets me the map out of the above homotopy fiber?

]]>A simpler way to get $Aut_{Grp}(V)$ is as $\sum_{e:B V \simeq B V} (e(pt) = pt)$. To get the map to $Aut(V)$ you just observe that any map between pointed types that preserves basepoints induces a map between loop spaces.

In the second question, if you represent $X_1$ as a type family $X_1 : B_1 \to Type$, then its automorphisms over $B_1$ are $\prod_{b:B_1} Aut(X_1(b))$. Then $X_2$ is just the composite $B_2 \xrightarrow{g} B_1 \to Type$ and an $f:\prod_{b:B_1} Aut(X_1(b))$ sends $x:X_2(a)$ (i.e. $x:X_1(g(a))$) to $f(g(a),x)$.

]]>Hm, I know how to elementarily get $\mathbf{Aut}_{Grp}(V) \to \mathbf{Aut}(\mathbf{B}V)$, as this is the stabilizer group (by the discussion there) of $(\ast \to \mathbf{B}V) \in [\ast,\mathbf{B}V]$ under the right $\mathbf{Aut}(\mathbf{B}V)$-action. But I am not sure how to get the map to $\mathbf{Aut}(V)$.

I see that I have another problem of similar nature. Given a homotopy pullback

$\array{ X_2 &\longrightarrow& B_2 \\ \downarrow && \downarrow \\ X_1 &\stackrel{\phi}{\longrightarrow}& B_1 }$then the automorphisms of $X_1$ over $B_1$ should canonically act on $X_2$. The elementary construction o the former is again as the stabilizer of $\phi\in [X_1,B_1]$ under $\mathbf{Aut}(X_1)$. But how to construct the action of that on $X_2$ by elementary means?

]]>Given any object $V$ in an elementary $\infty$-topos, then its automorphism group $\mathbf{Aut}(V)$ may be characterized as the pointed connected object which is the 1-image of the name of $V$ in the type universe.

Now if $V$ itself has group structure, hence if there is pointed connected $\ast \to \mathbf{B}V$, what is the elementary way to speak of its group $\mathbf{Aut}_{Grp}(V)$ of group automorphisms, hence of automorphisms of $\mathbf{B}V$ that preserve the basepoint?

And I’d need a canonical forgetful map

$\mathbf{Aut}_{Grp}(V) \longrightarrow \mathbf{Aut}(V) \,.$ ]]>