The walking adjoint equivalence (as in βwalking structureβ) or free-standing adjoint equivalence is the 2-category (in fact a (2,1)-category) which βrepresentsβ adjoint equivalences in a 2-category. It is a categorification of the free-standing adjoint isomorphism?.
The free-standing adjoint equivalence is the unique (up to isomorphism) 2-category with exactly two objects and , 1-morphisms freely generated by an arrow , and an arrow , and 2-morphisms generated by 2-isomorphisms and , subject to the equalities
The arrow is an adjoint equivalence.
The free-standing adjoint equivalence is a (2,1)-category.
is the model for all adjoint equivalences in all 2-categories. In other words, any adjoint equivalence in a 2-category is just a 2-functor from :
Let be a 2-category (weak or strict). Let be a 1-arrow of which is part of an adjoint equivalence. Then there is a 2-functor such that the arrow of maps under to .
Immediate from the definitions.
the boolean domain ; i.e. the walking pair of objects
the directed interval category ; i.e. the walking morphism
the (2,0)-horn category ; i.e. the walking cospan
the (2,1)-horn category ; i.e. the walking composable pair
the (2,2)-horn category ; i.e. the walking span
the 2-simplex category ; i.e. the walking commutative triangle
Adj; i.e. the walking adjunction
the syntactic category of a theory ; i.e. the walking -model
In dependent type theory, many higher inductive types can be considered to be walking structures:
the boolean type is the walking pair of elements
the interval type is the walking identification
one definition of the circle type is the walking self-identification
another definition of the circle type is the walking parallel pair of identifications.
the suspension type of a type is the walking parallel -indexed family of identifications.
the natural numbers type is the walking sequence
the integers type is the walking bi-infinite sequence
the walking bridge
the directed interval type is the walking morphism in the sense of element of a hom type
Last revised on June 1, 2025 at 04:07:27. See the history of this page for a list of all contributions to it.