Theorems · Definition · category theory

CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            (t : CategoryTheory.Bicategory.LeftExtension f g) →
              t.IsKan → {x : B} → (h : c ⟶ x) → [CategoryTheory.Bicategory.Lan.CommuteWith f g h] → (t.whisker h).IsKan

If h commutes with f⁺ g and t is another left Kan extension of g along f, then t.whisker h is a left Kan extension of g ≫ h along f.

Defined in

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory.HasLeftKanExtensionCategoryTheory.Bicategory.Lan.CommuteWith