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.
   • CommentAuthorUrs
   • CommentTimeJun 1st 2012
   • (edited Jun 1st 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexFinally I have a spare second to recover (my lecture now over). The following thought crossed my mind: it would be nice to have applications of the [[homotopy type theory|HoTT]] constructions [[isContr]], [[isProp]], and generally [[isnTrunc]] in homotopy theory (i.e. independent from the point of view of formal logic). Similarly for [[isnConn]]. First of all, I assume it is true that $$ \sum_{A : Type} isnTrunc(A) : Type $$ is the classifier for $n$-truncated objects/morphisms. (right?) Similarly $$ \sum_{A : Type} isnConn(A) : Type $$ should be the classifier of $n$-connected objects/morphisms. This is something that people have considered independently of logic: if I am right here then $$ \infty Gerbe \coloneqq \sum_{A : Type} is0Conn(A) : Type $$ is the classifier for [[infinity-gerbes]]. :-) And if that's right then $$ Ab n Gerbe \coloneqq \sum_{A : Type} (isnTrunc(A) and isnConn(A)) $$ is the classifier for abelian $n$-gerbes.

   Finally I have a spare second to recover (my lecture now over).

   The following thought crossed my mind:

   it would be nice to have applications of the HoTT constructions isContr, isProp, and generally isnTrunc in homotopy theory (i.e. independent from the point of view of formal logic). Similarly for isnConn.

   First of all, I assume it is true that

   $$\sum_{A : Type} isnTrunc(A) : Type$$

   is the classifier for $n$-truncated objects/morphisms. (right?)

   Similarly

   $$\sum_{A : Type} isnConn(A) : Type$$

   should be the classifier of $n$-connected objects/morphisms.

   This is something that people have considered independently of logic: if I am right here then

   $$\infty Gerbe \coloneqq \sum_{A : Type} is0Conn(A) : Type$$

   is the classifier for infinity-gerbes. :-)

   And if that’s right then

   $$Ab n Gerbe \coloneqq \sum_{A : Type} (isnTrunc(A) and isnConn(A))$$

   is the classifier for abelian $n$-gerbes.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJun 1st 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, that all seems right to me, except that I wonder whether you want to combine $n$-connectedness with $(n+1)$-truncatedness? (And is it still called "abelian" if $n=0,1$?) Has a definition of "isnConn" been written down in HoTT? It seems like it should require HITs ("the $n$-truncation is contractible").

   Yes, that all seems right to me, except that I wonder whether you want to combine $n$-connectedness with $(n+1)$-truncatedness? (And is it still called “abelian” if $n=0,1$?)

   Has a definition of “isnConn” been written down in HoTT? It seems like it should require HITs (“the $n$-truncation is contractible”).

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJun 2nd 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexRight, that one index was off by one. And $n \geq 2$ for the abelian case, sure. > Has a definition of "isnConn" been written down in HoTT? Ah, so it hasn't? I seemed to remember that you had written it down somewhere?

   Right, that one index was off by one. And $n \geq 2$ for the abelian case, sure.

   Has a definition of “isnConn” been written down in HoTT?

   Ah, so it hasn’t? I seemed to remember that you had written it down somewhere?

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJun 2nd 2012
   • (edited Jun 2nd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexProbably when one thinks about it more, one finds many more useful examples. For instance I am playing with the thought of: a moduli $\infty$-stack classifying not just "Freed-Witten anomaly free fields" on a fixed spacetime with a _fixed_ D-brane included, but classifying also all possible D-brane inclusions: in terms of monomorphsims, hence invoking $isProp(-)$. Such a construction is certainly beginning to sound like something that may be genuinely useful outside of formal logic and somewhat non-trivial to write down (as a rectified moduli $\infty$-stack, hence as a simplicial presheaf) without invoking the HoTT compiler.

   Probably when one thinks about it more, one finds many more useful examples. For instance I am playing with the thought of: a moduli $\infty$-stack classifying not just “Freed-Witten anomaly free fields” on a fixed spacetime with a fixed D-brane included, but classifying also all possible D-brane inclusions: in terms of monomorphsims, hence invoking $isProp(-)$. Such a construction is certainly beginning to sound like something that may be genuinely useful outside of formal logic and somewhat non-trivial to write down (as a rectified moduli $\infty$-stack, hence as a simplicial presheaf) without invoking the HoTT compiler.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeJun 4th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexMight there be a way to have classifiers for _absolutely compact sub-types_? By this I mean $(-1)$-truncated $Q \hookrightarrow X$ where $Q$ is not just $X$-relatively compact (as every $X$-dependent type) but also absolutely compact (in the termial context).

   Might there be a way to have classifiers for absolutely compact sub-types?

   By this I mean $(-1)$-truncated $Q \hookrightarrow X$ where $Q$ is not just $X$-relatively compact (as every $X$-dependent type) but also absolutely compact (in the termial context).

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJun 4th 2012
   • (edited Jun 4th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm, actually that question shows that I am confused about something. I need to come back to this. But have to run now... What I am thinking about is whether there is a nice way to say _compactly supported cohomology_ in homotopy type theory.

   Hm, actually that question shows that I am confused about something. I need to come back to this. But have to run now…

   What I am thinking about is whether there is a nice way to say compactly supported cohomology in homotopy type theory.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJun 5th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAbsolutely compact sub-types aren't stable under pullback, are they?

   Absolutely compact sub-types aren’t stable under pullback, are they?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeJun 5th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAnd I guess we do have a definition of isnConn: if we take localization at $S^{n+1}$ to define $n$-truncatedness, then in the resulting stable factorization system, the left class is the class of $n$-connected morphisms; so we can define a type to be $n$-connected if $A\to 1$ is in that left class.

   And I guess we do have a definition of isnConn: if we take localization at $S^{n+1}$ to define $n$-truncatedness, then in the resulting stable factorization system, the left class is the class of $n$-connected morphisms; so we can define a type to be $n$-connected if $A\to 1$ is in that left class.