Theorems · Theorem · category theory

CategoryTheory.Functor.relativelyRepresentable.symmetry_fst_assoc

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful] {Z : C} (h : a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.fst' f') h) =
    CategoryTheory.CategoryStruct.comp (hf'.snd g) h

Defined in

Mathlib.CategoryTheory.MorphismProperty.Representable

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.FullCategoryTheory.Functor.Faithful