Theorems · Theorem · category theory

CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  CategoryTheory.StructuredArrow.Hom.right
      (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).inv =
    (CategoryTheory.Bicategory.LanLift.CommuteWith.isKan f g h).desc
      (CategoryTheory.Bicategory.lanLiftLeftLift f (CategoryTheory.CategoryStruct.comp h g))

Defined in

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory.HasLeftKanLiftCategoryTheory.Bicategory.LanLift.CommuteWith