Theorems · Definition · category theory

CategoryTheory.Adjunction.CoreUnitCounit.recOn

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {motive : CategoryTheory.Adjunction.CoreUnitCounit F G → Sort u} →
              (t : CategoryTheory.Adjunction.CoreUnitCounit F G) →
                ((unit : CategoryTheory.Functor.id C ⟶ F.comp G) →
                    (counit : G.comp F ⟶ CategoryTheory.Functor.id D) →
                      (left_triangle :
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit F)
                              (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit)) =
                            CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F)) →
                        (right_triangle :
                            CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit)
                                (CategoryTheory.CategoryStruct.comp (G.associator F G).inv
                                  (CategoryTheory.Functor.whiskerRight counit G)) =
                              CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C))) →
                          motive
                            { unit := unit, counit := counit, left_triangle := left_triangle,
                              right_triangle := right_triangle }) →
                  motive t

Defined in

Mathlib.CategoryTheory.Adjunction.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category