17
$\begingroup$

This is a combined question, strictly speaking I am asking three questions concerning, respectively, homotopy type theory, stable homotopy theory and Yetter-Drinfeld modules. But I believe in the present context they can be viewed as a single question.

After a lecture on HoTT by Voevodsky (at TACL 2013 in Nashville) I asked him whether Homotopy Type Theory can be useful for stable homotopy theory. Without much hesitation he replied that HoTT is not really well suited to describe stable phenomena. We never talked after that, and now we will never talk at all, so I still do not know where the main difficulty lies.

Discussing this with several other people (sorry, don't exactly remember with whom) I gradually developed impression that the main difficulty relates to the fact that there seems to be no known good formalism combining constructive type theory and substructural logics, that would lead to some sort of linear type theory. Among possible models one should have triangulated monoidal categories, like stable homotopy category, and it seems not to be known what is the analog of dependent types there.

The first question then is whether what I said above makes any sense, and whether there is any work in this direction.

A situation where one has something like "linear dependent types" is in the context of Yetter-Drinfeld modules over Hopf algebras. Heuristically, the starting point is the fact that in any category $\mathscr C$ with (Cartesian) products every object $X$ has a unique comonoid structure, and the category of comodules over this comonoid is equivalent to the slice $\mathscr C/X$. One could then try to imitate this in (non-Cartesian) monoidal categories, considering comodules over comonoids as variable families over that comonoid. When this comonoid is equipped with a Hopf monoid structure, one can get a "linear" analog of Freyd-Yetter's crossed G-sets.

The second question is then, whether anybody studied features of categories of Yetter-Drinfeld modules over varying Hopf algebras which would resemble either what happens in HoTT or in stable homotopy category.

And the third question comes from the fact that while there are plenty of examples of monoids in stable homotopy categories (ring spectra) I cannot remember any considerations of comonoids or Hopf objects there. Does anybody know some works on this? Or even more simple question (actually fourth, sorry): in unstable homotopy theory one knows that for a, say, topological group $G$ there are certain homotopy categories of $G$-spaces and of spaces over $BG$ which are equivalent. Is there an analog of this fact in stable homotopy theory?

Or maybe Voevodsky had in mind that there seems to be no analog of univalence in the stable context? (Well that was fifth, I certainly must stop here.)

I found only one related question, Are there connections between Homotopy type theory and Grothendieck's theory of motives?, about possible connections between HoTT and motivic homotopy theory. I discovered my pessimistic comment there, remembering that answer by Voevodsky and arguing that motivic homotopy is in a sense even "more linear" than stable homotopy, so it might be even more difficult to relate these two. Anyway.

$\endgroup$
  • 2
    $\begingroup$ I would assume that he had in mind that there is no analogue of univalence in the stable context... Although maybe there is something to work on regarding the fact that the category of parametrized spectra is an $\infty$-topos... But Type theory with just identity type is suppose to be the internal logic of finitely complete $(\infty,1)$-category, so one can probably define an internal logic of stable categories which would be an extension of dependant type theory with identity type ? (this has not been done as far as I know) $\endgroup$ – Simon Henry Oct 12 '17 at 22:08
  • 2
    $\begingroup$ HoTT, in the sens of the full system with exponential, $\Pi$-type, univalent Univers etc... probably not. But bare dependant type theory with just identities and sigma and additional axioms assuring that every object is pointed and that the loop construction is an equivalence should corresponds to the internal logic of stable $\infty$-category. In fact I would believe it can be proved using (maybe extending a little) the recent of K.Szumilo and C.Kapulkin arxiv.org/abs/1709.09519 that I hadn't time to look at in details yet, as well as previous works of Szumilo... $\endgroup$ – Simon Henry Oct 12 '17 at 22:23
  • 1
    $\begingroup$ ... There are things to prove of course, and I don't have a precise formulation of these axioms in mind. Moreover it would give a very asymmetrical presentation of stable categories (where limits and colimits are treated very differently) which might be unsatisfying. $\endgroup$ – Simon Henry Oct 12 '17 at 22:27
  • 2
    $\begingroup$ You may find interesting attempts to form a linear dependent type theory/dependent homotopy type theory, discussed here: ncatlab.org/nlab/show/dependent+linear+type+theory. $\endgroup$ – David Corfield Oct 13 '17 at 7:34
  • 2
    $\begingroup$ I meant to write "dependent linear type theory/linear homotopy type theory". I'd recommend Urs Schreiber's 'Quantization via Linear homotopy types' arxiv.org/abs/1402.7041 as well. He wrote much of that nLab page. $\endgroup$ – David Corfield Oct 13 '17 at 7:51
10
$\begingroup$

With respect to the first question, expanding on my comment which pointed out the nLab page dependent linear type theory and the article by Urs Schreiber, 'Quantization via Linear homotopy types', I'd like to pass on some additional relevant commentary by Urs.

There is a way to express linearity for homotopy types, see stable homotopy type. As Simon pointed out in his comment, the category of parametrized spectra is an ∞-topos, indeed a tangent ∞-topos. One can then look to add an axiom to HoTT that makes it the internal language for tangent ∞-toposes. That axiom should be:

  1. there is a pointed type $X_\ast$

  2. the morphism $\Sigma \Omega X_\star \to X_\star$ is an equivalence

So far this makes the ambient category "linear" in the terminology of Schwede's old article on parameterized spectra. One could now continue to add the axioms

  1. the morphism $\Sigma \Omega(X_\star^{S_\star}) \to X_\star^{S_\star}$ is an equivalence, for finite pointed powers.

If one could add the infinite set of these axioms, that would be Goodwillie's localization for the tangent $\infty$-topos.

There's work in preparation by Mathieu Anel, Eric Finster, and André Joyal along these lines.

$\endgroup$
  • 1
    $\begingroup$ Thanks, David. I had advertized tangent infinity-toposes as a route for HoTT to go stable in 2014 in my talk at the IHP trimester on Semantics of proofs and certified mathematics in Workshop 1: "Formalization of Mathematics"; the talk notes are here: ncatlab.org/schreiber/show/… $\endgroup$ – Urs Schreiber Oct 13 '17 at 15:34
  • $\begingroup$ Lest this give the wrong impression, let me point out that nearly all of the content at ncatlab.org/nlab/show/dependent+linear+type+theory is not type theory but category theory. The reason it was placed there is, I guess, that the categories it takes place in are the conjectural models of some as-yet-undefined notion of dependent linear type theory. $\endgroup$ – Mike Shulman Oct 13 '17 at 16:01
  • $\begingroup$ @MikeShulman , sure, the first paragraphs mean to be quite explicit about that. But if it doesn't become clear enough, I am happy to add more highlighting or else rename. There is some elaboration of syntax for linear dependent type theory in Vakar's thesis ncatlab.org/nlab/show/… $\endgroup$ – Urs Schreiber Oct 13 '17 at 16:18
  • $\begingroup$ Mike went ahead and split my "semantics" content from the page on "dependent linear type theory" off to its own page here: ncatlab.org/nlab/show/indexed+monoidal+(infinity,1)-category $\endgroup$ – Urs Schreiber Oct 16 '17 at 10:24
8
$\begingroup$

There are multiple possible routes to study stable homotopy theory in a type-theoretic system, some of which are work in progress by various people, but none of which are fully developed.

As has been pointed out, one can make use of the fact that the category of parametrized spectra is an $(\infty,1)$-topos and therefore (conjecturally) admits an interpretation of HoTT, then use this model to motivate new structures and axioms for HoTT to produce a "homotopy type theory of parametrized spectra" analogous to what we have done for directed and cohesive homotopy type theories. There is work in progress on deciding what exactly these new features should be.

On the other hand, one can try to attack the category of spectra directly. As has been pointed out, since it has finite limits it conjecturally admits a model of dependent type theory but without $\Pi$-types and without a universe. This lack makes it almost impossible to do anything resembling current homotopy type theory purely inside spectra. What seems more useful is to have an ambient unstable homotopy type theory which can be related to the stable one in some way. So that, for instance, we have an unstable homotopy type of maps between two spectra, and can talk about homotopies and apply the theory of h-levels and equivalences (using unstable $\Pi$-types) in that way. There could also be an unstable universe of stable types that is "univalent" in an appropriate sense.

When one plays with this a bit, it starts to seem very natural, even necessary, to allow stable homotopy types to depend on unstable ones, so that we are heading back in the direction of parametrized spectra. But now instead of considering each parametrized spectrum as a basic object, we are stratifying them over their base spaces, with two context zones for unstable and stable types. In the non-homotopy context, it's not hard to write down such a type theory that has models in "indexed monoidal categories", and that categorical structure can be generalized to "indexed monoidal $(\infty,1)$-categories", which are mostly what the original nLab page "dependent linear type theory" is about (I've now moved that content to Indexed monoidal (∞,1)-category). But as far as I know, no one has yet proposed a good way to write down a homotopy type theory that has semantics in such indexed monoidal $(\infty,1)$-categories.

