Theorems · Inductive type · category theory

CategoryTheory.Bicategory.Adj

(B : Type u) → [CategoryTheory.Bicategory B] → Type u

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).

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Cited by

131 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Bicategory