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.
   • CommentAuthorStephane_Bronoff
   • CommentTimeMay 1st 2015
   • (edited May 2nd 2015)
   • PermaLink
   Author: Stephane_Bronoff
   Format: MarkdownItexAlthough univalence appears as independent from any cohesion it is instructive to look if cohesion has something to do with univalence. Let’s look at the archetypal cohesive topos of reflexive directed graphs. Its cohesion comes solely from its reflexivity. When we model it through right $\Delta_1$-sets [Lawvere](http://ncatlab.org/nlab/files/LawvereCohesiveToposes.pdf), we see that it is precisely the $\Delta_1$ monic from “point” to “arrow” that allows to identify “point” to its image in “arrow”, and therefore differentiates reflexive directed graphs from directed graphs. And the topos of directed graphs is not a cohesive topos. Then we can lift those concepts to some infinity-topos and we know that infinity-topos internal logic can be described by homotopy type theory. The act of lifting (technique due to Lawvere) will suffer from a lack of information but surely right $\Delta_1$-sets topos contains more information about variation and cohesion of the infinity-topos than the topos of sets. Following this technique, the core of cohesion, which is the possibility to identify a point with its image in an arrow, is lifted to a canonical map $Id \rightarrow Eq$ for which univalence axiom states that this map is itself an equivalence. The logical notion of identity expands into the experiential notion of equivalence. This is exactly the role of the monic in $\Delta_1^{op}$ to expand the "points" into "arrows" in right $\Delta_1$-sets.

   Although univalence appears as independent from any cohesion it is instructive to look if cohesion has something to do with univalence.

   Let’s look at the archetypal cohesive topos of reflexive directed graphs. Its cohesion comes solely from its reflexivity. When we model it through right $\Delta_1$-sets Lawvere, we see that it is precisely the $\Delta_1$ monic from “point” to “arrow” that allows to identify “point” to its image in “arrow”, and therefore differentiates reflexive directed graphs from directed graphs. And the topos of directed graphs is not a cohesive topos.

   Then we can lift those concepts to some infinity-topos and we know that infinity-topos internal logic can be described by homotopy type theory. The act of lifting (technique due to Lawvere) will suffer from a lack of information but surely right $\Delta_1$-sets topos contains more information about variation and cohesion of the infinity-topos than the topos of sets.

   Following this technique, the core of cohesion, which is the possibility to identify a point with its image in an arrow, is lifted to a canonical map $Id \rightarrow Eq$ for which univalence axiom states that this map is itself an equivalence. The logical notion of identity expands into the experiential notion of equivalence. This is exactly the role of the monic in $\Delta_1^{op}$ to expand the “points” into “arrows” in right $\Delta_1$-sets.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeMay 1st 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexThis seems to be the result of rather loose associations. The symbol "Id" is used (in different context, even in different communities) both for identity morphisms as well as for identity types, but these two concepts are rather different. Accordingly, the discrete inclusion in cohesive situations such as that of simplicial objects is rather unlike the map to which the univalence axiom applies.

   This seems to be the result of rather loose associations.

   The symbol “Id” is used (in different context, even in different communities) both for identity morphisms as well as for identity types, but these two concepts are rather different. Accordingly, the discrete inclusion in cohesive situations such as that of simplicial objects is rather unlike the map to which the univalence axiom applies.

3. • CommentRowNumber3.
   • CommentAuthorStephane_Bronoff
   • CommentTimeMay 1st 2015
   • (edited May 1st 2015)
   • PermaLink
   Author: Stephane_Bronoff
   Format: MarkdownItexThe map to which the univalence axiom applies has identity types for domain. If you consider the full tower of idendity types with the structure of an $\infty$-groupoid, this map is rather unlike the discrete inclusion in traditional cohesive situations. But homotopy type theory provides a synthetic description of identity type, where points, paths, and paths between paths are primitive notions With those primitive notions, one can construct a new cohesive situation just by asking points to be self-paths. This is like asking the theory to be untyped single-sorted with only path between paths as primitive notion.

   The map to which the univalence axiom applies has identity types for domain. If you consider the full tower of idendity types with the structure of an $\infty$-groupoid, this map is rather unlike the discrete inclusion in traditional cohesive situations.

   But homotopy type theory provides a synthetic description of identity type, where points, paths, and paths between paths are primitive notions

   With those primitive notions, one can construct a new cohesive situation just by asking points to be self-paths. This is like asking the theory to be untyped single-sorted with only path between paths as primitive notion.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeMay 1st 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItex> by asking points to be self-paths. Sure, elements may be identified with the constant paths on them, the refl-elements of the identity types. Which only makes my point that it seems to me that you are conflating these constant paths, sometimes denoted "Id", with the full identity type, also denoted $Id$. But if you don't agree with my impression of your vague indication in #1, you have an easy way out: write down in precise detail what you really mean.

   by asking points to be self-paths.

   Sure, elements may be identified with the constant paths on them, the refl-elements of the identity types.

   Which only makes my point that it seems to me that you are conflating these constant paths, sometimes denoted “Id”, with the full identity type, also denoted $Id$.

   But if you don’t agree with my impression of your vague indication in #1, you have an easy way out: write down in precise detail what you really mean.

5. • CommentRowNumber5.
   • CommentAuthorStephane_Bronoff
   • CommentTimeMay 1st 2015
   • PermaLink
   Author: Stephane_Bronoff
   Format: MarkdownItexIn homotopy type theory, one can apply path constructors such as loop to generate a new inhabitant of an identity type, which is not a priori equal to any previously existing such inhabitant. One can interpret constructors as axioms, or in other words properties already appearing at the level of the induction principle are fundamental compare to those of the "full" identity type. proposition: "The type of such identity types, for which new inhabitant are generated by a loop as path constructor, is still an univalent universe, and gives the internal logic of an infinity-topos with its axioms of cohesion"

   In homotopy type theory, one can apply path constructors such as loop to generate a new inhabitant of an identity type, which is not a priori equal to any previously existing such inhabitant.

   One can interpret constructors as axioms, or in other words properties already appearing at the level of the induction principle are fundamental compare to those of the “full” identity type.

   proposition: “The type of such identity types, for which new inhabitant are generated by a loop as path constructor, is still an univalent universe, and gives the internal logic of an infinity-topos with its axioms of cohesion”

6. • CommentRowNumber6.
   • CommentAuthorStephane_Bronoff
   • CommentTimeMay 2nd 2015
   • (edited May 3rd 2015)
   • PermaLink
   Author: Stephane_Bronoff
   Format: MarkdownItex> Sure, elements may be identified with the constant paths on them, the refl-elements of the identity types. Please consider the case of a type family indexed by a loop. We cannot apply path induction and consider only the case where this loop is reflexivity. As a matter of fact, in homotopy type theory, we cannot prove that all loops are reflexivity. But your are right, although I understand clearly the difference, I am conflating the equivalence map $Id_U(A,B)\rightarrow Eq(A,B)$ in some univalent universe with the simplex monic [0] $\xrightarrow{id}$ [1] leading to cohesion within the topos of reflexive directed graphs. My intuition is that the two a priori unrelated notions of univalence and cohesion, might be both expressed in terms of the same topos-theoretic invariants (in the sense of properties of toposes written in the language of Topos Theory, see [Caramello](http://www.oliviacaramello.com/Files/Unification.pdf)). The interest of doing so is the following: You do not have to posite an infinity-topos $H$ and externally require cohesion axioms leading to the adjoint triple of modalities $\int\dashv\flat \dashv\sharp$, analogous to the structure introduced by William Lawvere for cohesive toposes ([Cohesive infinity-topos](http://nlab.mathforge.org/nlab/show/cohesive+%28infinity%2C1%29-topos)). These structures exist in homotopy type theory and one shall use path constructors as loop to construct/proove it. Of course, one would need to demonstrate that the collection of these inductively defined structures are actually describing the internal logic of an infinity-topos (see proposition in previous comment). But if this is the case, the infinity-topos will automatically get the cohesion axioms from the constructors. And this infinity-topos notion of cohesion would be due to the expansion of the logical notion of identity into the non-local notion of equivalence in the internal logic (univalence).

   Sure, elements may be identified with the constant paths on them, the refl-elements of the identity types.

   Please consider the case of a type family indexed by a loop. We cannot apply path induction and consider only the case where this loop is reflexivity. As a matter of fact, in homotopy type theory, we cannot prove that all loops are reflexivity.

   But your are right, although I understand clearly the difference, I am conflating the equivalence map $Id_U(A,B)\rightarrow Eq(A,B)$ in some univalent universe with the simplex monic [0] $\xrightarrow{id}$ [1] leading to cohesion within the topos of reflexive directed graphs.

   My intuition is that the two a priori unrelated notions of univalence and cohesion, might be both expressed in terms of the same topos-theoretic invariants (in the sense of properties of toposes written in the language of Topos Theory, see Caramello).

   The interest of doing so is the following: You do not have to posite an infinity-topos $H$ and externally require cohesion axioms leading to the adjoint triple of modalities $\int\dashv\flat \dashv\sharp$, analogous to the structure introduced by William Lawvere for cohesive toposes (Cohesive infinity-topos). These structures exist in homotopy type theory and one shall use path constructors as loop to construct/proove it.

   Of course, one would need to demonstrate that the collection of these inductively defined structures are actually describing the internal logic of an infinity-topos (see proposition in previous comment). But if this is the case, the infinity-topos will automatically get the cohesion axioms from the constructors. And this infinity-topos notion of cohesion would be due to the expansion of the logical notion of identity into the non-local notion of equivalence in the internal logic (univalence).