Composition of composable 2-cells in a 2-category is unambiguously defined?

I believe the following nice statement is true, but I cannot find a reference or proof it myself.

In a 2-category(i.e., bicategory), the composition of composable 2-cells is unambiguously defined.

Where 2-cells are 2-commutative triangles (other shape will not give more information), "composable" is not easy to say in simple words but it is easy to imagine.

Special cases of this statement include vertical composition of 2-morphisms are associative and the exchange law of vertical composition and horizontal composition.

Any comments or references would be appreciated. Thank you guys!

-

A well-known reference:

John Power, A 2-categorical pasting theorem, Journal of Algebra Volume 129, Issue 2, March 1990, Pages 439-445.

See the nLab page on pasting diagrams for more.

Power's paper just deals with strict 2-categories, if I remember correctly.

Edit: Following Todd's comment, here's the reference to Verity's thesis, where the bicategorical case is covered. The original thesis came out in 1992, but it has recently been reprinted:

Dominic Verity, Enriched categories, internal categories and change of base, Reprints in Theory and Applications of Categories No. 20 (2011) pp 1-266.

-
Yes, just strict 2-categories. There's also a bicategorical pasting theorem in Dominic Verity's thesis. – Todd Trimble Nov 23 '11 at 12:23
I just read the paper of Power. The most part of the paper is graph theory, i.e. how to phrase the theory precisely. The actual proof is a very short induction, and the induction part which have to do is left to reader"It is routine to apply the axioms for 2-category and ...". So, I think it works for weak 2-category too. – Ma Ming Nov 23 '11 at 15:13
Yes, I would imagine so. – Tom Leinster Nov 23 '11 at 16:16
A Weak 2-category or bicategory (I guess you mean) is biequivalent (doing by a pseudofunctor that locally is a equivalence) to a 2-category (strictifiable) by a generalized Yoneda Lemma, and then diagram of 2-cells is commutative (or coherent) in a bicategory iff it is commutative in its 2-category strictifications, then the coherence theorem (for 2-cells diagrams) on 2-category is automaticaly generalizable to bicategory. See T. Leinster article: front.math.ucdavis.edu/9810.5017 – Buschi Sergio Nov 23 '11 at 19:08
@Buschi Sergio: that's the rough idea, of course. It's another matter to nail down the precise details. See Verity's thesis for a full accounting. – Todd Trimble Nov 24 '11 at 1:13

I think Tom's answer is what was being looked for, but I just thought I would mention that there is another way of stating and proving such a theorem, namely using string diagrams instead of pasting diagrams. The corresponding theorem for string diagrams in a monoidal category was proven by Joyal and Street; the one for bicategories is an easy extension (but I don't know of anywhere that it appears in print). There are some references at the nLab page.

-

Se also "General associativity and general composition for double categories - Dawson, Robert; Pare, Robert"

Cahiers de Topologie et Géométrie Différentielle Catégoriques, 34 no. 1 (1993), p. 57-79

-

For simplicial compositions see Richard Steiner's paper

The algebraic structure of the universal complicial sets arXiv:1009.3384v1

-