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: AT category

Bottom of Page

1 to 42 of 42

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2013
    • (edited Dec 6th 2013)

    slightly edited AT category to make the definition/lemma/proposition-numbering and cross-referencing to them come out.

    Probably Todd should have a look over it to see if he agrees.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 6th 2013

    Any new thoughts on your question of whether there’s some relation to the Goodwillie calculus?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2013
    • (edited Dec 6th 2013)

    Indeed, it was some thinking in this direction that made me come back to the entry of AT-categories. But I am not sure yet.

    I need an axiomatic way to characterize an ambient ∞\infty-topos such that to each object XX is associated a closed symmetric monoidal ∞\infty-category EMod(X)E Mod(X) and to suitable morphisms f:X→Yf : X \to Y a Wirthmüller context (f !⊣f *⊣f *):EMod(X)→EMod(Y)(f_! \dashv f^\ast \dashv f_\ast) : E Mod(X) \to E Mod(Y).

    In tangent cohesion we have something close: here it is immediate to say GL 1(E)Mod(X)GL_1(E) Mod(X) and so forth. I have to see how much that helps me.

    Specifically I am interested in E ∞E_\infty-rings EE that are obtained from free E ∞E_\infty-rings on an abelian ∞\infty-group (connective spectrum) after inverting some elements. For these I might actually get away with GL 1(E)ModGL_1(E) Mod. Not sure yet.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 7th 2013

    Is there any way to get at a (∞,1)(\infinity, 1)-version of Freyd’s AT result? Are stable (infinity,1)-categories the right analogue of abelian categories? Would there need to be a notion of (∞,1)(\infinity, 1)-pretoposes?

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 7th 2013
    • (edited Dec 7th 2013)

    Urs #1: not only do I agree, but I thank you. I’ve taken advantage of your improved structuring by rewriting some of the proofs so that they link back in logical fashion.

    There’s something I find a little ungainly though in Freyd’s development; intriguing though the result is, the axioms look pretty ad hoc, and that probably explains why there hasn’t been much work on them. Perhaps this should be revisited.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2013
    • (edited Dec 7th 2013)

    I think David has a good point, in that in the context of ∞\infty-category theory the role of abelian categories is played by stable ∞\infty-categories, and these already share some key abstract properties with ∞\infty-toposes.

    The most striking one is probably the “stable Giraud theorem” which says that presentable stable ∞\infty-categories are precisely the lex reflective acessible localizations of categories of presheaves of spectra, just like sheaf ∞\infty-toposes are precisely the lex reflective accessible localizations of the categories of presheaves of homotopy types.

    As a slogan this means: stable ∞\infty-categories are to ∞\infty-toposes as stable homotopy types are to homotopy types.

    Now for a given ∞\infty-site of definition, the tangent (infinity,1)-category of the ∞\infty-topos over that site, unifies both of these: it has both the ∞\infty-topos as well as the stable ∞\infty-category over that site as full sub-∞\infty-categories.

    At this point one seems to be pretty close to what Freyd was after, maybe one should play with this a bit more.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 4th 2017

    Since at AT category there’s a topos version of the idea TA category after the main pretopos version, does Mike’s new definition of elementary (infinity,1)-topos suggest anything for my question in #4?

    Another thought, should there be a concept of (∞,1)(\infty, 1)-pretopos?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeApr 29th 2019

    Suppose 𝒜\mathcal{A} is an abelian category, 𝒯\mathcal{T} is a pretopos, and G:𝒜→𝒯G:\mathcal{A} \to \mathcal{T} is a left exact functor (such as the forgetful functor Ab→SetAb\to Set). Then unless I am mistaken, then Artin gluing (𝒯↓G)(\mathcal{T} \downarrow G) is a “weak AT category”, i.e. it satisfies Freyd’s universal Horn axioms but not the existential AE axiom. So that axiom is actually doing something to cut down the class of models, and there are interesting models of the rest of the axioms that aren’t products. I wouldn’t be surprised if there are other axioms we can impose to characterize such gluings among the AT categories, similarly to how every quasitopos is the Artin gluing of a Heyting algebra with an extensive quasitopos (A2.6.7 in the Elephant).

    This also suggests to me that AT categories are not doing quite the same thing as tangent ∞\infty-categories: both of them are a way to put together an abelian thing with a topos thing, but the ways of putting them together are different. I wonder what elementary axioms are satisfied by categories like Fam(Ab)Fam(Ab), the obvious 1-categorical analogue of parametrized spectra?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeApr 29th 2019

    Actually, here is one additional axiom on a weak AT category that suffices to enable reconstruction of the functor GG from (𝒯↓G)(\mathcal{T}\downarrow G): the object 00 is exponentiable (in the cartesian sense). This is true in a topos, of course, but also in any pretopos since A 0=1A^0=1, and also in any abelian category where A 0=AA^0=A. And in (𝒯↓G)(\mathcal{T}\downarrow G), for A=(A 0,A 1,A 1→G(A 0))A = (A_0, A_1, A_1 \to G(A_0)) we have A 0=(A 0,G(A 0),id G(A 0))A^0 = (A_0, G(A_0), id_{G(A_0)}). So for a type A object AA, which is of the form (A 0,0,0→G(A 0))(A_0, 0, 0\to G(A_0)), we have T(A 0)T(A^0) being the type T object corresponding to G(A 0)G(A_0), namely (1,G(A 0),!)(1, G(A_0), !).

    In (𝒯↓G)(\mathcal{T}\downarrow G), the operation A↦A 0A\mapsto A^0 is a right adjoint modality to A↦A×0A\mapsto A\times 0, giving two different ways to embed 𝒜\mathcal{A} into the gluing category. In general, once this is true, if we define G(A)=T(A 0)G(A) = T(A^0), then the map A 0→T(A 0)A^0 \to T(A^0) induces a functor from 𝒞\mathcal{C} to the gluing category of this GG (as a functor from the abelian category of type A objects to the pretopos of type T objects), and so there should be axioms ensuring that this functor is an equivalence.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJul 11th 2023

    made a proper bibitem for

    so that it can be cited, here and elsewhere

    diff, v26, current

    • CommentRowNumber11.
    • CommentAuthornonemenon
    • CommentTimeAug 23rd 2023

    Any updates on this? Mike directed me here five years ago from MO (thank you for that!); I am still wondering, of what ∞-stuff are AT categories “1-truncated shadows”? Does it relate to Goodwillie calculus, tangent cohesion and higher differential geometry?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeAug 23rd 2023

    I think AT-categories are a red herring. The structure of interest, unifying spaces with motives, are tangent ∞\infty-toposes, i.e. ∞\infty-Grothendieck constructions on Joyal loci – the categorical semantics of linear homotopy type theory.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 24th 2023

    You were pointing in that direction about 10 years ago (#6).

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2023

    Incidentally, I will be speaking about this topic in a few hours from now, at the Colloquium of the Topos Institute

    A first rough draft of the corresponding article is now here. Comments are welcome

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 24th 2023

    Exciting.

    Ah, OK, this is something I’ve been fishing for here for a while:

    Our thesis is that the conceptual foundation not just of quantum computing but in fact of fundamental quantum physics generally is in linear homotopy theory

    so then to what extent do we see the full computational structure of LHoTT in fundamental quantum physics? I mean presumably in experimental situations it’s just a question of picking up cross-sections, etc., whereas in quantum computing

    Even the most elementary quantum information protocols involve mid-circuit measurement and classical control.

    So then could there be any place in general quantum physics for mid-circuit measurement and classical control? Could you let them know at CERN that there’s a further way to experiment with composite processes, or will HEP only experiment on/detect one step?

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2023

    to what extent do we see the full computational structure of LHoTT in fundamental quantum physics?

    It’s everything

    could there be any place in general quantum physics for mid-circuit measurement and classical control?

    Sure, because what is a “quantum information protocol” to those who want to use the quantum effect (say for doing business) is just a “Bell experiment” or similar to those who are still investigating the effect.

    We had a line in the draft (did it get lost in the latest version?) of the form:

    The verified programming of a quantum algorithm is the act of accurately recounting, in formalized language, the physical quantum process that executes it, and conversely.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2023

    By the way, the

    thesis that the conceptual foundation not just of quantum computing but in fact of fundamental quantum physics generally is in linear homotopy theory.

    was originally presented at:

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 24th 2023

    Ok. Thanks, I’ll think about that. I didn’t notice that lightcone quantization section before.

    On another point

    In this case and assuming WW is finite (as it is for any realistic quantum measurement)…

    will there ever be a need for more general WW? Is it that, say, a position operator can only give an eigenvalue to a specified degree of accuracy?

    Would there ever be a need to form the linear version of relative modal operators, for a f:W→Vf: W \to V, representing classically an ’accessibility’ relation on possible worlds?

    How about some smooth structure on the WW and the jet comonad construction as ’relative necessity’ along

    i:X⟶ℑX. i \colon X \longrightarrow \Im X.

    What might a linear version of this entail? Maybe we’ll see this later in some Linear differential cohesive HoTT:

    While such modal type theory is going to be relevant for various enhancements of the computational context presented here (to be discussed elsewhere)

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2023

    will there ever be a need for more general W?

    Of course, for instance in Quantization via Linear homotopy types the base types represent general (stacky) phase spaces.

    But for WW to be a type of “measurement results” as understood in quantum information theory, it better be finite — in the literal sense of “better”: It need not strictly be, but if it isn’t then its interpretation as measurement outcomes may at times become murky.

    (For what it’s worth, this matches well with the idea that measurement should be something practically doable. All real measurements have a finite set of outcomes.)

    Would there ever be a need to form the linear version of relative modal operators

    You may be after something different, but let me mention that “quantization”

    Q:ClaTypes→QuTypes↪Types \mathrm{Q} \;\colon\; ClaTypes \to QuTypes \hookrightarrow Types

    is a relative modal operator in a remarkably (I find) satisfactory way: as explained on what is currently p. 35 of the draft here.

    • CommentRowNumber20.
    • CommentAuthorperezl.alonso
    • CommentTimeAug 24th 2023
    • (edited Aug 24th 2023)

    Thanks for the talk, Urs. How does Definition 3.10 interact with taking slices in ClaTypes? Obviously, what I have in mind is taking ClaTypes=H=smooth stacks\text{ClaTypes}=H=\text{smooth stacks} and considering the slice oo-topos H/X for X=B nU(1) connX=B^n U(1)_{conn}. Just taking H/XH/X to mean ClaType would give modules indexed by a gerbe, which isn’t precisely what we want. For example for n=1, do we want to consider something like PreQuTypes using U(1)U(1)-modules that then embed appropriately into ℂ\mathbb{C}-modules?

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeAug 24th 2023
    • (edited Aug 24th 2023)

    Maybe not quite the answer to your question, but let me highlight the following:

    For G:Grp(ClaTypes)G \,\colon\, Grp(ClaTypes) a group, the classical slice over its delooping is equivalently (eg. p. 14 here) the GG-actions (non-linear, as in G-sets):

    ClaTypes /BG≃GAct(ClaTypes). ClaTypes_{/\mathbf{B}G} \;\simeq\; G Act\big(ClaTypes\big) \,.

    But now (where, compared to the talk, here I write LinTypes≡QuTypesLinTypes \equiv QuTypes) we have that

    LinTypes BG≃GAct(LinTypes) LinTypes_{\mathbf{B}G} \;\simeq\; G Act\big(LinTypes\big)

    is the linear GG-actions, hence the actual GG-representations.

    (This needs to be written up in a nice way, but the idea of how this straightforwardly follows from the previous statement is on p. 7 here and then again p. 18).

    Here we can take Type≔THType \,\coloneqq\, T\mathbf{H} in which case ClaTypes=HClaTypes = \mathbf{H} and LinTypes=Spectra(H)LinTypes = Spectra(\mathbf{H}) and hence get (“naive”) GG-equivariant spectra in H\mathbf{H}.

    For something closer to the ℝ\mathbb{R}eal world, we consider H=SmthGrpd ∞\mathbf{H} = SmthGrpd_\infty and for ℝ∈Set↪Grpd ∞↪SmthGrpd ∞\mathbb{R} \in Set \hookrightarrow Grpd_\infty \hookrightarrow SmthGrpd_\infty we let

    Type≔T HℝSmthGrpd ∞≔∫ X∈SmthGrpd ∞HℝMod(SmthGrpd ∞) X Type \coloneqq T^{H \mathbb{R}} SmthGrpd_\infty \;\coloneqq\; \int_{ \mathbf{X} \in SmthGrpd_\infty } H\mathbb{R}Mod(SmthGrpd_\infty)_{\mathbf{X}}

    be the parameterized HℝH\mathbb{R}-module spectra. At least if we forget the smooth structure here and maybe replace ℝ\mathbb{R} by ℂ\mathbb{C} to stick with convention, then this is equivalently infinity-local systems (cf. pp. 23)

    T HℂGrpd ∞≃Loc ℂ T^{H \mathbb{C}} Grpd_\infty \;\simeq\; Loc_\mathbb{C}

    and the above “linear GG-representations” now are what some people call “representations up to homotopy” (eg. arXiv:0911.2859) but which, of course, really are higher homotopy-coherent linear representations on chain complexes.

    Now I am aware that I am probably not answering your actual question. :-) Maybe say again what exactly you’d like to see.

    • CommentRowNumber22.
    • CommentAuthorperezl.alonso
    • CommentTimeAug 24th 2023

    I mean to ask how the linearization step in motivic quantization follows from working with the slice topos H/Phases and the quantization relative modal operator you mentioned above. Probably there isn’t much to say about this, though.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023

    Yes, maybe just to amplify that there is no change in perspective since the discussion of motivic quantization: It’s the same toposes of parameterized module spectra that we were and are talking about.

    The discussion of “motivic quantization” is concerned specifically the formalization of pull-push transformations in this context, observing that the “Umkehr maps” in twisted cohomology theory have a neat linear-type-theoretic abstract formulation – this is the central Def. 4.18 on p. 53 with its Exp. 6.2 on p. 65 in “Quantization via LHoTT”.

    One difference is that back then LHoTT did not actually exist yet as a type theory, while now it does.

    So in the present discussion, we are looking at quantum via LHoTT afresh – paying more attention to various (co)modalities one may extract from it and their role in a more comprehensive formal quantum language – but it’s not a change of premise: All the previous discussion of motivic quantiztion – including those of linearization of higher groups of phases – carry over.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 25th 2023

    Typos:

    theory of kowledge; effecy

    In (30) rather than R×(−)R \times (-) presumably it’s [R,(−)][R, (-)], and in (31) there shouldn’t be any WWs.

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 25th 2023

    In (33) you have AA rather than WW.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023

    Thanks. There is more symbol clash in (33), seems that different authors had different ideas for which symbol to use. Am fixing it now…

    • CommentRowNumber27.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 25th 2023
    • (edited Aug 25th 2023)

    Re the set-up in Prop 3.8, is there anything of interest in the connection I was trying to make between the exponential comonad and (an adjusted) store comonad, on Twitter here.

    Perhaps we might think of coalgebras for the former in a lens-like way?

    I think I was getting somewhere with that thread from here.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023

    Maybe better to mention references and their potential relations not just in discussion fora, but to record them on the nLab. (This also helps in case you later want to be cited for a contribution! :)

    Looking through your tweets, it seems the new reference is Arone & Ching 2019, Exp. 2.6. I have recorded that now at Goodwillie calculus (here) and added a pointer from exponential modality (there). Please feel invited to expand!

    • CommentRowNumber29.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 25th 2023
    • (edited Aug 25th 2023)

    Ok, let me collect things here for the moment.

    The graded exponentials of bounded linear logic should correspond to polynomial approximations of the Goodwillie tower of Σ ∞Ω ∞\Sigma^\infty \Omega^\infty.

    Then on an old thread you’re telling us that Σ ∞Ω ∞\Sigma^\infty \Omega^\infty is the co-commutative coalgebra co-operad, which I then point out has the sphere spectrum as each coefficient.

    And then there’s the idea that Σ ∞\Sigma^\infty is wedging with the sphere spectrum, while Ω ∞\Omega^\infty is adjoint, so maps into. Perhaps then there’s something close to a costate comonad about this composite.

    Then what to say about coalgebras for Σ ∞Ω ∞\Sigma^\infty \Omega^\infty? There should be something lens-like about them. But we know that a divided power coalgebra over Σ ∞Ω ∞\Sigma^\infty \Omega^\infty is an object XX equipped with morphisms X→𝕊⊗ Σ nX ⊗nX \to \mathbb{S} \otimes_{\Sigma_n} X^{\otimes n}.

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023
    • (edited Aug 25th 2023)

    which I then point out has the sphere spectrum as each coefficient.

    I haven’t spotted this statement in the reference you give (there), but it is part of the statement by Arone & Ching 2019, Exp. 2.6 that is now recorded here.

    idea that Σ ∞\Sigma^\infty is wedging with the sphere spectrum, while Ω ∞\Omega^\infty is adjoint, so maps into.

    This is only loosely speaking: The actual adjunction which induces the exponential modality is the composition of that which induces the 𝟙\mathbb{1}-costate comonad on parameterized spectra with the quantumly-coreflection onto actual spectra – this is shown in the diagram here (currently p. 34 of the draft).

    Then what to say about coalgebras for Σ ∞Ω ∞\Sigma^\infty \Omega^\infty?

    That’s a good question. I’d expect that the adjunction is comonadic, so that the Σ ∞Ω ∞\Sigma^\infty \Omega^\infty-coalgebras are the spaces in their incarnation as suspension spectra. This would fit with your comment about Σ ∞Ω ∞\Sigma^\infty \Omega^\infty-coalgebras being comonoids, because suspension spectra are singled out as being co-ring spectra (here).

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023
    • (edited Aug 25th 2023)

    I see (via Tim Campion MO:a/333720) that the Σ ∞Ω ∞\Sigma^\infty \Omega^\infty-comonadicity of (simply connected, pointed) spaces over spectra is Thm 1.8 in

    • Jacobson R. Blomquist, John E. Harper, Suspension spectra and higher stabilization [arXiv:1612.08623]

    Will add this to some entry now…

    • CommentRowNumber32.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 26th 2023

    Bounded linear logic was introduced to model resource use, e.g., polynomial-time computability. So I wonder if having bounded ! n!_n in linear HoTT could speak to the resources needed in quantum computing.

    To further the bounded exponential idea, I guess I should work out adjunctions for the corresponding graded comonad. Presumably on the stable homotopy side, it’s about polynomial approximations.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeAug 26th 2023

    It’s certainly true that in practical quantum computation the plain exponential modality, understood as

    !ℋ≔⊕ψ∈ℋℂ, ! \mathscr{H} \,\coloneqq\, \underset{\psi \in \mathscr{H}}{ \oplus} \mathbb{C} \,,

    is completely unrealistic, since for non-zero ℋ\mathscr{H} it produces an infinite-dimensional space of states, which does not exist in a real digital quantum computer.

    (Even if it did or could be approximated for practical purposes, it would be absurdly inefficient. The exponential modality is a tool of theory, not of practice.)

    But also theoretically, the exponential modality is a hack in order to model behaviour of classical types in a purely linear type theory. This hack was needed as long as problems remained with formulating combined classical and linear (“bunched”) types.

    But once/since we have dependent linear type theory, we no longer need an exponential modality to get access to classical types. A formal way to say this is to show that in dependent linear type theory the exponential modality can be constructed from the basic type formation rules, hence is “already there” should one insist on using it.

    To my mind, this construction of the exponential modality in LHoTT serves to show how previous work on linear type theory embeds into the dependent linear framework, for backward compatibility. But once we have dependent linear type theory the exponential modality loses its relevance as a way to get access to, say, “duplicatable data”. And I don’t see that it wants to be used for quantum information protocols.

    Of course, it’s still gonna be useful elsewhere, and if its Goodwillie-Taylor tower can be shown to follow what people call bounded linear logic, that would be interesting. How interesting this would be depends on how much developed bounded linear type theory is.

    This I currently don’t have an idea about. I sense you do, but you haven’t shared it yet. You could go to the entry bounded linear logic and give it some content.

    • CommentRowNumber34.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 26th 2023

    Thanks. Well, I’ve been hearing a great deal from a colleague in Computing here about the use of graded (co)monads to deal with resource use issues, so I was vaguely imagining that something similar might carry over to quantum computing resources. I’ll have a think, when I have a moment.

    • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 29th 2023

    Typos:

    monoial; epsistemic

    • CommentRowNumber36.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 29th 2023

    I see in Lit 2.10 you’re talking about RR-linear tangent ∞\infty-toposes for general E ∞E_{\infty}-ring spectrum RR. I don’t think we have anything on the nnLab about this generality, e.g., here it’s just about a unique tangent ∞\infty-topos.

    I sense it would be good to try to approach Michael Ching et al.’s work on tangent structures.

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeAug 29th 2023

    Thanks, I am fixing the typos.

    For RR-linear tangent ∞\infty-toposes I’d point to Joyal locus, brief at it is.

    • CommentRowNumber38.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 30th 2023

    There probably should be a way to connect this Joyal locus approach to tangency with Michael Ching et al.’s, as in

    They’re after a kind of action by a monoidal ∞-category of Weil algebras.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeAug 30th 2023
    • (edited Aug 30th 2023)

    To my mind, the statement connected to Joyal loci – let’s call it Biedermann’s theorem – is not a particular “approach” to anything, but is a remarkable fact of ∞\infty-topos theory (a phenomenon, if you wish, something we observe in the Platonic universe), namely the fact (and its further generalization) that the ∞\infty-Grothendieck constructions on ∞\infty-categories of module spectra are themselves again ∞\infty-toposes.

    It is this fact that is crucial for categorical semantics of LHoTT: Because, LHoTT is an extension of plain HoTT and hence any categorical semantics should in particular be an ∞\infty-topos.

    This is a curious demand (as per the very topic of this thread here) since models of LHoTT also need to have plenty of sub-∞\infty-categories which are stable, and it might seem that it is too much to ask for all these stable ∞\infty-categories to amalgamate into an ∞\infty-topos, since non-trivial stable ∞\infty-categories by themselves are never ∞\infty-toposes, and vice versa.

    But Bidermann’s theorem says that it works: The ∞\infty-categories of parameterized module spectra over varying bases needed to interpret the linear types of LHoTT are in fact ∞\infty-toposes and hence do also interpret the classical types and the univalent universes of the HoTT underlying LHoTT.

    \,

    (Up to coherence issues, that is. A type-theoretic model category interpreting LHoTT remains to be found. This is going to be tough. The model category in Entanglement of Sections interprets just a small fragment of LHoTT – the “motivic yoga” over classical types – but is very far from being a model for the underlying full HoTT. In any case, this is another discussion.)

    • CommentRowNumber40.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 31st 2023
    • (edited Aug 31st 2023)

    a remarkable fact of ∞-topos theory

    I see Joyal and Anel in Topo-logie describe it as

    a surprise for everybody in the higher category community.

    Reading further the first Ching article in #38, I think there may be some interesting there. He’s producing a representable geometric tangent ∞\infty-topos, alongside the usual corepresentable Goodwillie tangent ∞\infty-topos. For an ∞\infty-topos, 𝒳\mathcal{X}, the geometric tangent ∞\infty-topos is the exponential 𝒳 T(𝒮)\mathcal{X}^{T(\mathcal{S})}, where T(𝒮)T(\mathcal{S}) is the ∞-topos of parameterized spectra. So it’s in the vein of synthetic differential geometry.

    The article ends with him grappling with the problem that “These exponential objects do not appear to be easy to calculate”

    The exponential objects U(𝒳)=𝒳 T(𝒮)U(\mathcal{X}) = \mathcal{X}^{T(\mathcal{S})}, however, do not seem to have a simple description, and we do not have a good understanding of the geometric tangent structure in its entirety,

    so he works with injective ∞\infty-toposes.

    Don’t know if any of this provides further LHoTT models.

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeAug 31st 2023

    a surprise for everybody in the higher category community.

    Indeed. When I highlighted this fact on slide 6 of my 2014 presentation to a room full of homotopy type theorists in Paris (including M.A.), the chair doubted it and my talk was bogged down in debate. I could say more about this remarkable event were it not for de mortuis nil nisi bonum. Maybe 10 years later the community is ready now.

    I think there may be some interesting there

    That sounds somewhat harsh towards Ching, whose articles are packed with interesting insights. His program there is to further strengthen the formal analogy between Goodwillie calculus and differential geometry, which is a great cause.

    What’s not so clear is what aspect you mean to bring up here for which purpose.

    We had the same problem further above with bounded linear logic: You mention the term and seem to expect a reaction on my part, but don’t say what you have in mind in the first place! I’d still be interested in reading up on your perspective in an expanded version of the entry bounded linear logic! :-)

    • CommentRowNumber42.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 31st 2023

    Sadly, too many things on the boil.

1 to 42 of 42

  1.