Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 13th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIn the talk I mentioned I'm giving in a couple of weeks, I'm going to touch on the homotopy quotient idea of a configuration space. Inevitably talk will turn to the metaphysics of it all. So what to say? We insist on the configuration space for general relativity on a spacetime $\Sigma$ being $$ [\Sigma, Fields]//Diff(\Sigma), $$ but they'll want to know what this means for relationalism/substantivalism, etc. Basically this means should we think of spacetime independently existing as that manifold $\Sigma$, to which we add fields, or does gauge equivalence mean that all gauge equivalent configurations should be taken to represent the 'same' physical system. The latter doesn't seem to allow us to think of that 'same' system as $\Sigma$ plus some structure. Some, recognising the symmetries lost by taking equivalence classes, but wanting uniqueness of something to stand for a component, are aiming for the skeleton of the configuration groupoid. Presumably that shouldn't help from a HoTT point of view. Keeping with the action groupoid, why not say a point within it really is just a manifold with structure? I'm sure there are more subtle positions where we don't take the configuration space so literally as representing sets of worlds, classes of sets of worlds or whatever, but rather think of models as more like maps picking up structural features. Do people have views on how to think of applied HoTT? In the nCafe discussion, we briefly touched on it in the simple case of matching apples and oranges. Here I seem to want to say: to the extent that the individual items of fruit obey the requirements of terms of a 0Type (if identity, only contractible identity), then I can count, match, etc., as normal arithmetic suggests. In the case of GTR, it seems harder to say something similar: to the extent that possible universes on a manifold, form this kind of smooth1Type, ...

   In the talk I mentioned I’m giving in a couple of weeks, I’m going to touch on the homotopy quotient idea of a configuration space. Inevitably talk will turn to the metaphysics of it all. So what to say?

   We insist on the configuration space for general relativity on a spacetime $\Sigma$ being

   $$[\Sigma, Fields]//Diff(\Sigma),$$

   but they’ll want to know what this means for relationalism/substantivalism, etc. Basically this means should we think of spacetime independently existing as that manifold $\Sigma$, to which we add fields, or does gauge equivalence mean that all gauge equivalent configurations should be taken to represent the ’same’ physical system. The latter doesn’t seem to allow us to think of that ’same’ system as $\Sigma$ plus some structure.

   Some, recognising the symmetries lost by taking equivalence classes, but wanting uniqueness of something to stand for a component, are aiming for the skeleton of the configuration groupoid. Presumably that shouldn’t help from a HoTT point of view. Keeping with the action groupoid, why not say a point within it really is just a manifold with structure?

   I’m sure there are more subtle positions where we don’t take the configuration space so literally as representing sets of worlds, classes of sets of worlds or whatever, but rather think of models as more like maps picking up structural features.

   Do people have views on how to think of applied HoTT? In the nCafe discussion, we briefly touched on it in the simple case of matching apples and oranges. Here I seem to want to say: to the extent that the individual items of fruit obey the requirements of terms of a 0Type (if identity, only contractible identity), then I can count, match, etc., as normal arithmetic suggests.

   In the case of GTR, it seems harder to say something similar: to the extent that possible universes on a manifold, form this kind of smooth1Type, …

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, that's good. I wish I had more leisure for this right now. But as things stand, I can only devote a few seconds to this every now and then. Please bear with me. Before I say anything, let me mention that Jack Morava discussed just this example in his talk at the Barcelona [CONFERENCE ON TYPE THEORY, HOMOTOPY THEORY AND UNIVALENT FOUNDATIONS](http://www.crm.cat/en/Activities/Pages/ActivityFoldersAndPages/Curs%202013-2014/CHomotopy/chomotopy.aspx) a few weeks back. See his second set of slides linked to there ([pdf](http://www.crm.cat/en/Activities/Documents/morava-crm-2013.pdf)), p. 14.

   Thanks, that’s good. I wish I had more leisure for this right now. But as things stand, I can only devote a few seconds to this every now and then. Please bear with me.

   Before I say anything, let me mention that Jack Morava discussed just this example in his talk at the Barcelona CONFERENCE ON TYPE THEORY, HOMOTOPY THEORY AND UNIVALENT FOUNDATIONS a few weeks back.

   See his second set of slides linked to there (pdf), p. 14.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexNext, I think this here is a good way to think about the key point at [general covariance -- Formalization in homotopy type theory](http://ncatlab.org/nlab/show/general%20covariance#InHomotopyTypeTheory): I should add more comments to that entry to make it clearer, but the key point there really is this: in a non-generally covariant field theory given a (spacetime-)manifold $\Sigma$ and a moduli space of fields $\mathbf{Fields}$, the space of fields on $\Sigma$ is simply the mapping space $[\Sigma, \mathbf{Fields}]$. But now take the traditional [[hole argument]] "paradox" and take it serious (or whatever to call that), as follows: if any point $$ x \colon \ast \to \Sigma $$ is supposed to be equivalent to any other point $$ y \colon \ast \to \Sigma $$ as soon as there is a diffeomorphism $\phi : \Sigma \to \Sigma$ that takes $x$ to $\phi(x) = y$, then this just means that the "moduli space for points in spacetime" is not $\Sigma$ itself, but is the homotopy quotient $\Sigma / / Diff(\Sigma)$. So until now I am saying: it should be plausible from just the informal basics of general relativity that it's $\Sigma / / Diff(\Sigma)$ which is the domain for the field of gravity. And once we accept this, now happens what when I first realized it seemed like a miracle (even though by now I find it "obvious", that's how it goes...), namely that homotopy type theory now automatically knows about what it means to have generally covariant fields. Namely the fact is that in homotopy type theory we have the equivalence $$ [\Sigma//Diff(\Sigma), \; \mathbf{Fields}] \simeq [\Sigma, \; \mathbf{Fields}]//Diff(\Sigma) \,. $$ In words: if spacetime is such that two points (or generally any two subsets) which are related by a diffeomorphism are to be regarded as equivalent, then it _follows_ that the configuration space of fields on spacetime is "generally covariant" in that any two configurations which are related by a diffeo are actually equivalent. (In writing the above equivalence I am suppressing some context, to make the point transparent: on the left the internal hom is taken in the context where everything in sight is equipped with $Diff(\Sigma)$-action, on the right the mapping space is taken in the ambient context ). I'd think this is a nice little fact (a theorem/proposition/lemma/observation/remark, depending on where you come from ;-) with a nice immediate informal interpretation and good reflection on an issue that was historically of great importance.

   Next, I think this here is a good way to think about the key point at general covariance – Formalization in homotopy type theory:

   I should add more comments to that entry to make it clearer, but the key point there really is this:

   in a non-generally covariant field theory given a (spacetime-)manifold $\Sigma$ and a moduli space of fields $\mathbf{Fields}$, the space of fields on $\Sigma$ is simply the mapping space $[\Sigma, \mathbf{Fields}]$.

   But now take the traditional hole argument “paradox” and take it serious (or whatever to call that), as follows:

   if any point

   $$x \colon \ast \to \Sigma$$

   is supposed to be equivalent to any other point

   $$y \colon \ast \to \Sigma$$

   as soon as there is a diffeomorphism $\phi : \Sigma \to \Sigma$ that takes $x$ to $\phi(x) = y$, then this just means that the “moduli space for points in spacetime” is not $\Sigma$ itself, but is the homotopy quotient $\Sigma / / Diff(\Sigma)$.

   So until now I am saying: it should be plausible from just the informal basics of general relativity that it’s $\Sigma / / Diff(\Sigma)$ which is the domain for the field of gravity.

   And once we accept this, now happens what when I first realized it seemed like a miracle (even though by now I find it “obvious”, that’s how it goes…), namely that homotopy type theory now automatically knows about what it means to have generally covariant fields.

   Namely the fact is that in homotopy type theory we have the equivalence

   $$[\Sigma//Diff(\Sigma), \; \mathbf{Fields}] \simeq [\Sigma, \; \mathbf{Fields}]//Diff(\Sigma) \,.$$

   In words: if spacetime is such that two points (or generally any two subsets) which are related by a diffeomorphism are to be regarded as equivalent, then it follows that the configuration space of fields on spacetime is “generally covariant” in that any two configurations which are related by a diffeo are actually equivalent.

   (In writing the above equivalence I am suppressing some context, to make the point transparent: on the left the internal hom is taken in the context where everything in sight is equipped with $Diff(\Sigma)$-action, on the right the mapping space is taken in the ambient context ).

   I’d think this is a nice little fact (a theorem/proposition/lemma/observation/remark, depending on where you come from ;-) with a nice immediate informal interpretation and good reflection on an issue that was historically of great importance.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeNov 13th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhile I had absolutely no time for it, I did now add a paragraph along the above lines to a new subsection [general covariance -- Formalization in HoTT -- Informal introduction](http://ncatlab.org/nlab/show/general+covariance#InHomotopyTypeTheory).

   While I had absolutely no time for it, I did now add a paragraph along the above lines to a new subsection general covariance – Formalization in HoTT – Informal introduction.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 13th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexOh, I had jotted down on a page 90 minutes ago a comparison of $[A, B]//Sym(A)$ and $[A//Sym(A), B]$ for two sets $A$ and $B$, and managed to convince myself they weren't the same. Silly me! Thanks for this. I'll try to digest it.

   Oh, I had jotted down on a page 90 minutes ago a comparison of $[A, B]//Sym(A)$ and $[A//Sym(A), B]$ for two sets $A$ and $B$, and managed to convince myself they weren’t the same. Silly me!

   Thanks for this. I’ll try to digest it.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeNov 14th 2013
   • (edited Nov 14th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWarning, as I tried to highlight, it's important to note that I am talking about $[A//Sym(A), B]_{B Sym(A)}$, the internal hom formed in the category of types with $Sym(A)$-action. You probably computed the homs out of the action groupoids as such. Then it does not work. What I am using here is the following fact, discussed in some detail at _[[infinity-action]]_: an action of som $G$ on some $V$ is equivalently encoded in the bundle $$ \array{ V &\to& V//G \\ && \downarrow \\ && \mathbf{B}G = \ast //G } \,. $$ In particular the slice $\infty$-topos over $\mathbf{B}G$ is equivalent to the category of $G$ actions $$ G Act(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G} \,. $$ Or in type-theoretic words: a $G$ action on $V$ is the same as a $\mathbf{B}G$-dependent type whose context extension to the global context is $V$. Now the key fact is this here: if $(V_1, \rho_1)$ and $(V_2, \rho_2)$ are two $G$-actions, then the internal hom *in the slice* /dependent over $\mathbf{B}G$ is 1. the type of _all_ maps $[V_1, V_2]$ 1. regarded as equipped with the $G$-action given by conjugation, hence the action where $g \in G$ acts on a function $f : V_1 \to V_2$ by $f \mapsto g \circ f \circ g^{-1}$. So when I write $$ [\Sigma // Diff(\Sigma), Fields] $$ this internal hom is that of the slice $\mathbf{H}_{/\mathbf{B}Diff(\Sigma)}$ where $\Sigma$ itself appears as the dependent type $$ \array{ \Sigma // Diff(\Sigma) \\ \downarrow \\ \mathbf{B}Diff(\Sigma) } $$ exhibiting the canonical action of $Diff(\Sigma)$, while Fields is regarded as equipped with the _trivial_ $\Sigma$-action, hence the dependent type $$ \array{ Fields \times \mathbf{B}\Sigma \\ \downarrow^{\mathrlap{p}_2} \\ \mathbf{B}Diff(\Sigma) } \,. $$ Then by the above conjugation-rule, we get the relation as claimed.

   Warning, as I tried to highlight, it’s important to note that I am talking about $[A//Sym(A), B]_{B Sym(A)}$, the internal hom formed in the category of types with $Sym(A)$-action.

   You probably computed the homs out of the action groupoids as such. Then it does not work.

   What I am using here is the following fact, discussed in some detail at infinity-action:

   an action of som $G$ on some $V$ is equivalently encoded in the bundle

   $$\array{ V &\to& V//G \\ && \downarrow \\ && \mathbf{B}G = \ast //G } \,.$$

   In particular the slice $\infty$-topos over $\mathbf{B}G$ is equivalent to the category of $G$ actions

   $$G Act(\mathbf{H}) \simeq \mathbf{H}_{/\mathbf{B}G} \,.$$

   Or in type-theoretic words: a $G$ action on $V$ is the same as a $\mathbf{B}G$-dependent type whose context extension to the global context is $V$.

   Now the key fact is this here:

   if $(V_1, \rho_1)$ and $(V_2, \rho_2)$ are two $G$-actions, then the internal hom in the slice /dependent over $\mathbf{B}G$ is

   1. the type of all maps $[V_1, V_2]$

   2. regarded as equipped with the $G$-action given by conjugation, hence the action where $g \in G$ acts on a function $f : V_1 \to V_2$ by $f \mapsto g \circ f \circ g^{-1}$.

   So when I write

   $$[\Sigma // Diff(\Sigma), Fields]$$

   this internal hom is that of the slice $\mathbf{H}_{/\mathbf{B}Diff(\Sigma)}$ where $\Sigma$ itself appears as the dependent type

   $$\array{ \Sigma // Diff(\Sigma) \\ \downarrow \\ \mathbf{B}Diff(\Sigma) }$$

   exhibiting the canonical action of $Diff(\Sigma)$, while Fields is regarded as equipped with the trivial $\Sigma$-action, hence the dependent type

   $$\array{ Fields \times \mathbf{B}\Sigma \\ \downarrow^{\mathrlap{p}_2} \\ \mathbf{B}Diff(\Sigma) } \,.$$

   Then by the above conjugation-rule, we get the relation as claimed.

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 14th 2013
   • (edited Nov 14th 2013)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAha, good! So now to the audience discussion: Q: So what is spacetime? A: It's the groupoid $\Sigma // Diff(\Sigma)$. Q: Remind me what $\Sigma$ is meant to be. I thought you said *it* was spacetime. You began with it, then decided it wasn't quite right. A: Well, $\Sigma$ is a homotopy fiber of the bundle $\Sigma//Diff(\Sigma) \to \mathbf{B}Diff(\Sigma)$. Q: So? What does this mean about my world? I click my fingers now. This is an event at a point in what? A: ???

   Aha, good!

   So now to the audience discussion:

   Q: So what is spacetime?

   A: It’s the groupoid $\Sigma // Diff(\Sigma)$.

   Q: Remind me what $\Sigma$ is meant to be. I thought you said it was spacetime. You began with it, then decided it wasn’t quite right.

   A: Well, $\Sigma$ is a homotopy fiber of the bundle $\Sigma//Diff(\Sigma) \to \mathbf{B}Diff(\Sigma)$.

   Q: So? What does this mean about my world? I click my fingers now. This is an event at a point in what?

   A: ???

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 14th 2013
   • (edited Nov 14th 2013)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIn other words, how to represent the idea of working in a context such as $\mathbf{B}\mathbf{Aut}(\Sigma)$ in ordinary language: >**Fact**. In terms of homotopy type theory, configuration spaces of a generally covariant theory over $\Sigma$ are precisely the ordinary configuration spaces of fields, but formed in the context $\mathbf{B}\mathbf{Aut}(\Sigma)$: >$$ \mathbf{Conf} =_{def} \;\;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Field}) : Type \,. $$ Or should we say that ordinary language isn't designed for this? We could say that the whole metaphysical debate hangs on a suitable interpretation of this situation. I guess we should be able to see the same thing in simpler situations. Let's take a set $X$. Then $[X, 2]$ are subsets of $X$. $[X, 2]/Sym(X)$ are equivalence classes of subset partioned by cardinality. What is it to think of $[X, 2] // Sym(X)$ as $$ X: \mathbf{B} Sym(X) \vdash X \to 2: Type ? $$ On this theme, I guess with $[X^n, 2] // Sym(X)$ we're looking at [Logic as Invariant Theory](http://golem.ph.utexas.edu/category/2012/01/logic_as_invarianttheory.html). Sometimes it seems I never got far away from higher Klein geometry.

   In other words, how to represent the idea of working in a context such as $\mathbf{B}\mathbf{Aut}(\Sigma)$ in ordinary language:

   Fact. In terms of homotopy type theory, configuration spaces of a generally covariant theory over $\Sigma$ are precisely the ordinary configuration spaces of fields, but formed in the context $\mathbf{B}\mathbf{Aut}(\Sigma)$:

   $$\mathbf{Conf} =_{def} \;\;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Field}) : Type \,.$$

   Or should we say that ordinary language isn’t designed for this? We could say that the whole metaphysical debate hangs on a suitable interpretation of this situation.

   I guess we should be able to see the same thing in simpler situations. Let’s take a set $X$. Then $[X, 2]$ are subsets of $X$. $[X, 2]/Sym(X)$ are equivalence classes of subset partioned by cardinality.

   What is it to think of $[X, 2] // Sym(X)$ as

   $$X: \mathbf{B} Sym(X) \vdash X \to 2: Type ?$$

   On this theme, I guess with $[X^n, 2] // Sym(X)$ we’re looking at Logic as Invariant Theory.

   Sometimes it seems I never got far away from higher Klein geometry.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeNov 14th 2013
   • (edited Nov 14th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI certainly think that in the end ordinary language is less designed for this than, well, homotopy type theory is. But still it will be good for your audience and also for ourselves to see how close we can get in ordinary language to capture this. Your example of subsets is a good one, as it indeed captures all of the phenomenon under discussion in a possibly simpler or at least simpler-looking situation. But yes, if asked in this context I would reply that, yes, in a generally covariant context $\Sigma // Diff(\Sigma)$ "is spacetime" for larger values of "is" than $\Sigma$. And I think this can be well motivated with the probe-picture of stacks/of physics. It should be plausible to your audience that the definition of physical entities such as spacetimes is "operational" in a sense. Namely what spacetime is we detect by probing it, say by putting point (particles) into it. Now we see that there are different such ways which however are supposed to be equivalent by general covariance. So spacetime must be such that it has probes given by maps into a space which are equivalent if related by a diffeomorphisms of this space. But that is what characterizes $\Sigma // Diff(\Sigma)$. Your example of finite sets with symmetric group actions is good to realize that there are many examples of this phenomenon in pure mathematics. For instance in the definition of [[symmetric spectrum]] and [[symmetric operad]] everything is labeled by finite sets equipped with their automorphism action, and it is for a very similar reason as in general covariance, it models the situation that things are labeled by finite sets in a way that is "generally covariant" with respect to their automorphisms. Have to run now. More later.

   I certainly think that in the end ordinary language is less designed for this than, well, homotopy type theory is. But still it will be good for your audience and also for ourselves to see how close we can get in ordinary language to capture this.

   Your example of subsets is a good one, as it indeed captures all of the phenomenon under discussion in a possibly simpler or at least simpler-looking situation.

   But yes, if asked in this context I would reply that, yes, in a generally covariant context $\Sigma // Diff(\Sigma)$ “is spacetime” for larger values of “is” than $\Sigma$.

   And I think this can be well motivated with the probe-picture of stacks/of physics.

   It should be plausible to your audience that the definition of physical entities such as spacetimes is “operational” in a sense. Namely what spacetime is we detect by probing it, say by putting point (particles) into it. Now we see that there are different such ways which however are supposed to be equivalent by general covariance. So spacetime must be such that it has probes given by maps into a space which are equivalent if related by a diffeomorphisms of this space. But that is what characterizes $\Sigma // Diff(\Sigma)$.

   Your example of finite sets with symmetric group actions is good to realize that there are many examples of this phenomenon in pure mathematics. For instance in the definition of symmetric spectrum and symmetric operad everything is labeled by finite sets equipped with their automorphism action, and it is for a very similar reason as in general covariance, it models the situation that things are labeled by finite sets in a way that is “generally covariant” with respect to their automorphisms.

   Have to run now. More later.

10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexSome more things I can imagine being asked: It seems that you first start with $\Sigma$, so that you then can form $\mathbf{B} Aut(\Sigma)$, and then form the action groupoid. How did you originally come up with the $\Sigma$? Is this the wrong way around? Perhaps the right kind of probing gives me a groupoid, and from that I recognise it as a special kind of action groupoid for a manifold. Did it need to be like that? There are plenty of smooth groupoids not of that form. Or is that the probing gives rise to a sheaf on $CartSp$, so there's my manifold. What does it mean to probe with a particle anyway? And why should I count two probings as equivalent? How would a comparable process work in the simple finite set case? I probe by withdrawing samples of different sizes. Two samples of the same size are equivalent. I must be dealing with a set of indistinguishable objects, and the moduli space is $X//Sym(X)$ for $X$ of cardinality equal to that of the largest successful probe. But here, because I imagine my finite objects in space, I'm inclined to think of them as distinguishable by their position. I think they're really just a set, but given I can't tell them apart, I work with $X//Sym(X)$. General relativity seems to add that extra spice that when finding critical points of the Hilbert-Einstein action, one is varying over worlds that can't exist. At least the catenary that the chain ends up in was one of a collection of possible curves.

    Some more things I can imagine being asked:

    It seems that you first start with $\Sigma$, so that you then can form $\mathbf{B} Aut(\Sigma)$, and then form the action groupoid. How did you originally come up with the $\Sigma$?

    Is this the wrong way around? Perhaps the right kind of probing gives me a groupoid, and from that I recognise it as a special kind of action groupoid for a manifold. Did it need to be like that? There are plenty of smooth groupoids not of that form. Or is that the probing gives rise to a sheaf on $CartSp$, so there’s my manifold.

    What does it mean to probe with a particle anyway? And why should I count two probings as equivalent?

    How would a comparable process work in the simple finite set case? I probe by withdrawing samples of different sizes. Two samples of the same size are equivalent. I must be dealing with a set of indistinguishable objects, and the moduli space is $X//Sym(X)$ for $X$ of cardinality equal to that of the largest successful probe.

    But here, because I imagine my finite objects in space, I’m inclined to think of them as distinguishable by their position. I think they’re really just a set, but given I can’t tell them apart, I work with $X//Sym(X)$.

    General relativity seems to add that extra spice that when finding critical points of the Hilbert-Einstein action, one is varying over worlds that can’t exist. At least the catenary that the chain ends up in was one of a collection of possible curves.

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex>Your example of finite sets with symmetric group actions is good to realize that there are many examples of this phenomenon in pure mathematics. When maths is properly written out in HoTT, are we going to see a lot of use of symmetry contexts? You'd think chunks of representation theory would happen like that. With types as propositions, it seemed to be about judging that something is the case on the basis that something else is assumed. Having $\mathbf{B} G$ as my context, seems different. Maybe I could say, "Assuming $G$-equivariance,..." But perhaps this is just another case of Hegel's subjective/objective logic distinction. Things can equally be interpreted metaphysically or in terms of judgements.

    Your example of finite sets with symmetric group actions is good to realize that there are many examples of this phenomenon in pure mathematics.

    When maths is properly written out in HoTT, are we going to see a lot of use of symmetry contexts? You’d think chunks of representation theory would happen like that.

    With types as propositions, it seemed to be about judging that something is the case on the basis that something else is assumed. Having $\mathbf{B} G$ as my context, seems different. Maybe I could say, “Assuming $G$-equivariance,…”

    But perhaps this is just another case of Hegel’s subjective/objective logic distinction. Things can equally be interpreted metaphysically or in terms of judgements.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2013
    • (edited Nov 14th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> It seems that you first start with $\Sigma$, so that you then can form $\mathbf{B} Aut(\Sigma)$, and then form the action groupoid. How did you originally come up with the $\Sigma$? Right, so I like to think about it like this: We start with choosing $\Sigma$ and so we say $$ \vdash \; \Sigma \colon Type $$ In the $\infty$-topos semantics this means a morphism $$ \ast \stackrel{\vdash \Sigma}{\longrightarrow} Obj $$ into the small object classified object. Given this, we can ask for its [[1-image]] factorization $$ \vdash \Sigma \;\colon\; \ast \longrightarrow im_1(\vdash \Sigma) \hookrightarrow Obj $$ One finds that this 1-image is precisely $im_1(\vdash \Sigma) \simeq \ast//\mathbf{Aut}(\Sigma) \simeq \ast // Diff(\Sigma) \simeq \mathbf{B}\mathbf{Aut}(\Sigma)$. And then $\Sigma$ with its action by $Diff(\Sigma)$ is the dependent type classified by the 1-image injection map, in that we have a pasting diagram of homotopy pullbacks of this form $$ \array{ \Sigma &\longrightarrow& \Sigma//Diff(\Sigma) &\longrightarrow& \widehat{Obj} \\ \downarrow &{}^{(pb)}& \downarrow &{}^{(pb)}& \downarrow \\ \ast &\stackrel{\vdash \Sigma}{\longrightarrow}& \mathbf{B}Diff(\Sigma) &\hookrightarrow& Obj } \,. $$ I guess this should make a good story when translated to ordinary language. Maybe like this: "In the universe of all possible spacetimes, choose the sub-universe of the spacetime $\Sigma$. In this context, $\Sigma$ is $\Sigma//Diff(\Sigma)$."

    It seems that you first start with $\Sigma$, so that you then can form $\mathbf{B} Aut(\Sigma)$, and then form the action groupoid. How did you originally come up with the $\Sigma$?

    Right, so I like to think about it like this:

    We start with choosing $\Sigma$ and so we say

    $$\vdash \; \Sigma \colon Type$$

    In the $\infty$-topos semantics this means a morphism

    $$\ast \stackrel{\vdash \Sigma}{\longrightarrow} Obj$$

    into the small object classified object. Given this, we can ask for its 1-image factorization

    $$\vdash \Sigma \;\colon\; \ast \longrightarrow im_1(\vdash \Sigma) \hookrightarrow Obj$$

    One finds that this 1-image is precisely $im_1(\vdash \Sigma) \simeq \ast//\mathbf{Aut}(\Sigma) \simeq \ast // Diff(\Sigma) \simeq \mathbf{B}\mathbf{Aut}(\Sigma)$.

    And then $\Sigma$ with its action by $Diff(\Sigma)$ is the dependent type classified by the 1-image injection map, in that we have a pasting diagram of homotopy pullbacks of this form

    $$\array{ \Sigma &\longrightarrow& \Sigma//Diff(\Sigma) &\longrightarrow& \widehat{Obj} \\ \downarrow &{}^{(pb)}& \downarrow &{}^{(pb)}& \downarrow \\ \ast &\stackrel{\vdash \Sigma}{\longrightarrow}& \mathbf{B}Diff(\Sigma) &\hookrightarrow& Obj } \,.$$

    I guess this should make a good story when translated to ordinary language. Maybe like this:

    “In the universe of all possible spacetimes, choose the sub-universe of the spacetime $\Sigma$. In this context, $\Sigma$ is $\Sigma//Diff(\Sigma)$.”

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItex> When maths is properly written out in HoTT, are we going to see a lot of use of symmetry contexts? You’d think chunks of representation theory would happen like that. Yes! I kept and keep trying to advertize this cool fact, in the hope that more people would start investigating it further: a basic but curious fact is that the _dependent_ type theory aspect of HoTT means essentially that _homotopy type theory in non-0-truncated contexts is equivariant homotopy theory/higher representation theory_. And in some sense the "generic" context is not 0-truncated in HoTT, so HoTT is "generically" about equivariant homotopy theory/higher representation theory. This will eventually become more pronounced in publications, I am sure.

    When maths is properly written out in HoTT, are we going to see a lot of use of symmetry contexts? You’d think chunks of representation theory would happen like that.

    Yes! I kept and keep trying to advertize this cool fact, in the hope that more people would start investigating it further:

    a basic but curious fact is that the dependent type theory aspect of HoTT means essentially that homotopy type theory in non-0-truncated contexts is equivariant homotopy theory/higher representation theory.

    And in some sense the “generic” context is not 0-truncated in HoTT, so HoTT is “generically” about equivariant homotopy theory/higher representation theory.

    This will eventually become more pronounced in publications, I am sure.

14. • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 14th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThere's that weird feeling of being caught up in a mystical creation myth again. Out of $\empty$ there arises $\ast$, then a universe. A choice from this gives us spacetime, from where we find its sub-universe. A configuration space is the internal hom from the spacetime to an object $\mathbf{Fields}$ in the context of the sub-universe. Continuing the mystical path, we might then think the choice of any one spacetime to be arbitrary. All must exist in some sense. As must all types of object $\mathbf{Fields}$. Do God's choices just range over any two types $\Sigma$ and $\mathbf{Fields}$? He just happens to have chosen $\Sigma$ for us at a certain scale to look like a pseudo-Riemannian smooth 0 type. My audience will truly think I've gone mad.

    There’s that weird feeling of being caught up in a mystical creation myth again.

    Out of $\empty$ there arises $\ast$, then a universe. A choice from this gives us spacetime, from where we find its sub-universe. A configuration space is the internal hom from the spacetime to an object $\mathbf{Fields}$ in the context of the sub-universe.

    Continuing the mystical path, we might then think the choice of any one spacetime to be arbitrary. All must exist in some sense. As must all types of object $\mathbf{Fields}$.

    Do God’s choices just range over any two types $\Sigma$ and $\mathbf{Fields}$? He just happens to have chosen $\Sigma$ for us at a certain scale to look like a pseudo-Riemannian smooth 0 type.

    My audience will truly think I’ve gone mad.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2013
    • (edited Nov 14th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Do God's choices just range over any two types $\Sigma$ and $\mathbf{Fields}$? To define a field theory, one needs roughly one more ingredient: the Lagrangian/action functional, which is a promotion of $\mathbf{Fields}$ to the context of the form $\mathbf{B}GL_1(E)$, for $E$ an $E_\infty$-ring. (There will be improvements on this statement in the context of [[tangent cohesion]]. When I find a calm moment, I should work that out more. ) But notice that for the field of gravity there is actually another context to be taken into account. Namely the moduli stack $\mathbf{Fields} = Gravity_n = Met_n$ of pseudo-Riemannian metrics in $n$ dimensions is itself a dependent type, namely it is $GL(n)//(O(n)\times GL(n)) \simeq \mathbf{B}O(n)$ regarded as a $\mathbf{B}GL(n)$-dependent type whose $\infty$-categorical semantics is $$ \array{ GL(n)//O(n) &\longrightarrow& \mathbf{B}O(n) \\ && \downarrow \\ && \mathbf{B}GL(n) } \,. $$ And also the spacetime manifold $\Sigma$ is, even before we put it into the general covariant conext over $\mathbf{B} Diff(\Sigma)$, to be regarded as dependent on the type $\mathbf{B}GL(n)$ via the map $\tau_X$ that modulates its tangent frame bundle $$ \array{ Frames(\Sigma) &\longrightarrow& \Sigma \\ && \downarrow^{\mathrlap{\tau_\Sigma}} \\ && \mathbf{B}GL(n) } \,. $$ This way a function $$ \mathbf{B}GL(n) \;\vdash\; \phi \;\colon \; \Sigma \longrightarrow \mathbf{Fields} $$ is equivalently a choice of reduction of the structure group of the frame bundle to an orthogonal bundle, and that is equivalently a field of gravity on $\Sigma$. (I think I discuss this somewhere at _[[general covariance]]_.) In general, those field theories which appear with the least "effort" in cohesive homtopy type theory are higher Chern-Simons-type field theories. A bunch of others is then induced from these by choosing boundary and "defect" structures of these "bulk" higher Chern-Simons theories. There is a hierachy of "HoTT-ly fundamental field theories" and "less HoTT-ly fundamental field theories" appearing as their boundaries and defects, which involves choosing ever more data. Now Einstein-gravity or similar is not "of higher Chern-Simons type". But for instance [[closed string field theory]] is.

    Do God’s choices just range over any two types $\Sigma$ and $\mathbf{Fields}$?

    To define a field theory, one needs roughly one more ingredient: the Lagrangian/action functional, which is a promotion of $\mathbf{Fields}$ to the context of the form $\mathbf{B}GL_1(E)$, for $E$ an $E_\infty$-ring.

    (There will be improvements on this statement in the context of tangent cohesion. When I find a calm moment, I should work that out more. )

    But notice that for the field of gravity there is actually another context to be taken into account. Namely the moduli stack $\mathbf{Fields} = Gravity_n = Met_n$ of pseudo-Riemannian metrics in $n$ dimensions is itself a dependent type, namely it is $GL(n)//(O(n)\times GL(n)) \simeq \mathbf{B}O(n)$ regarded as a $\mathbf{B}GL(n)$-dependent type whose $\infty$-categorical semantics is

    $$\array{ GL(n)//O(n) &\longrightarrow& \mathbf{B}O(n) \\ && \downarrow \\ && \mathbf{B}GL(n) } \,.$$

    And also the spacetime manifold $\Sigma$ is, even before we put it into the general covariant conext over $\mathbf{B} Diff(\Sigma)$, to be regarded as dependent on the type $\mathbf{B}GL(n)$ via the map $\tau_X$ that modulates its tangent frame bundle

    $$\array{ Frames(\Sigma) &\longrightarrow& \Sigma \\ && \downarrow^{\mathrlap{\tau_\Sigma}} \\ && \mathbf{B}GL(n) } \,.$$

    This way a function

    $$\mathbf{B}GL(n) \;\vdash\; \phi \;\colon \; \Sigma \longrightarrow \mathbf{Fields}$$

    is equivalently a choice of reduction of the structure group of the frame bundle to an orthogonal bundle, and that is equivalently a field of gravity on $\Sigma$.

    (I think I discuss this somewhere at general covariance.)

    In general, those field theories which appear with the least “effort” in cohesive homtopy type theory are higher Chern-Simons-type field theories. A bunch of others is then induced from these by choosing boundary and “defect” structures of these “bulk” higher Chern-Simons theories. There is a hierachy of “HoTT-ly fundamental field theories” and “less HoTT-ly fundamental field theories” appearing as their boundaries and defects, which involves choosing ever more data.

    Now Einstein-gravity or similar is not “of higher Chern-Simons type”. But for instance closed string field theory is.

16. • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 15th 2013
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI guess after $$ \Sigma : \mathbf{B} Aut(\Sigma) \vdash \Sigma: Type $$ we get things like $$ \Sigma : \mathbf{B} Aut(\Sigma) \vdash IsSet(\Sigma): Type. $$ Is that to be thought of as, although $\Sigma$ in that context is the groupoid $\Sigma // \mathbf{B} Aut(\Sigma)$, we can still wonder if the fibre above $\ast // \mathbf{B} Aut(\Sigma)$ is a set?

    I guess after

    $$\Sigma : \mathbf{B} Aut(\Sigma) \vdash \Sigma: Type$$

    we get things like

    $$\Sigma : \mathbf{B} Aut(\Sigma) \vdash IsSet(\Sigma): Type.$$

    Is that to be thought of as, although $\Sigma$ in that context is the groupoid $\Sigma // \mathbf{B} Aut(\Sigma)$, we can still wonder if the fibre above $\ast // \mathbf{B} Aut(\Sigma)$ is a set?

17. • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeNov 15th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGoing back to the equivalence $$[A//Sym(A), B]_{B Sym(A)} = [A//Sym(A), B]$$ it may be worth a reminder that in HoTT, this is just the induction principle for dependent sums. We have a type $X$ (here $B Sym(A)$), a type family $Y:X\to Type$ (here $A$ with its $Sym(A)$-action), and a type $Z$ (here $B$), and we can consider the dependent sum $\sum_{x:X} Y(x)$ (here $A//Sym(A)$). The induction principle of this dependent sum says that to give a function $$\Big(\sum_{x:X} Y(x)\Big) \to Z$$ is equivalent to give a dependent function $$ \prod_{x:X} (Y(x) \to Z). $$ or equivalently a map $Y(x)\to Z$ in context $x:X$. A more general version of this equivalence, where $Z$ can depend on $X$ and $Y$ as well, is (2.15.9) in the HoTT Book. And the special case where $Y$ is independent of $X$ is just the exponential law for the cartesian closed category of types: $$ ((X\times Y) \to Z) = (X\to (Y\to Z)) $$

    Going back to the equivalence

    $$[A//Sym(A), B]_{B Sym(A)} = [A//Sym(A), B]$$

    it may be worth a reminder that in HoTT, this is just the induction principle for dependent sums. We have a type $X$ (here $B Sym(A)$), a type family $Y:X\to Type$ (here $A$ with its $Sym(A)$-action), and a type $Z$ (here $B$), and we can consider the dependent sum $\sum_{x:X} Y(x)$ (here $A//Sym(A)$). The induction principle of this dependent sum says that to give a function

    $$\Big(\sum_{x:X} Y(x)\Big) \to Z$$

    is equivalent to give a dependent function

    $$\prod_{x:X} (Y(x) \to Z).$$

    or equivalently a map $Y(x)\to Z$ in context $x:X$. A more general version of this equivalence, where $Z$ can depend on $X$ and $Y$ as well, is (2.15.9) in the HoTT Book. And the special case where $Y$ is independent of $X$ is just the exponential law for the cartesian closed category of types:

    $$((X\times Y) \to Z) = (X\to (Y\to Z))$$
18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeNov 16th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexPerhaps a way to clarify how to think of $\Sigma//Diff(\Sigma)$ is to think first of other action groupoids and orbifolds. Here's how I might try to explain this to someone not familiar with it. To begin with, we might have just a set of points. Now perhaps we know that some of these points are actually to be regarded as the *same* as some other of these points. Perhaps our set of points is $\mathbb{R}^2$, a 2-dimensional space, but we happen to know that for whatever reason God has decided that space should be symmetric under a $180^\circ$ rotation about the origin. Then we can think instead of the quotient of our set of points by an equivalence relation, but it's better to perform a *homotopy* quotient. Here we have a group $G$, namely the 2-element group $\mathbb{Z}/2$, acting on our set of points, and for each point $x$ and $g\in G$, we add an isomorphism from $x$ to $g\cdot x$ labeled by $g$. If the action is free, we end up with something equivalent to a set again, but in general we have points (like the origin) that end up with isotropy (they are now the same as themselves in nontrivial ways). Why is it important to make the homotopy quotient rather than the ordinary one? Well, consider a different case, when the group $G$ is the infinite cyclic group, with the generator acting on $\mathbb{R}^2$ by translation 1 unit to the right. This is a free action, so the homotopy quotient is just the ordinary quotient, namely an infinite cylindrical world. This quotient world has nontrivial $\pi_1$: if we start at a point and go around the cylinder, our path is not contractible. Up in the original world, we can see this noncontractibility by noting that our path "around the cylinder" lifts to a path connecting two *different* points, so of course it can't be contracted back to a single point while leaving the endpoints fixed. In the case of the $\mathbb{Z}/2$ action by $180^\circ$ rotation, the quotient is a "cone", which looks as though it would have trivial $\pi_1$, if we could "pull strings over the cone point". But if we go around the cone once in this quotient world, then in the original world, the lifted path again connects two different points, and hence should *not* be able to be contracted over the cone point. In order to remember this information in the quotient, we equip the cone point with an isotropy group. The same reasoning suggests that if we go around the cone *twice*, we *should* be able to contract that loop back over the cone point; thus we need to record the specific isotropy group $\mathbb{Z}/2$ in order to "quantify the pointiness" of the cone. In conclusion, if God has decided that the world should be covariant under a fixed group $G$, She then has to choose a spacetime that is acted on by $G$. The homotopy quotient by this action is then the "moduli space of points", in which the $G$-action has been taken into account by identifying points that should be the same. The prescription of GR is similar, but a bit different: rather than fixing the group of covariance at the outset, we demand instead that the theory be covariant under *all* automorphisms of spacetime. In other words, God chooses the spacetime manifold $\Sigma$ first, and *then* the group $G$ is determined as $Diff(\Sigma)$. But after that, the construction is the same.

    Perhaps a way to clarify how to think of $\Sigma//Diff(\Sigma)$ is to think first of other action groupoids and orbifolds. Here’s how I might try to explain this to someone not familiar with it.

    To begin with, we might have just a set of points.

    Now perhaps we know that some of these points are actually to be regarded as the same as some other of these points. Perhaps our set of points is $\mathbb{R}^2$, a 2-dimensional space, but we happen to know that for whatever reason God has decided that space should be symmetric under a $180^\circ$ rotation about the origin. Then we can think instead of the quotient of our set of points by an equivalence relation, but it’s better to perform a homotopy quotient. Here we have a group $G$, namely the 2-element group $\mathbb{Z}/2$, acting on our set of points, and for each point $x$ and $g\in G$, we add an isomorphism from $x$ to $g\cdot x$ labeled by $g$. If the action is free, we end up with something equivalent to a set again, but in general we have points (like the origin) that end up with isotropy (they are now the same as themselves in nontrivial ways).

    Why is it important to make the homotopy quotient rather than the ordinary one? Well, consider a different case, when the group $G$ is the infinite cyclic group, with the generator acting on $\mathbb{R}^2$ by translation 1 unit to the right. This is a free action, so the homotopy quotient is just the ordinary quotient, namely an infinite cylindrical world. This quotient world has nontrivial $\pi_1$: if we start at a point and go around the cylinder, our path is not contractible. Up in the original world, we can see this noncontractibility by noting that our path “around the cylinder” lifts to a path connecting two different points, so of course it can’t be contracted back to a single point while leaving the endpoints fixed.

    In the case of the $\mathbb{Z}/2$ action by $180^\circ$ rotation, the quotient is a “cone”, which looks as though it would have trivial $\pi_1$, if we could “pull strings over the cone point”. But if we go around the cone once in this quotient world, then in the original world, the lifted path again connects two different points, and hence should not be able to be contracted over the cone point. In order to remember this information in the quotient, we equip the cone point with an isotropy group. The same reasoning suggests that if we go around the cone twice, we should be able to contract that loop back over the cone point; thus we need to record the specific isotropy group $\mathbb{Z}/2$ in order to “quantify the pointiness” of the cone.

    In conclusion, if God has decided that the world should be covariant under a fixed group $G$, She then has to choose a spacetime that is acted on by $G$. The homotopy quotient by this action is then the “moduli space of points”, in which the $G$-action has been taken into account by identifying points that should be the same.

    The prescription of GR is similar, but a bit different: rather than fixing the group of covariance at the outset, we demand instead that the theory be covariant under all automorphisms of spacetime. In other words, God chooses the spacetime manifold $\Sigma$ first, and then the group $G$ is determined as $Diff(\Sigma)$. But after that, the construction is the same.

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2013
    • (edited Nov 17th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, I don't quite follow #17 right now. But notation (my notation, possibly) may be misleading for what we want to express here. The equivalence in categorical semantics should be $$ [A//G, Z]_{\mathbf{B} G} \simeq [A,Z]//G $$ where on the left we have the total space of the internal hom in the slice and on the right we have the homotopy quotient of $G$ acting on the internal hom of the fibers in the ambient context. Let me see about the type theory syntax for this..., if we write $$ p \colon \mathbf{B}G \; \vdash \; (A//G)(p) \colon Type $$ for the action of $G$ on $A$ as a dependent type, then the internal hom $[A//G, Z]_{\mathbf{B}G}$ in that context is the semantics for $$ p \colon \mathbf{B}G \vdash ((A//G)(p) \to Z) \colon Type $$ and so the left hand side should be $$ \vdash \; \left(\underset{p \colon\mathbf{B}G}{\sum} \left(\left(A//G\right)\left(p\right) \to Z\right) \right) \colon Type $$ (with dependent sum as opposed to dependent product. ) Now I am not sure how to correctly type-set (pun) the right hand side. I want to say that $A = (A//G)(p)$. If I do that indeed I end up with the same line as the previous one for the syntax also of the right hand side.

    Hm, I don’t quite follow #17 right now. But notation (my notation, possibly) may be misleading for what we want to express here.

    The equivalence in categorical semantics should be

    $$[A//G, Z]_{\mathbf{B} G} \simeq [A,Z]//G$$

    where on the left we have the total space of the internal hom in the slice and on the right we have the homotopy quotient of $G$ acting on the internal hom of the fibers in the ambient context.

    Let me see about the type theory syntax for this…, if we write

    $$p \colon \mathbf{B}G \; \vdash \; (A//G)(p) \colon Type$$

    for the action of $G$ on $A$ as a dependent type, then the internal hom $[A//G, Z]_{\mathbf{B}G}$ in that context is the semantics for

    $$p \colon \mathbf{B}G \vdash ((A//G)(p) \to Z) \colon Type$$

    and so the left hand side should be

    $$\vdash \; \left(\underset{p \colon\mathbf{B}G}{\sum} \left(\left(A//G\right)\left(p\right) \to Z\right) \right) \colon Type$$

    (with dependent sum as opposed to dependent product. )

    Now I am not sure how to correctly type-set (pun) the right hand side. I want to say that $A = (A//G)(p)$. If I do that indeed I end up with the same line as the previous one for the syntax also of the right hand side.

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2013
    • (edited Nov 17th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexJust to be clear, the equivalence, that I, at least, have in mind is the one which is the topic of what is currently prop. 3 and remark 5 [here at: infinity-action -- Conjugation action](http://ncatlab.org/nlab/show/infinity-action#CartesianClosedMonoidalStructure)

    Just to be clear, the equivalence, that I, at least, have in mind is the one which is the topic of what is currently prop. 3 and remark 5 here at: infinity-action – Conjugation action

21. • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeNov 17th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOh... maybe you are saying something even more trivial than I thought you were saying. (-: Are you just saying that the equivalence between spaces over $B G$ and spaces with a $G$-action preserves internal-homs, and that under this equivalence the "total space" functor corresponds to the "homotopy quotient" functor?

    Oh… maybe you are saying something even more trivial than I thought you were saying. (-: Are you just saying that the equivalence between spaces over $B G$ and spaces with a $G$-action preserves internal-homs, and that under this equivalence the “total space” functor corresponds to the “homotopy quotient” functor?

22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexThe statement I am talking about is that the internal hom of G-actions/spaces over $\mathbf{B}G$ sends two actions to the conjugation action on the space of all maps between the types being acted on.

    The statement I am talking about is that the internal hom of G-actions/spaces over $\mathbf{B}G$ sends two actions to the conjugation action on the space of all maps between the types being acted on.

23. • CommentRowNumber23.
    • CommentAuthorspitters
    • CommentTimeNov 17th 2013
    • (edited Nov 17th 2013)
    • PermaLink
    Author: spitters
    Format: MarkdownItexMike's explanation of adding a group action of Z/2Z is reminiscent of Wraith's work on Galois theory in a topos. In the simple case of algebraic construction of the complex numbers, it is irrelevant whether we extend our field with either i or -i, so we better keep the action in mind and work in a new topos. [Galois theory in a topos](http://www.sciencedirect.com/science/article/pii/0022404980901085/pdf?md5=e570ad5355c50aa059a9f6d223e09197&pid=1-s2.0-0022404980901085-main.pdf&_valck=1) Wraith's work is closely connected Grothendieck's Galois theory.

    Mike’s explanation of adding a group action of Z/2Z is reminiscent of Wraith’s work on Galois theory in a topos. In the simple case of algebraic construction of the complex numbers, it is irrelevant whether we extend our field with either i or -i, so we better keep the action in mind and work in a new topos. Galois theory in a topos Wraith’s work is closely connected Grothendieck’s Galois theory.

24. • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeNov 17th 2013
    • (edited Nov 17th 2013)
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex@Urs, I don't think any knowledge about the conjugation action is needed for the statement as I currently understand it. On the right hand side, you have the internal hom of two spaces with $G$-action (whatever that may be) followed by the homotopy quotient. On the left hand side, you have the internal hom of the corresponding two spaces over $B G$ (whatever that may be) followed by the total space. So it's enough to know that whatever the internal homs are, they match up on either side, as do the quotient and total space functors.

    @Urs, I don’t think any knowledge about the conjugation action is needed for the statement as I currently understand it. On the right hand side, you have the internal hom of two spaces with $G$-action (whatever that may be) followed by the homotopy quotient. On the left hand side, you have the internal hom of the corresponding two spaces over $B G$ (whatever that may be) followed by the total space. So it’s enough to know that whatever the internal homs are, they match up on either side, as do the quotient and total space functors.

25. • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2013
    • (edited Nov 17th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThere might be different things under discussion. David started out referring to the conjugation action and I was reacting to that: the nice fact about the conceptualization of "general covariance" is that the moduli stack of generally covariant fields $[\Sigma, \mathbf{Fields}]//Diff(\Sigma)$ is equivalently just the mapping space from $\Sigma$ to $\mathbf{Fields}$ in the context of $G$-actions. I agree that this is trivial when viewed from the right angle (as it goes in maths). But this conjugation-action statement is specifically what appears in the discussion of general covariance. Other statements might be more interesting in themselves, of course.

    There might be different things under discussion. David started out referring to the conjugation action and I was reacting to that:

    the nice fact about the conceptualization of “general covariance” is that the moduli stack of generally covariant fields $[\Sigma, \mathbf{Fields}]//Diff(\Sigma)$ is equivalently just the mapping space from $\Sigma$ to $\mathbf{Fields}$ in the context of $G$-actions.

    I agree that this is trivial when viewed from the right angle (as it goes in maths). But this conjugation-action statement is specifically what appears in the discussion of general covariance.

    Other statements might be more interesting in themselves, of course.

26. • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeNov 17th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, okay, I see --- it's also important to identify the *right* hand side with the thing you expect.

    Ah, okay, I see — it’s also important to identify the right hand side with the thing you expect.

27. • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeNov 17th 2013
    • (edited Nov 17th 2013)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, good. Now let's talk about this specific statement in the type theory. It should become a complete triviality there, but maybe one that is usefully made explicit. Above I tried it like this: the type theoretic expression $$ (A//G)(p) \to Z $$ is manifestly two things at the same time: 1. when read as a function type in context $p \colon \mathbf{B} G$ it is the internal hom of $G$-actions; 1. when read with $p \colon \mathbf{B} G$ understood as the canonical term that witnesses the pointed connectedness of $\mathbf{B}G$, then it is rather $A \to Z$ and the conjugation action on that is "clear". Now you will be able to refine this attempt of mine to something more precise and more useful. Could you give it a try?

    Okay, good. Now let’s talk about this specific statement in the type theory. It should become a complete triviality there, but maybe one that is usefully made explicit.

    Above I tried it like this: the type theoretic expression

    $$(A//G)(p) \to Z$$

    is manifestly two things at the same time:

    1. when read as a function type in context $p \colon \mathbf{B} G$ it is the internal hom of $G$-actions;

    2. when read with $p \colon \mathbf{B} G$ understood as the canonical term that witnesses the pointed connectedness of $\mathbf{B}G$, then it is rather $A \to Z$ and the conjugation action on that is “clear”.

    Now you will be able to refine this attempt of mine to something more precise and more useful. Could you give it a try?

28. • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeNov 18th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIt's not clear to me that the statement we're talking about can actually be made in the type theory, since we so far lack a formalization of $\infty$-actions other than "spaces over $\mathbf{B}G$" (due to the problem of infinite objects). We can say something partial, though, which is that the transport action of a loop in $\mathbf{B}G$ (i.e. an element of $G$) on a function type (formed in context $p:\mathbf{B} G$) is given by conjugation. This is essentially (2.9.4) in the book.

    It’s not clear to me that the statement we’re talking about can actually be made in the type theory, since we so far lack a formalization of $\infty$-actions other than “spaces over $\mathbf{B}G$” (due to the problem of infinite objects). We can say something partial, though, which is that the transport action of a loop in $\mathbf{B}G$ (i.e. an element of $G$) on a function type (formed in context $p:\mathbf{B} G$) is given by conjugation. This is essentially (2.9.4) in the book.

29. • CommentRowNumber29.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 18th 2013
    • (edited Nov 18th 2013)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI was hoping that type theory would allow a mode of expression which could help philosophers come to terms with how they must adjust their notion of sameness, but I begin to wonder whether it isn't easier just to speak externally, as in #18. I mean it would be great if we could have some simple constructions in the context $\mathbf{B} G$, and then say >$G$-equivariantly, [something simple], where [something simple] would involve traditional language of entities with properties in relation to each other. We spoke above about illustrating what was happening with simple permutation groups on finite sets. Say I have a set, $B$, of 5 indiscernible balls in a box, each of which can be coloured in 3 ways. I might take the state space to be $[B, 3]$, of cardinality 243. But then I think that I can't tell the difference between any two versions of 2 reds, 2 greens and a blue, so I decide to chop down to $[B, 3]/Sym(B)$, a set of cardinality 21 (I think). We know the problems with this, so we change to $[B, 3]//Sym(B)$, a groupoid of cardinality 243/120. (By the way, is groupoid cardinality definable within HoTT?) OK, now I have represented the fact that any colouring of 2 reds, 2 greens and a blue are equivalent, but that still I'd notice if a green and a red were swapped. Now could I get around the problem of someone worried about the apparent 5-ness of the balls, with the moduli of balls being $B//Sym(B)$ of cardinality 1/24, by being able to say >Sym(B)-equivariantly, there are 5 balls?

    I was hoping that type theory would allow a mode of expression which could help philosophers come to terms with how they must adjust their notion of sameness, but I begin to wonder whether it isn’t easier just to speak externally, as in #18. I mean it would be great if we could have some simple constructions in the context $\mathbf{B} G$, and then say

    $G$-equivariantly, [something simple],

    where [something simple] would involve traditional language of entities with properties in relation to each other.

    We spoke above about illustrating what was happening with simple permutation groups on finite sets. Say I have a set, $B$, of 5 indiscernible balls in a box, each of which can be coloured in 3 ways. I might take the state space to be $[B, 3]$, of cardinality 243. But then I think that I can’t tell the difference between any two versions of 2 reds, 2 greens and a blue, so I decide to chop down to $[B, 3]/Sym(B)$, a set of cardinality 21 (I think).

    We know the problems with this, so we change to $[B, 3]//Sym(B)$, a groupoid of cardinality 243/120. (By the way, is groupoid cardinality definable within HoTT?)

    OK, now I have represented the fact that any colouring of 2 reds, 2 greens and a blue are equivalent, but that still I’d notice if a green and a red were swapped.

    Now could I get around the problem of someone worried about the apparent 5-ness of the balls, with the moduli of balls being $B//Sym(B)$ of cardinality 1/24, by being able to say

    Sym(B)-equivariantly, there are 5 balls?

30. • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeNov 18th 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> By the way, is groupoid cardinality definable within HoTT? The cardinality of a 1-type is definable, since it's just defined in terms of the cardinality of the sets $\pi_1$ and $\pi_0$. Same for $n$-types for any finite $n$. > Sym(B)-equivariantly, there are 5 balls? Yes, I think that's true. If we interpret the statement "there are five balls" as "${|X|}=5$", with cardinality $|-|$ being defined as in chapter 10 of the book, then since cardinalities are the elements of $\Vert Set\Vert_0$, the statement ${|X|}=5$ is equivalent to $\Vert X \simeq N_5\Vert$, where $N_5$ is the canonical 5-element set. Since this is a mere proposition, its truth is reflected by surjections of contexts. And the inclusion of the point $\ast \to B G$ is a surjection, while when we regard $X$ as acted on by $Aut(X)$, its fiber over the point of $B Aut(X)$ is the original set $X$ itself.

    By the way, is groupoid cardinality definable within HoTT?

    The cardinality of a 1-type is definable, since it’s just defined in terms of the cardinality of the sets $\pi_1$ and $\pi_0$. Same for $n$-types for any finite $n$.

    Sym(B)-equivariantly, there are 5 balls?

    Yes, I think that’s true. If we interpret the statement “there are five balls” as “${|X|}=5$”, with cardinality $|-|$ being defined as in chapter 10 of the book, then since cardinalities are the elements of $\Vert Set\Vert_0$, the statement ${|X|}=5$ is equivalent to $\Vert X \simeq N_5\Vert$, where $N_5$ is the canonical 5-element set. Since this is a mere proposition, its truth is reflected by surjections of contexts. And the inclusion of the point $\ast \to B G$ is a surjection, while when we regard $X$ as acted on by $Aut(X)$, its fiber over the point of $B Aut(X)$ is the original set $X$ itself.