Theorems · Theorem · category theory

CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.hom_ext

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P]
  {Φ :
    CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂})}
  (f g :
    CategoryTheory.Functor.LeftExtension.mk F.op.lan
        (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶
      Φ),
  f = g

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.HasLeftKanExtension