Suppose you want to work with TQFTs in homotopy type theory (HoTT). Working with $(\infty,n)$-categories, or even $(\infty,1)$-categories, is something that I gather is too difficult for HoTT at the moment because of coherence issues. However, you could just forget all noninvertible cobordisms, and you should be able to obtain an $\infty$-groupoid from your $(\infty,1)$-category of cobordisms. Then you could try to define functions from this $\infty$-groupoid to other $\infty$-groupoids, ideally inspired by TQFT invariants.

Is there an inductive definition in HoTT of such a "groupoid of manifolds?" I'd also be happy with something like an $\infty$-groupoid of knots in $S^3$.

  • 1
    $\begingroup$ One motivation for this question is the existence of naturality results for Heegaard Floer homology (arxiv.org/abs/1210.4996) and related theories. One could at least try to reformulate such results in the language of higher groupoids, and HoTT seems like an enticing possibility for doing this cleanly. $\endgroup$ – Andy Manion Sep 25 '15 at 21:04
  • $\begingroup$ Do you mean in HoTT or in some interpretation of HoTT? $\endgroup$ – user40276 Sep 25 '15 at 21:06
  • $\begingroup$ I'd prefer in HoTT itself- something inductively defined and thus (ideally) easy to work with. $\endgroup$ – Andy Manion Sep 25 '15 at 21:07
  • 1
    $\begingroup$ Maybe there's some formulation in cohesive HoTT (ncatlab.org/nlab/show/cohesive+homotopy+type+theory) . However as I understand this is done inside an infinity topos. $\endgroup$ – user40276 Sep 25 '15 at 21:16
  • 2
    $\begingroup$ @DavidRoberts: The OP discards all noninvertible bordisms, which results in a vastly different category than Lurie's. $\endgroup$ – Dmitri Pavlov Sep 26 '15 at 15:11

Your Answer

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

Browse other questions tagged or ask your own question.