Thorsten Altenkirch and Ondřej Rypáček, a syntactical approach to weak omega-groupoids, [pdf](http://www.cs.nott.ac.uk/~txa/publ/weakomega2.pdf) ## Abstract When moving to a Type Theory without proof-irrelevance the notion of a [[setoid]] has to be generalized to the notion of a weak omega-groupoid. As a first step in this direction we study the formalisation of weak omega-groupoids in Type Theory. This is motivated by Voevodsky’s proposal of univalent type theory which is incompatible with proof-irrelevance and the results by Lumsdaine and Garner/van de Berg showing that the standard eliminator for equality gives rise to a weak omega-groupoid.