The blue social bookmark and publication sharing system.
Log in with your username.
I've lost my password.
Log in with your OpenID-Provider.
An introduction to 2-categories is given by illustrating how the structure of typed lambda calculus may naturally be viewed as a 2-category. In this vein. the structure of computations or conversions gives rise to notions of lax 2':"adjointness.