# Is there a definition of an $\infty$-groupoid in HoTT whose terms are $n$-manifolds and whose higher morphisms are diffeomorphisms/isotopies/etc?

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$.

• 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. – Andy Manion Sep 25 '15 at 21:04
• Do you mean in HoTT or in some interpretation of HoTT? – user40276 Sep 25 '15 at 21:06
• I'd prefer in HoTT itself- something inductively defined and thus (ideally) easy to work with. – Andy Manion Sep 25 '15 at 21:07
• 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. – user40276 Sep 25 '15 at 21:16
• @DavidRoberts: The OP discards all noninvertible bordisms, which results in a vastly different category than Lurie's. – Dmitri Pavlov Sep 26 '15 at 15:11