You can see examples at http://ncatlab.org/nlab/show/bicategory

Ah, it's only for bicategories. I was expecting a definition in dependent type theory of omega-categories. That would have helped me understanding it.

The answer is the same: when stating the associativity law, you begin with objects W,X,Y,Z and go on from there.

Yes, it makes sense. Thank you. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]