Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: differential cohesive homotopy type theory

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 19th 2012
    • (edited Oct 19th 2012)

    While working at geometry of physics on the next chapter Differentiation I am naturally led back to think again about how to best expose/introduce infinitesimal cohesion. To the reader but also, eventually, to Coq.

    First the trivial bit, concerning terminology: I am now tending to want to call it differential cohesion, and differential cohesive homotopy type theory. What do you think?

    Secondly, I have come to think that the extra right adjoint in an infinitesimally cohesive neighbourhood need not be part of the axioms (although it happens to be there for Sh ∞(CartSp)↪Sh ∞(CartSp th)Sh_\infty(CartSp) \hookrightarrow Sh_\infty(CartSp_{th}) ).

    So I am now tending to say

    Definition. A differential structure on a cohesive topos is an ∞-connected and locally ∞-connected geometric embedding into another cohesive topos.

    And that’s it. This induces a homotopy cofiber sequence

    CohesiveType ↪ InfThickenedCohesiveType → InfinitesimalType ↘ ↓ ↙ DiscreteType \array{ CohesiveType &\hookrightarrow& InfThickenedCohesiveType &\to& InfinitesimalType \\ & \searrow & \downarrow & \swarrow \\ && DiscreteType }

    Certainly that alone is enough axioms to say in the model of smooth cohesion all of the following:

    So that seems to be plenty of justification for these axioms.

    We should, I think, decide which name is best (“differential cohesion”?, “infinitesimal cohesion”?) and then get serious about the “differential cohesive homotopy type theory” or “infinitesimal cohesive homotopy type theory” or maybe just “differential homotopy type theory” respectively.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 19th 2012

    So these axioms are at least a tad more general than what is strictly subsumed by “infinitesimal” theory, but in a good way:

    I think these axioms also capture “germ structure” and in fact can resolve the full hierarchy:

    • first order infintiesimals

    • second order infinitesimals

    • …

    • orbitrary order infinitesimals

    • germs

    To which corresponds the hierarchy

    • Lie algebra / Lie algebroid

    • …

    • formal group

    • local group

    So that’s good. All of this can be captured by a hierarchy of differential cohesion structures

    CohesiveType↪FirstOrderInfThickenedCohesiveTypehookrightorderSecondOrderInfThickenedCohesiveType↪⋯↪⋯↪FormallyThickenedCohesiveType↪LocallyThickenedCohesiveType CohesiveType \hookrightarrow FirstOrderInfThickenedCohesiveType \hookrightorder SecondOrderInfThickenedCohesiveType \hookrightarrow \cdots \hookrightarrow \cdots \hookrightarrow FormallyThickenedCohesiveType \hookrightarrow LocallyThickenedCohesiveType
    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeOct 19th 2012

    I haven’t thought at all about this thickening business; I need to spend some time looking at it. A priori, “differential cohesion” seems a reasonable name.

    I’m not quite sure that “∞-connected and locally ∞-connected” is what you want to say, though. When its codomain isn’t ∞Gpd\infty Gpd, having a left adjoint to the inverse image isn’t sufficient to make a geometric morphism locally connected. And if it isn’t locally connected, then being connected (i.e. the inverse image functor being fully faithful) isn’t equivalent to the left adjoint preserving the terminal object. And of course, an embedding can never be connected (in the usual sense) without being an equivalence.

  4. to parallel the naming of cohesive (infinity,1)-topos and cohesive homotopy type theory, we have differential cohesive (infinity,1)-topos and differential cohesive homotopy type theory.

    Anonymous

    diff, v5, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2022

    Okay. Yet later I had changed my mind to calling this elastic homotopy theory – have added the remark here.

    diff, v6, current

  6. this added text was from the HoTT wiki on differential cohesive homotopy type theory, I don’t know how accurate it is.

    Anonymous

    diff, v7, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2022

    Who is it who has been working on or thinking about this syntactic formulation of the theory? I wasn’t aware that anyone looked into this.

    • CommentRowNumber8.
    • CommentAuthorGuest
    • CommentTimeJun 18th 2022
    I have no idea, looking at the history of the corresponding page on the HoTT wiki it was some anonymous editor from the beginning of April 2022

    https://ncatlab.org/homotopytypetheory/history/differential+cohesive+homotopy+type+theory
    • CommentRowNumber9.
    • CommentAuthorGuest
    • CommentTimeJun 18th 2022

    Last revision before merger: https://ncatlab.org/homotopytypetheory/revision/differential+cohesive+homotopy+type+theory+%3E+history/2

    • CommentRowNumber10.
    • CommentAuthorGuest
    • CommentTimeJun 19th 2022

    This looks very incomplete, the given rules in the article seem to only be formation rules.

    • CommentRowNumber11.
    • CommentAuthormaxsnew
    • CommentTimeSep 17th 2022
    • (edited Sep 17th 2022)

    I don’t really know what to make of the type theory on the page currently, it looks like someone was sketching something out on the hott lab? It looks like someone just took the definition of an infinitesimal cohesive neighborhood of a topos from differential cohesive (infinity,1)-topos and turned all the toposes into kinds and all of the functors into type constructors acting uniformly on the context, which I am pretty sure doesn’t work at all: for instance in cohesive hott you need a distinction between crisp and non-crisp variables.

    Shall I delete what is written here?

    Also we now have a proposal for a fragment of this type theory which is David Jaz Myers’ synthetic differential cohesive hott, which extends cohesive hott with axioms of synthetic differential geometry, and so allows the shape and infinitesimal shape to be defined as localizations. There no reduction and inf flat modalities, though the inf flat could probably be added by introducing a notion of “infinitesimally crisp” variable.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2022

    Shall I delete what is written here?

    Sounds good to me. Thanks for looking into it.

    • CommentRowNumber13.
    • CommentAuthormaxsnew
    • CommentTimeSep 17th 2022

    Remove the HoTT stuff and add that this type theory hasn’t been defined yet, and cite some work in fragments of the theory.

    diff, v10, current

  14. fixing links

    Anonymous

    diff, v11, current

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJan 12th 2023

    I’ve been thinking about general modal type theories again, and wondering what the mode theory for elastic type theory would look like. Let’s leave out ʃʃ and ℜ\Re, since they aren’t left exact and thus don’t work so well judgmentally with current technology. In state-of-the-art general modal dependent type theories like MTT, the mode 2-category has to represent all the modalities (we don’t get right adjoints for free like in LSR). So we’ll have a 2-category generated by one object and four idempotent endomorphisms ℑ,&,♭,♯\Im,\&,\flat,\sharp, such that ♭,&\flat,\& are comonads and ♯,ℑ\sharp,\Im are monads, and ♭⊣♯\flat\dashv\sharp and ℑ⊣&\Im \dashv \&, plus ♭⇒&\flat \Rightarrow \&. This is sufficient to characterize many of the composites of these four morphisms, but there are some that aren’t clear to me.

    ↓∘→ ♭ ♯ ℑ & ♭ ♭ ♭ ♭ ♯ ♯ ♯ ℑ ♭ ℑ & & ♭ ℑ & \begin{array}{ccccc} \downarrow \circ \rightarrow & \flat & \sharp & \Im & \& \\ \flat & \flat & \flat & & \flat \\ \sharp & \sharp & \sharp & & \\ \Im & \flat & & \Im & \&\\ \& & \flat & & \Im & \& \\ \end{array}

    Can the gaps in this table all be filled using the four morphisms ℑ,&,♭,♯\Im,\&,\flat,\sharp? Or are some of those composites not identifiable with any of the four morphisms we already have? Can we explicitly describe the 2-category generated by these four morphisms and the laws they satisfy?

1 to 15 of 15

  1.