Theorems · Theorem · category theory

CategoryTheory.Functor.sectionsEquivHom_naturality

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F G : CategoryTheory.Functor C (Type u₂)} (f : F ⟶ G)
  (X : Type u₂) [inst_1 : Unique X] (x : ↑F.sections),
  (G.sectionsEquivHom X) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.sectionsFunctor C).map f)) x) =
    CategoryTheory.CategoryStruct.comp ((F.sectionsEquivHom X) x) f

Defined in

Mathlib.CategoryTheory.Yoneda

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryUnique