homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
In higher category theory, the exchange law, or interchange law, states that the multiple ways of forming the composite of a pasting diagram of k-morphisms are equivalent.
The first exchange law (often called the exchange law) asserts that for composition of 2-morphisms we have an equivalence
asserting a compatibility of horizontal composition and vertical composition of 2-morphisms.
In a bicategory this equivalence is an identity. In even higher (and non-semi-strict) category theory, the interchange law becomes a higher morphism itself: the exchanger.
One way to capture all exchange laws combinatorially is encoded by the cosimplicial -cateory that induces the homotopy coherent nerve. See there for more details on how this encodes the exchange laws.