Theorems · Definition · category theory

CategoryTheory.Bicategory.LeftLift

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

Triangle diagrams for (left) lifts. `` b ◹ | lift / | △ / | f | unit / ▽ c - - - ▷ a g ``

Defined in

Mathlib.CategoryTheory.Bicategory.Extension

Cited by

29 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory