Theorems · Inductive type · category theory

CategoryTheory.Bicategory.HasLeftKanExtension

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

The existence of a left Kan extension of g along f.

Defined in

Mathlib.CategoryTheory.Bicategory.Kan.HasKan

Cited by

19 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Bicategory