Theorems · Theorem · category theory

CategoryTheory.Presheaf.uliftYonedaAdjunction.congr_simp

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A]
  (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ)
  (α α_1 : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) (e_α : α = α_1) [inst_3 : L.IsLeftKanExtension α],
  CategoryTheory.Presheaf.uliftYonedaAdjunction L α = CategoryTheory.Presheaf.uliftYonedaAdjunction L α_1

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.HasPointwiseLeftKanExtensionCategoryTheory.Functor.IsLeftKanExtension