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.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 9th 2012
   • (edited Sep 9th 2012)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexSo a while back I said that I'd like to make more of an effort to understand things like cohesive homotopy type theory, but I haven't said anything since then. Urs and Mike have been collaborating on this, and I hope they can explain some things to me. I'm probably going to be slowed down by trying to grapple with the syntax (and even more with Coq code), so I was hoping to understand things first at the semantic level, in the language of $(\infty, 1)$-toposes and so on. I'm looking at the page [[cohesive homotopy type theory]], to begin with. (Urs had recommended that I read his paper with Mike, but I'm already quickly confused by things like $Type$, so I think maybe I need to back up even more.) I should also mention that I had complained to Urs in email about statements on [[cohesive homotopy type theory]] such as, "The ambient homotopy type theory has a left-exact reflective sub-$(infty,1)$-category" which sounds to me like there's some mixing together of syntax ("ambient homotopy type theory") with semantics ("left-exact reflective sub-$(\infty, 1)$-category") taking place. I would have expected a different presentation which keeps the syntax-semantics distinction straight, perhaps something like: "Let $H$ be an $(\infty, 1)$-topos. A _cohesive structure_ on $H$ consists of two $(\infty, 1)$-monads $\sharp: H \to H$, $\Pi: H \to H$ and an $(\infty, 1)$-comonad $\flat: H \to H$ such that..." Even if this sentence is not quite technically correct (maybe there are some extra axioms on the $(\infty, 1)$-topos or something like that), that's the kind of _style_ that would come as a great relief to me. Is it possible to lay things out in that style? (Then we could have companion axioms written out in the syntax, which as I say contains elements which are currently a mystery to me.) I'm going to have a bunch of questions, but let's maybe start there, if we could, please. <b>Edit:</b> Why did I stop there? Can we summarize it like this (I'm going to skip the $(\infty, 1)$-prefixes): A _cohesive structure_ consists of an idempotent monad $\Pi: H \to H$ which preserves products, with a right adjoint $\flat: H \to H$ (which automatically acquires an idempotent comonad structure, say with counit $\varepsilon: \flat \to 1_H$ and comultiplication $\delta: \flat \to \flat \flat$), that in turn has a right adjoint $\sharp: H \to H$ possessing an idempotent monad structure (with unit $\eta: 1_H \to \sharp$ and multiplication $\mu: \sharp \sharp \to \sharp$), such that the composites $$\flat \stackrel{\delta}{\to} \flat \flat \stackrel{\flat (\eta \circ \varepsilon)}{\to} \flat \sharp; \qquad \sharp \flat \stackrel{\sharp (\eta \circ \varepsilon)}{\to} \sharp \sharp \stackrel{\mu}{\to} \sharp$$ are equivalences. Maybe some of that is redundant, but does that more or less cover it?

   So a while back I said that I’d like to make more of an effort to understand things like cohesive homotopy type theory, but I haven’t said anything since then. Urs and Mike have been collaborating on this, and I hope they can explain some things to me.

   I’m probably going to be slowed down by trying to grapple with the syntax (and even more with Coq code), so I was hoping to understand things first at the semantic level, in the language of $(\infty, 1)$-toposes and so on. I’m looking at the page cohesive homotopy type theory, to begin with. (Urs had recommended that I read his paper with Mike, but I’m already quickly confused by things like $Type$, so I think maybe I need to back up even more.)

   I should also mention that I had complained to Urs in email about statements on cohesive homotopy type theory such as, “The ambient homotopy type theory has a left-exact reflective sub-$(infty,1)$-category” which sounds to me like there’s some mixing together of syntax (“ambient homotopy type theory”) with semantics (“left-exact reflective sub-$(\infty, 1)$-category”) taking place. I would have expected a different presentation which keeps the syntax-semantics distinction straight, perhaps something like:

   “Let $H$ be an $(\infty, 1)$-topos. A cohesive structure on $H$ consists of two $(\infty, 1)$-monads $\sharp: H \to H$, $\Pi: H \to H$ and an $(\infty, 1)$-comonad $\flat: H \to H$ such that…”

   Even if this sentence is not quite technically correct (maybe there are some extra axioms on the $(\infty, 1)$-topos or something like that), that’s the kind of style that would come as a great relief to me. Is it possible to lay things out in that style? (Then we could have companion axioms written out in the syntax, which as I say contains elements which are currently a mystery to me.)

   I’m going to have a bunch of questions, but let’s maybe start there, if we could, please.

   Edit: Why did I stop there? Can we summarize it like this (I’m going to skip the $(\infty, 1)$-prefixes):

   A cohesive structure consists of an idempotent monad $\Pi: H \to H$ which preserves products, with a right adjoint $\flat: H \to H$ (which automatically acquires an idempotent comonad structure, say with counit $\varepsilon: \flat \to 1_H$ and comultiplication $\delta: \flat \to \flat \flat$), that in turn has a right adjoint $\sharp: H \to H$ possessing an idempotent monad structure (with unit $\eta: 1_H \to \sharp$ and multiplication $\mu: \sharp \sharp \to \sharp$), such that the composites

   $$\flat \stackrel{\delta}{\to} \flat \flat \stackrel{\flat (\eta \circ \varepsilon)}{\to} \flat \sharp; \qquad \sharp \flat \stackrel{\sharp (\eta \circ \varepsilon)}{\to} \sharp \sharp \stackrel{\mu}{\to} \sharp$$

   are equivalences. Maybe some of that is redundant, but does that more or less cover it?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexHave you looked at section 2.3 in our paper? There's no type theory there, only the toposes. (Sorry to be brief, I'd like to write more but don't have time right now.) I do agree with you about mixing syntax and semantics. That's the sort of thing that isn't really a problem any more once you know what you're talking about, but as exposition it is confusing.

   Have you looked at section 2.3 in our paper? There’s no type theory there, only the toposes. (Sorry to be brief, I’d like to write more but don’t have time right now.)

   I do agree with you about mixing syntax and semantics. That’s the sort of thing that isn’t really a problem any more once you know what you’re talking about, but as exposition it is confusing.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItex> Have you looked at section 2.3 in our paper? Yes, thanks, I had (and I used it to write my first comment; I should have acknowledged that). Yes, that section was helpful, and should probably be incorporated into the nLab article (I mean on the main lab, not Urs's web) at some point. But I want to understand some things better first before going in there myself.

   Have you looked at section 2.3 in our paper?

   Yes, thanks, I had (and I used it to write my first comment; I should have acknowledged that). Yes, that section was helpful, and should probably be incorporated into the nLab article (I mean on the main lab, not Urs’s web) at some point. But I want to understand some things better first before going in there myself.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexAs I said in reply by email: I entirely agree that the exposition at _[[cohsive homotopoy type theory]]_ deserves to be improved as you indicate. This entry is not meant to be in perfect state, that's why it is labeled as "under construction"... so I'd enjoy seeing it being constructed further! :-) First, I guess there should be no mystery as to what it _should_ eventually say in the entry. The definition of cohesion at _[[cohesive (infinity,1)-topos]]_ should be crystal clear, I suppose. A topos (I'll drop the "$\infty$", too), which is local, connected and locally connected, such that the extra left adjoint also preserves products. That's it. Now at _[[cohesive homotopy type theory]]_ there should ideally eventually be two steps of discussion: 1. reformulate "local and locally connected and local and $\Pi$ preserves products" entirely in terms of monads on the topos, 1. formulate these monads in homotopy type theory (the subtle point being, the one that Mike figured out: we first formulate the $\sharp$-monad naively as a monad on $Type$, and then the rest as monads on $\sharp Type$ ). (By the way, us formulating things in terms of monads $Type \to Type$ is just the same kind of idea as underlies a [[Lawvere-TIerney topology]]. Only that the $\Omega$ there (the $(-1)$-truncated object classifier) is now called $Type$ (the object classifier). So, Todd, if you have time and energy to put the description of cohesion in terms of monads the way you like it best into the entry, I would be delighted. As I said, I will not work on the entry currently, but will be back to doing so 6 weeks from now.

   As I said in reply by email: I entirely agree that the exposition at cohsive homotopoy type theory deserves to be improved as you indicate. This entry is not meant to be in perfect state, that’s why it is labeled as “under construction”… so I’d enjoy seeing it being constructed further! :-)

   First, I guess there should be no mystery as to what it should eventually say in the entry. The definition of cohesion at cohesive (infinity,1)-topos should be crystal clear, I suppose. A topos (I’ll drop the “$\infty$”, too), which is local, connected and locally connected, such that the extra left adjoint also preserves products. That’s it.

   Now at cohesive homotopy type theory there should ideally eventually be two steps of discussion:

   1. reformulate “local and locally connected and local and $\Pi$ preserves products” entirely in terms of monads on the topos,

   2. formulate these monads in homotopy type theory (the subtle point being, the one that Mike figured out: we first formulate the $\sharp$-monad naively as a monad on $Type$, and then the rest as monads on $\sharp Type$ ).

   (By the way, us formulating things in terms of monads $Type \to Type$ is just the same kind of idea as underlies a Lawvere-TIerney topology. Only that the $\Omega$ there (the $(-1)$-truncated object classifier) is now called $Type$ (the object classifier).

   So, Todd, if you have time and energy to put the description of cohesion in terms of monads the way you like it best into the entry, I would be delighted. As I said, I will not work on the entry currently, but will be back to doing so 6 weeks from now.

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexUrs, thanks for these excellent hints. They are extremely helpful. Is there just one object classifier $Type$, or are there many $Type_\kappa$ (and we use a uniform definition to handle them all at once)?

   Urs, thanks for these excellent hints. They are extremely helpful.

   Is there just one object classifier $Type$, or are there many $Type_\kappa$ (and we use a uniform definition to handle them all at once)?

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeSep 9th 2012
   • (edited Sep 9th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHi Todd, yes, so in an $\infty$-topos there is for each regular cardinal $\kappa$ an [[object classifier]] $Type_\kappa$, which is such that it classifies $\kappa$-compact objects, hence such that maps $X \to Type_\kappa$ are equivalent to maps $P \to X$ all whose homotopy fibers are $\kappa$-compact. In the type theory syntax these cardinals $\kappa$ are implicit. Or rather, in the syntax there is a tower of types $Type, Type_1, \cdots$, such that their categorical interpretation in an $\infty$-topos is given by some choice of tower of regular cardinals. Mike gives an account of this around [p. 9](http://arxiv.org/pdf/1203.3253v1.pdf) of his [arXiv:1203.3253](http://arxiv.org/abs/1203.3253). In other words, we don't really need to specify a $\kappa$. All we really need is one universe $Type$ to start with and a means to enlarge it. when necessary.

   Hi Todd,

   yes, so in an $\infty$-topos there is for each regular cardinal $\kappa$ an object classifier $Type_\kappa$, which is such that it classifies $\kappa$-compact objects, hence such that maps $X \to Type_\kappa$ are equivalent to maps $P \to X$ all whose homotopy fibers are $\kappa$-compact.

   In the type theory syntax these cardinals $\kappa$ are implicit. Or rather, in the syntax there is a tower of types $Type, Type_1, \cdots$, such that their categorical interpretation in an $\infty$-topos is given by some choice of tower of regular cardinals.

   Mike gives an account of this around p. 9 of his arXiv:1203.3253.

   In other words, we don’t really need to specify a $\kappa$. All we really need is one universe $Type$ to start with and a means to enlarge it. when necessary.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 10th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWould step 1 in #4 more properly be part of [[cohesive (infinity,1)-topos]]? Seeing as it has nothing to do really with the type theory yet?

   Would step 1 in #4 more properly be part of cohesive (infinity,1)-topos? Seeing as it has nothing to do really with the type theory yet?

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeSep 10th 2012
   • (edited Sep 10th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexSure, we could also expand there. There is already a section, actually _[cohesive infinity-topos --- Internally](http://ncatlab.org/nlab/show/cohesive%20%28infinity,1%29-topos#InternalDefinition)_ Todd did however express the feeling that the entry _[[cohesive homotopy type theory]]_ should be more self-contained, to be better readable. So I think his idea was actually to move material the other way. But I am fine whichever way. I am glad Todd is looking at this from a third-party perspective now. That always helps to see expositional aspects which those involved can no longer see.

   Sure, we could also expand there. There is already a section, actually

   cohesive infinity-topos — Internally

   Todd did however express the feeling that the entry cohesive homotopy type theory should be more self-contained, to be better readable. So I think his idea was actually to move material the other way. But I am fine whichever way. I am glad Todd is looking at this from a third-party perspective now. That always helps to see expositional aspects which those involved can no longer see.