Theorems · Theorem · category theory

CategoryTheory.Bicategory.Adjunction.ext

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  {x y : CategoryTheory.Bicategory.Adjunction f g}, x.unit = y.unit → x.counit = y.counit → x = y

Defined in

Mathlib.CategoryTheory.Bicategory.Adjunction.Basic

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound