# Fibration of Batanin/Leinster $\omega$-groupoids

Is there (defined somewhere) a notion of fibration between two weak $\omega$-groupoids in the sense of Batanin/Leinster? I tried to search on Google and in Higher Operads, Higher Categories of Tom Leinster, but I haven't found anything.
This would probably be very useful for interpreting Martin-Löf type theory in the category of Batanin/Leinster weak $\omega$-groupoids.

-
Excellent question. There is a definition of a fibration of 2-groupoids (Hardie-Kamps-Kieboom) which is too strict, and also Hermida's definition, but I think there is another definition out there, which should be exemplified by the map of fundamental bigroupoids induced by a Dold fibration of spaces. My gut feeling is that this low-dimensional example will give good insight into the $\infty$-case. –  David Roberts Jan 4 '12 at 23:39
I don't know of one. –  Tom Leinster Jan 9 '12 at 12:50
I haven't seen one written down, but in the case of $\omega$-groupoids (as opposed to $\omega$-categories) it should be easy to define: just stipulate that every k-morphism lifts with every possible domain (or codomain), as for an isofibration. The tricky part would probably be showing that these are the right class of a WFS. –  Mike Shulman Jan 13 '12 at 17:21

There isn't one existing. There is something on the completely strict omega-categorical case in Michael Warren's article "The strict ω-groupoid interpretation of type theory" (available from his web page at IAS).

However we have a PhD student here at Macquarie working on higher fibrations and all that so hopefully there will be something on the weak case in due course!

-
Welcome to MO, Richard! That's good news; I look forward to seeing the thesis. –  Mike Shulman Jan 24 '12 at 18:17
(arXiv:1009.5609) in which the notion of fibration is just a Kan fibration of cubical sets. However I understand a cubical version of weak $\omega$-groupoids has not been developed (attempted?).