Theorems · Definition · category theory

CategoryTheory.Bicategory.LeftExtension

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

Triangle diagrams for (left) extensions. `` b △ \ | \ extension △ f | \ | unit | ◿ a - - - ▷ c 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