Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Bicategory.RightLift.IsKan.desc

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.RightLift f g} →
            t.IsKan → (s : CategoryTheory.Bicategory.RightLift f g) → s.lift ⟶ t.lift

The family of 2-morphisms into a right Kan lift.

Defined in
Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Cited by
4 results in Mathlib
Foundations
Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.Bicategory
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Bicategory.RightLift.IsKan.fac · cited by 1IsKan.facCategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso_hom_left · cited by 0IsKan.uniqueUpToIso_hom_l…CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso_inv_left · cited by 0IsKan.uniqueUpToIso_inv_l…CategoryTheory.Bicategory.RightLift.IsAbsKan.desc · cited by 0IsAbsKan.descCategoryTheory.Bicategory.RightLift.IsKan.fac_assoc · cited by 0IsKan.fac_assocQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Bicategory · cited by 1587CategoryTheory.BicategoryCategoryTheory.Bicategory.RightLift · cited by 19Bicategory.RightLiftCategoryTheory.Bicategory.RightLift.lift · cited by 13RightLift.liftCategoryTheory.Bicategory.RightLift.IsKan · cited by 5RightLift.IsKanCategoryTheory.CostructuredArrow.IsUniversal.lift · cited by 5IsUniversal.liftIsKan.descCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.