Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Bicategory.RightLift.IsAbsKan.isKan

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

An absolute right Kan lift is a right Kan lift.

Defined in
Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Cited by
0 results in Mathlib
Foundations
Depth 34 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.

Quiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.Bicategory · cited by 1587CategoryTheory.BicategoryCategoryTheory.Bicategory.RightLift · cited by 19Bicategory.RightLiftCategoryTheory.Bicategory.RightLift.whisker · cited by 8RightLift.whiskerCategoryTheory.Bicategory.RightLift.IsKan · cited by 5RightLift.IsKanCategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelf · cited by 2RightLift.whiskerOfIdComp…CategoryTheory.Bicategory.RightLift.IsAbsKan · cited by 0RightLift.IsAbsKanCategoryTheory.Bicategory.RightLift.IsKan.ofIdComp · cited by 0IsKan.ofIdCompCategoryTheory.Bicategory.RightLift.IsKan.ofIsoKan · cited by 0IsKan.ofIsoKanIsAbsKan.isKanCITED BYCITES

Cites10

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.