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