Theorems · Theorem · category theory

CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app

∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (a : CategoryTheory.Functor (C × D) E) {X Y : D}
  (f : X ⟶ Y) (j : C),
  ((CategoryTheory.Functor.curryingFlipEquiv.symm a).map f).app j =
    a.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id j) f)

Defined in

Mathlib.CategoryTheory.Functor.Currying

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category