Are there any "visions" (maybe "dreams"), future plans or connections between Homotopy type theory and Grothendieck's theory of motives (or at least "connections" with universal cohomology theory)?


closed as too broad by Yemon Choi, Stefan Kohl, Joonas Ilmavirta, Marco Golla, José Figueroa-O'Farrill Jul 20 '15 at 21:31

Please edit the question to limit it to a specific problem with enough detail to identify an adequate answer. Avoid asking multiple distinct questions at once. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 3
    $\begingroup$ I think the best we can hope here is that some 'interesting' modification of the motivic homotopy category would be an infinity topos and hence could be manipulated using homotopy type theory... $\endgroup$ – Simon Henry Jul 17 '15 at 13:50
  • 2
    $\begingroup$ ...assuming that homotopy type theory actually does end up modeling every infinity topos, which from what I understand has not been proven yet. $\endgroup$ – David White Jul 17 '15 at 14:28
  • 3
    $\begingroup$ Well, motivic homotopy theory is a presentable locally cartesian closed ∞-category, and therefore it admits a presentation by a type-theoretic model category. Of course, univalence does not hold... $\endgroup$ – Marc Hoyois Jul 17 '15 at 18:11
  • 7
    $\begingroup$ Downvoting because this question consists of little more than "X and Y are cool. Is there any kind of connection between X and Y?" $\endgroup$ – Daniel Miller Jul 18 '15 at 12:20
  • 1
    $\begingroup$ I agree with Daniel Miller $\endgroup$ – Yemon Choi Jul 20 '15 at 19:16