Theorems · Definition · category theory
CategoryTheory.Bicategory.RightLift.lift
{B : Type u} →
[inst : CategoryTheory.Bicategory B] →
{a b c : B} → {f : b ⟶ a} → {g : c ⟶ a} → CategoryTheory.Bicategory.RightLift f g → (c ⟶ b)The lift of g along f.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Bicategory
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
- CategoryTheory.CostructuredArrow.leftproof · cited by 202
- CategoryTheory.Bicategory.RightLiftstatement and proof · cited by 19
Cited by21
Results whose statement or proof uses this declaration.
- CategoryTheory.Bicategory.RightLift.counitstatement · cited by 8
- CategoryTheory.Bicategory.RightLift.whiskerproof · cited by 8
- CategoryTheory.Bicategory.RightLift.ofIdCompproof · cited by 6
- CategoryTheory.Bicategory.RightLift.IsKan.descstatement · cited by 4
- CategoryTheory.Bicategory.RightLift.homMkstatement and proof · cited by 2
- CategoryTheory.Bicategory.RightLift.whiskerOfIdCompIsoSelfproof · cited by 2
- CategoryTheory.Bicategory.RightLift.IsKan.facstatement · cited by 1
- CategoryTheory.Bicategory.RightLift.whiskerIdCancelproof · cited by 1
- CategoryTheory.Bicategory.RightLift.IsAbsKan.descstatement · cited by 0
- CategoryTheory.Bicategory.RightLift.ofIdComp_homstatement · cited by 0
- CategoryTheory.Bicategory.RightLift.ofIdComp_leftstatement · cited by 0
- CategoryTheory.Bicategory.RightLift.IsKan.fac_assocstatement · cited by 0