Documentation

Mathlib.CategoryTheory.Functor.Currying

Curry and uncurry, as functors. #

We define curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E)) and uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E), and verify that they provide an equivalence of categories currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E).

source
@[simp]
theorem CategoryTheory.uncurry_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X : C × D} {Y : C × D} (f : X ⟶ Y) :
(CategoryTheory.uncurry.toPrefunctor.obj F).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map f.1).app X.2) ((F.toPrefunctor.obj Y.1).toPrefunctor.map f.2)
source
@[simp]
theorem CategoryTheory.uncurry_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D), (CategoryTheory.uncurry.toPrefunctor.map T).app X_1 = (T.app X_1.1).app X_1.2
source
@[simp]
theorem CategoryTheory.uncurry_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D) :
(CategoryTheory.uncurry.toPrefunctor.obj F).toPrefunctor.obj X = (F.toPrefunctor.obj X.1).toPrefunctor.obj X.2
source
def CategoryTheory.uncurry {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E)) (CategoryTheory.Functor (C × D) E)

The uncurrying functor, taking a functor C ⥤ (D ⥤ E) and producing a functor (C × D) ⥤ E.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def CategoryTheory.curryObj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) :
    CategoryTheory.Functor C (CategoryTheory.Functor D E)

    The object level part of the currying functor. (See curry for the functorial version.)

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.curry_obj_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) :
      ∀ {X_1 Y : D} (g : X_1 ⟶ Y), ((CategoryTheory.curry.toPrefunctor.obj F).toPrefunctor.obj X).toPrefunctor.map g = F.toPrefunctor.map (CategoryTheory.CategoryStruct.id X, g)
      source
      @[simp]
      theorem CategoryTheory.curry_map_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
      ∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.curry.toPrefunctor.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
      source
      @[simp]
      theorem CategoryTheory.curry_obj_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) :
      ∀ {X Y : C} (f : X ⟶ Y) (Y_1 : D), ((CategoryTheory.curry.toPrefunctor.obj F).toPrefunctor.map f).app Y_1 = F.toPrefunctor.map (f, CategoryTheory.CategoryStruct.id Y_1)
      source
      @[simp]
      theorem CategoryTheory.curry_obj_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) :
      ((CategoryTheory.curry.toPrefunctor.obj F).toPrefunctor.obj X).toPrefunctor.obj Y = F.toPrefunctor.obj (X, Y)
      source
      def CategoryTheory.curry {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
      CategoryTheory.Functor (CategoryTheory.Functor (C × D) E) (CategoryTheory.Functor C (CategoryTheory.Functor D E))

      The currying functor, taking a functor (C × D) ⥤ E and producing a functor C ⥤ (D ⥤ E).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.currying_unitIso_inv_app_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C) (X : D) :
        ((CategoryTheory.currying.unitIso.inv.app X✝¹).app X✝).app X = CategoryTheory.CategoryStruct.id ((X✝¹.toPrefunctor.obj X✝).toPrefunctor.obj X)
        source
        @[simp]
        theorem CategoryTheory.currying_counitIso_hom_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor (C × D) E) (X : C × D) :
        (CategoryTheory.currying.counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj (X.1, X.2))
        source
        @[simp]
        theorem CategoryTheory.currying_inverse_map_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
        ∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.currying.inverse.toPrefunctor.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
        source
        @[simp]
        theorem CategoryTheory.currying_functor_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D) :
        (CategoryTheory.currying.functor.toPrefunctor.obj F).toPrefunctor.obj X = (F.toPrefunctor.obj X.1).toPrefunctor.obj X.2
        source
        @[simp]
        theorem CategoryTheory.currying_functor_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X : C × D} {Y : C × D} (f : X ⟶ Y) :
        (CategoryTheory.currying.functor.toPrefunctor.obj F).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((F.toPrefunctor.map f.1).app X.2) ((F.toPrefunctor.obj Y.1).toPrefunctor.map f.2)
        source
        @[simp]
        theorem CategoryTheory.currying_counitIso_inv_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor (C × D) E) (X : C × D) :
        (CategoryTheory.currying.counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.toPrefunctor.obj (X.1, X.2))
        source
        @[simp]
        theorem CategoryTheory.currying_inverse_obj_obj_obj {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) :
        ((CategoryTheory.currying.inverse.toPrefunctor.obj F).toPrefunctor.obj X).toPrefunctor.obj Y = F.toPrefunctor.obj (X, Y)
        source
        @[simp]
        theorem CategoryTheory.currying_unitIso_hom_app_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C) (X : D) :
        ((CategoryTheory.currying.unitIso.hom.app X✝¹).app X✝).app X = CategoryTheory.CategoryStruct.id ((X✝¹.toPrefunctor.obj X✝).toPrefunctor.obj X)
        source
        @[simp]
        theorem CategoryTheory.currying_inverse_obj_obj_map {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) :
        ∀ {X_1 Y : D} (g : X_1 ⟶ Y), ((CategoryTheory.currying.inverse.toPrefunctor.obj F).toPrefunctor.obj X).toPrefunctor.map g = F.toPrefunctor.map (CategoryTheory.CategoryStruct.id X, g)
        source
        @[simp]
        theorem CategoryTheory.currying_functor_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
        ∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D), (CategoryTheory.currying.functor.toPrefunctor.map T).app X_1 = (T.app X_1.1).app X_1.2
        source
        @[simp]
        theorem CategoryTheory.currying_inverse_obj_map_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) :
        ∀ {X Y : C} (f : X ⟶ Y) (Y_1 : D), ((CategoryTheory.currying.inverse.toPrefunctor.obj F).toPrefunctor.map f).app Y_1 = F.toPrefunctor.map (f, CategoryTheory.CategoryStruct.id Y_1)
        source
        def CategoryTheory.currying {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] :
        CategoryTheory.Functor C (CategoryTheory.Functor D E) ≌ CategoryTheory.Functor (C × D) E

        The equivalence of functor categories given by currying/uncurrying.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.flipIsoCurrySwapUncurry_hom_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D) (X : C) :
          ((CategoryTheory.flipIsoCurrySwapUncurry F).hom.app X✝).app X = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj X).toPrefunctor.obj X✝)
          source
          @[simp]
          theorem CategoryTheory.flipIsoCurrySwapUncurry_inv_app_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D) (X : C) :
          ((CategoryTheory.flipIsoCurrySwapUncurry F).inv.app X✝).app X = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj X).toPrefunctor.obj X✝)
          source
          def CategoryTheory.flipIsoCurrySwapUncurry {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) :
          CategoryTheory.Functor.flip F ≅ CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.Functor.comp (CategoryTheory.Prod.swap D C) (CategoryTheory.uncurry.toPrefunctor.obj F))

          F.flip is isomorphic to uncurrying F, swapping the variables, and currying.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.uncurryObjFlip_hom_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D × C) :
            (CategoryTheory.uncurryObjFlip F).hom.app X = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj X.2).toPrefunctor.obj X.1)
            source
            @[simp]
            theorem CategoryTheory.uncurryObjFlip_inv_app {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D × C) :
            (CategoryTheory.uncurryObjFlip F).inv.app X = CategoryTheory.CategoryStruct.id ((F.toPrefunctor.obj X.2).toPrefunctor.obj X.1)
            source
            def CategoryTheory.uncurryObjFlip {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) :
            CategoryTheory.uncurry.toPrefunctor.obj (CategoryTheory.Functor.flip F) ≅ CategoryTheory.Functor.comp (CategoryTheory.Prod.swap D C) (CategoryTheory.uncurry.toPrefunctor.obj F)

            The uncurrying of F.flip is isomorphic to swapping the factors followed by the uncurrying of F.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.whiskeringRight₂_map_app_app_app (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] :
              ∀ {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (f : X ⟶ Y) (X_1 : CategoryTheory.Functor B C) (Y_1 : CategoryTheory.Functor B D) (c : B), ((((CategoryTheory.whiskeringRight₂ B C D E).toPrefunctor.map f).app X_1).app Y_1).app c = (f.app (X_1.toPrefunctor.obj c)).app (Y_1.toPrefunctor.obj c)
              source
              @[simp]
              theorem CategoryTheory.whiskeringRight₂_obj_map_app_app (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) :
              ∀ {X_1 Y : CategoryTheory.Functor B C} (f : X_1 ⟶ Y) (Y_1 : CategoryTheory.Functor B D) (X_2 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).toPrefunctor.obj X).toPrefunctor.map f).app Y_1).app X_2 = (X.toPrefunctor.map (f.app X_2)).app (Y_1.toPrefunctor.obj X_2)
              source
              @[simp]
              theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_map (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) :
              ∀ {X_1 Y_1 : B} (f : X_1 ⟶ Y_1), ((((CategoryTheory.whiskeringRight₂ B C D E).toPrefunctor.obj X✝).toPrefunctor.obj X).toPrefunctor.obj Y).toPrefunctor.map f = CategoryTheory.CategoryStruct.comp ((X✝.toPrefunctor.map (X.toPrefunctor.map f)).app (Y.toPrefunctor.obj X_1)) ((X✝.toPrefunctor.obj (X.toPrefunctor.obj Y_1)).toPrefunctor.map (Y.toPrefunctor.map f))
              source
              @[simp]
              theorem CategoryTheory.whiskeringRight₂_obj_obj_map_app (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : CategoryTheory.Functor B C) :
              ∀ {X_1 Y : CategoryTheory.Functor B D} (g : X_1 ⟶ Y) (X_2 : B), ((((CategoryTheory.whiskeringRight₂ B C D E).toPrefunctor.obj X✝).toPrefunctor.obj X).toPrefunctor.map g).app X_2 = (X✝.toPrefunctor.obj (X.toPrefunctor.obj X_2)).toPrefunctor.map (g.app X_2)
              source
              @[simp]
              theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_obj (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] (X : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : CategoryTheory.Functor B C) (Y : CategoryTheory.Functor B D) (X : B) :
              ((((CategoryTheory.whiskeringRight₂ B C D E).toPrefunctor.obj X✝¹).toPrefunctor.obj X✝).toPrefunctor.obj Y).toPrefunctor.obj X = (X✝¹.toPrefunctor.obj (X✝.toPrefunctor.obj X)).toPrefunctor.obj (Y.toPrefunctor.obj X)
              source
              def CategoryTheory.whiskeringRight₂ (B : Type u₁) [CategoryTheory.Category.{v₁, u₁} B] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (D : Type u₃) [CategoryTheory.Category.{v₃, u₃} D] (E : Type u₄) [CategoryTheory.Category.{v₄, u₄} E] :
              CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E)) (CategoryTheory.Functor (CategoryTheory.Functor B C) (CategoryTheory.Functor (CategoryTheory.Functor B D) (CategoryTheory.Functor B E)))

              A version of CategoryTheory.whiskeringRight for bifunctors, obtained by uncurrying, applying whiskeringRight and currying back

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem CategoryTheory.Functor.uncurry_obj_curry_obj {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor (B × C) D) :
                CategoryTheory.uncurry.toPrefunctor.obj (CategoryTheory.curry.toPrefunctor.obj F) = F
                source
                theorem CategoryTheory.Functor.curry_obj_injective {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {F₁ : CategoryTheory.Functor (C × D) E} {F₂ : CategoryTheory.Functor (C × D) E} (h : CategoryTheory.curry.toPrefunctor.obj F₁ = CategoryTheory.curry.toPrefunctor.obj F₂) :
                F₁ = F₂
                source
                theorem CategoryTheory.Functor.curry_obj_uncurry_obj {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor B (CategoryTheory.Functor C D)) :
                CategoryTheory.curry.toPrefunctor.obj (CategoryTheory.uncurry.toPrefunctor.obj F) = F
                source
                theorem CategoryTheory.Functor.uncurry_obj_injective {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {F₁ : CategoryTheory.Functor B (CategoryTheory.Functor C D)} {F₂ : CategoryTheory.Functor B (CategoryTheory.Functor C D)} (h : CategoryTheory.uncurry.toPrefunctor.obj F₁ = CategoryTheory.uncurry.toPrefunctor.obj F₂) :
                F₁ = F₂
                source
                theorem CategoryTheory.Functor.flip_flip {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor B (CategoryTheory.Functor C D)) :
                CategoryTheory.Functor.flip (CategoryTheory.Functor.flip F) = F
                source
                theorem CategoryTheory.Functor.flip_injective {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {F₁ : CategoryTheory.Functor B (CategoryTheory.Functor C D)} {F₂ : CategoryTheory.Functor B (CategoryTheory.Functor C D)} (h : CategoryTheory.Functor.flip F₁ = CategoryTheory.Functor.flip F₂) :
                F₁ = F₂
                source
                theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {H : Type u₅} [CategoryTheory.Category.{v₅, u₅} H] (F₁ : CategoryTheory.Functor B C) (F₂ : CategoryTheory.Functor D E) (G : CategoryTheory.Functor (C × E) H) :
                CategoryTheory.uncurry.toPrefunctor.obj (CategoryTheory.Functor.flip (CategoryTheory.Functor.comp F₂ (CategoryTheory.Functor.flip (CategoryTheory.Functor.comp F₁ (CategoryTheory.curry.toPrefunctor.obj G))))) = CategoryTheory.Functor.comp (CategoryTheory.Functor.prod F₁ F₂) G
                source
                theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip' {B : Type u₁} [CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {H : Type u₅} [CategoryTheory.Category.{v₅, u₅} H] (F₁ : CategoryTheory.Functor B C) (F₂ : CategoryTheory.Functor D E) (G : CategoryTheory.Functor (C × E) H) :
                CategoryTheory.uncurry.toPrefunctor.obj (CategoryTheory.Functor.comp F₁ (CategoryTheory.Functor.flip (CategoryTheory.Functor.comp F₂ (CategoryTheory.Functor.flip (CategoryTheory.curry.toPrefunctor.obj G))))) = CategoryTheory.Functor.comp (CategoryTheory.Functor.prod F₁ F₂) G