Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Bicategory.RightLift.IsAbsKan

{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.RightLift f g → Type (max (max u v) w)

An absolute right Kan lift is a Kan lift such that every 1-morphism commutes with it.

Defined in
Mathlib.CategoryTheory.Bicategory.Kan.IsKan
Cited by
0 results in Mathlib
Foundations
Depth 28 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.IsAbsKan.desc · cited by 0IsAbsKan.descCategoryTheory.Bicategory.RightLift.IsAbsKan.isKan · cited by 0IsAbsKan.isKanCategoryTheory.Bicategory.RightLift.IsAbsKan.ofIsoAbsKan · cited by 0IsAbsKan.ofIsoAbsKanQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.Bicategory · cited by 1587CategoryTheory.BicategoryCategoryTheory.Bicategory.RightLift · cited by 19Bicategory.RightLiftCategoryTheory.Bicategory.RightLift.whisker · cited by 8RightLift.whiskerCategoryTheory.Bicategory.RightLift.IsKan · cited by 5RightLift.IsKanRightLift.IsAbsKanCITED BYCITES

Cites5

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

Cited by3

Results whose statement or proof uses this declaration.