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.
   • CommentAuthorMichael_Bachtold
   • CommentTimeMay 13th 2015
   • (edited May 13th 2015)
   • PermaLink
   Author: Michael_Bachtold
   Format: MarkdownItexFollowing [this discussion](http://nforum.mathforge.org/discussion/6583/differential-operators-as-cokleisli-morphisms-for-the-jet-comonad/?Focus=53301#Comment_53301), I take the opportunity to articulate some confusions I have, regarding the notions of path and identity in the context of cohesion. Contrary to the situation in "bare" homotopy type theory, it seems to me that "path" and "identity" no longer mean the same for cohesive types. It's maybe easiest to ask some concrete questions (apologies if these are completely misguided): 1. If I consider a manifold as a cohesive type, for concreteness the unit circle $S^1$. Is it right that there are no non-trivial identities between points of $S^1$? So $S^1$ is an h-set? If I had considered the real line $R$, the same applies and moreover $R\neq *$? 2. Is it right that there are plenty of non-trivial paths in $R$, which it's safe to think of as maps $[0,1]\to R$? 3. If I consider the [[shape modality]] of $R$, $\int R$. Am I right that this is still an h-set, which is neither isomorphic to $R$ nor to a point? I concluded this from what David wrote: >As with the shape modality, identifying path connected points in a space, one retains the information of different identifications, and identifications between identifications, etc. So in particular, since I retain the information of _different_ identifications (or paths), there should be a way to distinguish between a constant path and a non-trivial path homotopic to it. This confuses me, since it seems to contradict univalence. On the other hand, if I think of paths and identites as different notions, and substitute path for identification in the above it seems to make sense. On the other hand Urs wrote: >think of $\Pi_{inf}X \coloneqq \Im(X)$ as the result of forming a new groupoid from the groupoid $X$ by adding in further isomorphisms between all objects (points of $X$) that are infinitesimal neighbours. These isomorphisms are hence infinitesimal paths. Here you say isomorphism are paths, which makes me think that paths are identities after all...

   Following this discussion, I take the opportunity to articulate some confusions I have, regarding the notions of path and identity in the context of cohesion. Contrary to the situation in “bare” homotopy type theory, it seems to me that “path” and “identity” no longer mean the same for cohesive types.

   It’s maybe easiest to ask some concrete questions (apologies if these are completely misguided):

   1. If I consider a manifold as a cohesive type, for concreteness the unit circle $S^1$. Is it right that there are no non-trivial identities between points of $S^1$? So $S^1$ is an h-set? If I had considered the real line $R$, the same applies and moreover $R\neq *$?

   2. Is it right that there are plenty of non-trivial paths in $R$, which it’s safe to think of as maps $[0,1]\to R$?

   3. If I consider the shape modality of $R$, $\int R$. Am I right that this is still an h-set, which is neither isomorphic to $R$ nor to a point?

   I concluded this from what David wrote:

   As with the shape modality, identifying path connected points in a space, one retains the information of different identifications, and identifications between identifications, etc.

   So in particular, since I retain the information of different identifications (or paths), there should be a way to distinguish between a constant path and a non-trivial path homotopic to it. This confuses me, since it seems to contradict univalence. On the other hand, if I think of paths and identites as different notions, and substitute path for identification in the above it seems to make sense.

   On the other hand Urs wrote:

   think of $\Pi_{inf}X \coloneqq \Im(X)$ as the result of forming a new groupoid from the groupoid $X$ by adding in further isomorphisms between all objects (points of $X$) that are infinitesimal neighbours. These isomorphisms are hence infinitesimal paths.

   Here you say isomorphism are paths, which makes me think that paths are identities after all…

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeMay 13th 2015
   • (edited May 13th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOne issue, beyond my control, is that it is a bad idea to speak in bare homotopy type theory of paths. This comes from thinking, by default, of bare homotopy types as being the shape of topological spaces, which is good for some purposes but is a conceptual trick that in the hands of the unwary may backfire. Also, there is long established terminology for the non-paths in bare homotopy types, namely they are the morphisms of an $\infty$-groupoid. And it being an $\infty$-groupoid, they are all (higher) isomorphisms. With that out of the way, here are the replies to your questions: 1. The circle regarded as $S^1 \in SmoothMfd \hookrightarrow Smooth \infty Grpd$ is a 0-truncated cohesive homotopy type, in that, indeed, it does not have any nontrivial morphisms inside it, it is an h-set, yes, for emphasis: a _cohesive h-set_. Same for $\mathbb{R}^1 \in SmoothMfd \hookrightarrow Smooth \infty Grpd$ and $\mathbb{R}^1 \neq \ast$ in $Smooth \infty Grpd$, yes. 2. Yes. 3. Not quite. So $\int S^1 \simeq B \mathbb{Z}$ in $Smooth \infty Grpd$, where on the right hand side we have the homotopy type of the circle , which is the one that all presently available HoTT literature means when it says "circle". So $\int S^1$ is a cohesive homotopy 1-type that happens to be a geometrically discrete homotopy 1-type. Notice that the _morphisms_ in $\int S^1$ are the _geometric paths_ in $S^1$. Generally $\int$ may be thought of as producing fundamental path $\infty$-groupoids. Generally, for $X \in SmoothMfd \hookrightarrow Smooth \infty Grpd$, then $\int X$ is the geometrically discrete homotopy type which is presented by the topological space underlying $X$. Let me know if this clears up the remainder of what you wrote.

   One issue, beyond my control, is that it is a bad idea to speak in bare homotopy type theory of paths. This comes from thinking, by default, of bare homotopy types as being the shape of topological spaces, which is good for some purposes but is a conceptual trick that in the hands of the unwary may backfire.

   Also, there is long established terminology for the non-paths in bare homotopy types, namely they are the morphisms of an $\infty$-groupoid. And it being an $\infty$-groupoid, they are all (higher) isomorphisms.

   With that out of the way, here are the replies to your questions:

   1. The circle regarded as $S^1 \in SmoothMfd \hookrightarrow Smooth \infty Grpd$ is a 0-truncated cohesive homotopy type, in that, indeed, it does not have any nontrivial morphisms inside it, it is an h-set, yes, for emphasis: a cohesive h-set.

      Same for $\mathbb{R}^1 \in SmoothMfd \hookrightarrow Smooth \infty Grpd$ and $\mathbb{R}^1 \neq \ast$ in $Smooth \infty Grpd$, yes.

   2. Yes.

   3. Not quite. So $\int S^1 \simeq B \mathbb{Z}$ in $Smooth \infty Grpd$, where on the right hand side we have the homotopy type of the circle , which is the one that all presently available HoTT literature means when it says “circle”. So $\int S^1$ is a cohesive homotopy 1-type that happens to be a geometrically discrete homotopy 1-type.

      Notice that the morphisms in $\int S^1$ are the geometric paths in $S^1$. Generally $\int$ may be thought of as producing fundamental path $\infty$-groupoids.

      Generally, for $X \in SmoothMfd \hookrightarrow Smooth \infty Grpd$, then $\int X$ is the geometrically discrete homotopy type which is presented by the topological space underlying $X$.

   Let me know if this clears up the remainder of what you wrote.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeMay 13th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRight. A general cohesive homotopy type may have both *paths* (in the topological sense) and *identifications*, and two points may be connected by a path but not identified. The shape modality *makes paths into new identifications* (but also keeps the old identifications around). It does, however, happen to be the case that the shape of the (Dedekind) *real numbers* is a point (and in particular an h-set), because the real numbers are *topologically* (cohesively) contractible, in the sense that any two points are connected by a path (a map $[0,1]\to \mathbb{R}$), any two paths (in this sense) are homotopic (by a map $[0,1]\times [0,1]\to \mathbb{R}$), etc., so we have $ʃ \mathbb{R} = \ast$. (Note that the shape modality ʃ is an [esh](http://en.wikipedia.org/wiki/Esh_%28letter%29), `ʃ`, not an integral sign.)

   Right. A general cohesive homotopy type may have both paths (in the topological sense) and identifications, and two points may be connected by a path but not identified. The shape modality makes paths into new identifications (but also keeps the old identifications around).

   It does, however, happen to be the case that the shape of the (Dedekind) real numbers is a point (and in particular an h-set), because the real numbers are topologically (cohesively) contractible, in the sense that any two points are connected by a path (a map $[0,1]\to \mathbb{R}$), any two paths (in this sense) are homotopic (by a map $[0,1]\times [0,1]\to \mathbb{R}$), etc., so we have $ʃ \mathbb{R} = \ast$.

   (Note that the shape modality ʃ is an esh, ʃ, not an integral sign.)

4. • CommentRowNumber4.
   • CommentAuthorMichael_Bachtold
   • CommentTimeMay 14th 2015
   • PermaLink
   Author: Michael_Bachtold
   Format: MarkdownItexThanks Urs and Mike, that clarifies some things!

   Thanks Urs and Mike, that clarifies some things!