The bicategory of adjunctions in a bicategory #
Given a bicategory B
, we construct a bicategory Adj B
that has essentially
the same objects as B
but whose 1
-morphisms are adjunctions (in the same
direction as the left adjoints), and 2
-morphisms are tuples of mate maps
between the left and right adjoints (where the map between right
adjoints is in the opposite direction).
Certain pseudofunctors to the bicategory Adj Cat
are analogous to bifibered categories:
in various contexts, this may be used in order to formalize the properties of
both pullback and pushforward functors.
References #
- https://ncatlab.org/nlab/show/2-category+of+adjunctions
- https://ncatlab.org/nlab/show/transformation+of+adjoints
- https://ncatlab.org/nlab/show/mate
The bicategory that has the same objects as a bicategory B
, in which 1
-morphisms
are adjunctions (in the same direction as the left adjoints),
and 2
-morphisms are tuples of mate maps between the left and right
adjoints (where the map between right adjoints is in the opposite direction).
- obj : B
Instances For
Given two objects a
and b
in a bicategory,
this is the type of adjunctions between a
and b
.
the left adjoint
the right adjoint
- adj : Adjunction self.l self.r
the adjunction
Instances For
Equations
- One or more equations did not get rendered due to their size.
A morphism between two adjunctions consists of a tuple of mate maps.
the morphism between left adjoints
the morphism in the opposite direction between right adjoints
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Bicategory.Adj.instCategoryHom = { toCategoryStruct := CategoryTheory.Bicategory.Adj.instCategoryStructHom, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }
Constructor for isomorphisms between 1-morphisms in the bicategory Adj B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The associator in the bicategory Adj B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left unitor in the bicategory Adj B
.
Equations
Instances For
The right unitor in the bicategory Adj B
.
Equations
Instances For
The left whiskering in the bicategory Adj B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right whiskering in the bicategory Adj B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
The forget pseudofunctor from Adj B
to B
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given an isomorphism between two 1-morphisms in Adj B
, this is the
underlying isomorphisms between the left adjoints.
Equations
Instances For
Given an isomorphism between two 1-morphisms in Adj B
, this is the
underlying isomorphisms between the right adjoints.