Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeApr 28th 2015
   • (edited Apr 28th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexGiven 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) \,. $$

   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) \,.$$
2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeApr 28th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, 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?

   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?

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeApr 28th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexA 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)$.

   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)$.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeApr 28th 2015
   • (edited Apr 28th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, 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?

   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?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeApr 28th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOh, it's just so much easier to think internally... (-:

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

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeApr 28th 2015
   • (edited Apr 28th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> 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… (-:

   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.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeApr 28th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, 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$.

   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$.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeApr 28th 2015
   • (edited Apr 28th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks. 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeApr 29th 2015
   • (edited Apr 29th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAh, 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) $$

   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)$$
10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, good, using this I have a formalization of the concept of BPS charges for branes without tensor multiplets (now section 5.3.13 [here](https://dl.dropboxusercontent.com/u/12630719/dcct.pdf)). 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeApr 29th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGreat! Is the internal description I gave in #3 sufficient for you to extrarct a diagrammatic answer?

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

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • (edited Apr 29th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere 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$.

    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$.

13. • CommentRowNumber13.
    • CommentAuthorMichael_Bachtold
    • CommentTimeApr 29th 2015
    • PermaLink
    Author: Michael_Bachtold
    Format: MarkdownItexRe #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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes!

    Yes!

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeApr 29th 2015
    • (edited Apr 29th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe univalent type universe $Type$ aka [object classifier in an infinity-topos](http://ncatlab.org/nlab/show/%28sub%29object+classifier+in+an+%28infinity,1%29-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$".

    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$”.

16. • CommentRowNumber16.
    • CommentAuthorMichael_Bachtold
    • CommentTimeApr 30th 2015
    • PermaLink
    Author: Michael_Bachtold
    Format: MarkdownItexThanks 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}$?

    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}$?

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015
    • (edited Apr 30th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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](http://ncatlab.org/nlab/show/subobject+classifier#examples). 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.

    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.

18. • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 30th 2015
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI'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’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).

19. • CommentRowNumber19.
    • CommentAuthorMichael_Bachtold
    • CommentTimeApr 30th 2015
    • PermaLink
    Author: Michael_Bachtold
    Format: MarkdownItexThanks 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 :)

    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 :)

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexMichael, 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$. :-)

    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$. :-)

21. • CommentRowNumber21.
    • CommentAuthorMichael_Bachtold
    • CommentTimeApr 30th 2015
    • PermaLink
    Author: Michael_Bachtold
    Format: MarkdownItexAgreed 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.

    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.

22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015
    • (edited Apr 30th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexMichael, 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!

    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!