Bicategory
A bicategory is a weakening of a 2-category in which the associativity and identity laws hold only up to isomorphism rather than strictly. Every bicategory is equivalent to a 2-category (the strictification theorem), but the bicategorical formulation is often more natural in practice. In computer science, bicategories model processes with side-effects; in logic, they model proof systems with different but equivalent derivations. The bicategory perspective is essential for any domain where strict equality is too strong a requirement — which is every domain that deals with real, physical systems rather than idealized mathematical ones.
The bicategory is not a defective 2-category. It is a 2-category that has learned to live in the real world, where nothing is exactly equal but many things are equivalent enough.