There is work by type theorists on "dependent linear logic". Some of it, such as "linear LF", I believe involves linear types dependent on nonlinear ones. But I'm not aware of any version of such a theory yet that would, for instance, allow linear types to have non-linear identity types, which seems to me to be what we would want to be able to do stable homotopy theory this way.

$\endgroup$
  • 1
    $\begingroup$ Thanks for the information.You seem to be alluding to some further progress that has happened meanwhile. Is there any way that your hints as in "When one plays with this a bit..." could be materialized in some kind of reference that we could all look at? $\endgroup$ – Urs Schreiber Oct 16 '17 at 10:21
  • 1
    $\begingroup$ And now that you have split the nLab entry (thanks again!), maybe it would be good to remove the reference to a "misnamed nLab page" in your text above.. $\endgroup$ – Urs Schreiber Oct 16 '17 at 10:22
  • $\begingroup$ Thanks, done. (I meant to do that, but forgot.) $\endgroup$ – Mike Shulman Oct 17 '17 at 5:27
  • $\begingroup$ I like your new redaction of that nLab stuff very much. But (:D) mainly because it shows a new possibility to somehow get the whole stable structure "for free". What I have in mind is the idea of Franke and, I believe, Heller before him: impose (very strong) additional identities on transition functors in such a way that all cartesian and all cocartesian squares automatically become bicartesian. I believe this amounts to requiring left-right adjoint coincidence $\endgroup$ – მამუკა ჯიბლაძე Oct 17 '17 at 6:05
  • 1
    $\begingroup$ @მამუკაჯიბლაძე Well, those would be homotopy coherent comodules, and we don't know how to express infinite homotopy coherence in the finite syntax of type theory in general. I'm not sure what you have in mind regarding Franke and Heller. $\endgroup$ – Mike Shulman Oct 18 '17 at 14:52

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.