Theorems · Theorem · category theory

CategoryTheory.Over.postAdjunctionRight_counit_app

∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {Y : D} {F : CategoryTheory.Functor T D} {G : CategoryTheory.Functor D T} (a : F ⊣ G)
  (A : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj Y)),
  (CategoryTheory.Over.postAdjunctionRight a).counit.app A = CategoryTheory.Over.homMk (a.counit.app A.left) ⋯

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category