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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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 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 25th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItex(1) Just as I thought I had the covariance story straight, why doesn't the following work? We have a map in $\mathbf{H}$ from the delooping of $Diff(X)$ to the terminal object. We therefore have a base change map, $H/\ast \to H/\mathbf{B} Diff$, whose left adjoint is dependent sum. Expressing the adjoint relationship for $X$ with the obvious $Diff(X)$ action: $$ Hom_{H/\ast}(\sum_{\mathbf{B} Diff \to \ast} X, \mathbf{Fields}) \cong Hom_{H/\mathbf{B} Diff}(X, \mathbf{Fields} \times \mathbf{B} Diff). $$ But isn't the left hand side $$ Hom_{H/\ast}(X//Diff(X), \mathbf{Fields})? $$ (2) There was quite an industry a few years ago in philosophy of physics working out how much could be done constructively, e.g., was Gleason's theorem constructive. If not, and physics needs such theorems, this was supposed to be another argument for classical maths. If we now see logic as a fragment of HoTT, we must think about the appropriateness of the whole type system. Could we say that this is purely down to the practical matter of finding a type system/ that's adequate. Whether or not classical principles should be included is no different a kind of choice than whether or not we want, say, cohesion. Is this a good way to see things? on this theme, is there anything to be said about how the cohesion axioms interact with the addition of classical axioms, $AC_n$ and $LEM_n$?

   (1) Just as I thought I had the covariance story straight, why doesn’t the following work?

   We have a map in $\mathbf{H}$ from the delooping of $Diff(X)$ to the terminal object. We therefore have a base change map, $H/\ast \to H/\mathbf{B} Diff$, whose left adjoint is dependent sum. Expressing the adjoint relationship for $X$ with the obvious $Diff(X)$ action:

   $$Hom_{H/\ast}(\sum_{\mathbf{B} Diff \to \ast} X, \mathbf{Fields}) \cong Hom_{H/\mathbf{B} Diff}(X, \mathbf{Fields} \times \mathbf{B} Diff).$$

   But isn’t the left hand side

   $$Hom_{H/\ast}(X//Diff(X), \mathbf{Fields})?$$

   (2) There was quite an industry a few years ago in philosophy of physics working out how much could be done constructively, e.g., was Gleason’s theorem constructive. If not, and physics needs such theorems, this was supposed to be another argument for classical maths. If we now see logic as a fragment of HoTT, we must think about the appropriateness of the whole type system. Could we say that this is purely down to the practical matter of finding a type system/ that’s adequate. Whether or not classical principles should be included is no different a kind of choice than whether or not we want, say, cohesion. Is this a good way to see things?

   on this theme, is there anything to be said about how the cohesion axioms interact with the addition of classical axioms, $AC_n$ and $LEM_n$?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 25th 2013
   • (edited Nov 25th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHi David, concering 1): yes, but in the discussion at _[[general covariance]]_ we are considering the _internal_ hom instead of the external one. What you consider above is in words "If we map $G$-equivariantly out of a $G$-action into a trivial $G$-action, then all elements in the domain related by the $G$-action must go to the same element in the codomain, hence the map factors throgh the projection onto the quotient of the domain by the action". But over at _[[general covariance]]_ we are genuinely in the internal perspective. Given two actions, we form the internal hom which is again a space equipped with an action, namely crucially is the moduli space of generally covariant fields. Concerning constructivism in physics: I'd say one has to be careful with picking an isolated statement in physics and asking for how constructive it is without first asking about how to formulate the whole foundations of physics in which that statement appears. For instance in the [[Bohr topos]] perspective the natural internal formulation of states is (as discussed there) externally the [[quasi-states]] and so Gleason's theorem does not appear internally at all and is instead only used externally to verify that the internal sytanx has the expected external semantics (for $dim (space-of-states) \gt 2$). Concering this question: > Whether or not classical principles should be included is no different a kind of choice than whether or not we want, say, cohesion. Is this a good way to see things? I would think so. Finally concerning this question: > on this theme, is there anything to be said about how the cohesion axioms interact with the addition of classical axioms, ACn and LEMn? To the extent that classicality axioms prohibit interpretation in higher stacks semantics (which generically they do) assuming them will tend to make cohesion be only trivially realized. But here, too, one has to be careful: one point of cohesion is that via the [[sharp modality]] it does include an "external universe" and that may be much "more classical" then the full universe, notably it may be the non-stacky $\infty Grpd$ (possibly with AC) included as the discrete objects inside a stacky context which does not verify AC in general.

   Hi David,

   concering 1): yes, but in the discussion at general covariance we are considering the internal hom instead of the external one.

   What you consider above is in words “If we map $G$-equivariantly out of a $G$-action into a trivial $G$-action, then all elements in the domain related by the $G$-action must go to the same element in the codomain, hence the map factors throgh the projection onto the quotient of the domain by the action”.

   But over at general covariance we are genuinely in the internal perspective. Given two actions, we form the internal hom which is again a space equipped with an action, namely crucially is the moduli space of generally covariant fields.

   Concerning constructivism in physics: I’d say one has to be careful with picking an isolated statement in physics and asking for how constructive it is without first asking about how to formulate the whole foundations of physics in which that statement appears. For instance in the Bohr topos perspective the natural internal formulation of states is (as discussed there) externally the quasi-states and so Gleason’s theorem does not appear internally at all and is instead only used externally to verify that the internal sytanx has the expected external semantics (for $dim (space-of-states) \gt 2$).

   Concering this question:

   Whether or not classical principles should be included is no different a kind of choice than whether or not we want, say, cohesion. Is this a good way to see things?

   I would think so.

   Finally concerning this question:

   on this theme, is there anything to be said about how the cohesion axioms interact with the addition of classical axioms, ACn and LEMn?

   To the extent that classicality axioms prohibit interpretation in higher stacks semantics (which generically they do) assuming them will tend to make cohesion be only trivially realized.

   But here, too, one has to be careful: one point of cohesion is that via the sharp modality it does include an “external universe” and that may be much “more classical” then the full universe, notably it may be the non-stacky $\infty Grpd$ (possibly with AC) included as the discrete objects inside a stacky context which does not verify AC in general.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 25th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexBrilliant, thanks. I don't know why I always forget the internal hom issue. So in the future, we'll see the mathematician's task as devising interesting type theories and telling us what can be demonstrated in that type theory. While the physicist will select a type theory that allows him or her to talk about, and calculate, the things of interest -- spacetime, fields, etc. But maybe we'll find some especially rich type theories that are almost unavoidable.

   Brilliant, thanks. I don’t know why I always forget the internal hom issue.

   So in the future, we’ll see the mathematician’s task as devising interesting type theories and telling us what can be demonstrated in that type theory. While the physicist will select a type theory that allows him or her to talk about, and calculate, the things of interest – spacetime, fields, etc.

   But maybe we’ll find some especially rich type theories that are almost unavoidable.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeNov 25th 2013
   • (edited Nov 25th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> But maybe we’ll find some especially rich type theories that are almost unavoidable. You know that I have played before with thinking about what might single out the axioms of [[differential cohesion]] among all possible systems of modalities that one might consider. Recently I came to think that I should draw the full diagram of [[shape modality]] $\int$, [[flat modality]] $\flat$, [[sharp modality]] $\sharp$, [[reduction modality]] ®. [[infinitesimal shape modality]] $\oint$, [[infinitesimal flat modality]] $\flat_{inf}$ as follows, in order to highlight the special structure we see here: $$ \array{ && ® \\ && \bot \\ \int &\subset& \oint \\ \bot && \bot \\ \flat &\subset & \flat_{inf} \\ \bot \\ \sharp } $$ Here the inclusion means inclusion of modal types. That diagram makes clear that the axioms of differential cohesion follow some pattern. That might point to an origin of these axioms independent of the way we find them by looking at their semantics.

   But maybe we’ll find some especially rich type theories that are almost unavoidable.

   You know that I have played before with thinking about what might single out the axioms of differential cohesion among all possible systems of modalities that one might consider.

   Recently I came to think that I should draw the full diagram of shape modality $\int$, flat modality $\flat$, sharp modality $\sharp$, reduction modality ®. infinitesimal shape modality $\oint$, infinitesimal flat modality $\flat_{inf}$ as follows, in order to highlight the special structure we see here:

   $$\array{ && ® \\ && \bot \\ \int &\subset& \oint \\ \bot && \bot \\ \flat &\subset & \flat_{inf} \\ \bot \\ \sharp }$$

   Here the inclusion means inclusion of modal types. That diagram makes clear that the axioms of differential cohesion follow some pattern. That might point to an origin of these axioms independent of the way we find them by looking at their semantics.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 25th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI wonder if we need to pan out a bit. Is there some collection of type theories on which some operation adds in modalities? Presumably there will be a Stone duality between HoTTs and their collections of models, as [here](http://nforum.mathforge.org/discussion/4623/duality-for-homotopy-type-theories/?Focus=37603#Comment_37603). Can't we have some monad/comonad-like operation adding in modalities on the syntax side? Steve Awodey and students are looking at Stone duality for higher-order modal logic.

   I wonder if we need to pan out a bit. Is there some collection of type theories on which some operation adds in modalities?

   Presumably there will be a Stone duality between HoTTs and their collections of models, as here. Can’t we have some monad/comonad-like operation adding in modalities on the syntax side?

   Steve Awodey and students are looking at Stone duality for higher-order modal logic.