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).

This is used in CategoryTheory.Category.Cat.CartesianClosed to equip the category of small categories Cat.{u, u} with a cartesian closed structure.

source
def CategoryTheory.Functor.uncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
Functor (Functor C (Functor D E)) (Functor (C × D) E)

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

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

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

      Equations
        Instances For
          source
          def CategoryTheory.Functor.curry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
          Functor (Functor (C × D) E) (Functor C (Functor D E))

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

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.curry_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) :
              ((curry.obj F).map f).app Y = F.map (f, CategoryStruct.id Y)
              source
              @[simp]
              theorem CategoryTheory.Functor.curry_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor (C × D) E} (T : X✝ ⟶ Y✝) (X : C) (Y : D) :
              ((curry.map T).app X).app Y = T.app (X, Y)
              source
              @[simp]
              theorem CategoryTheory.Functor.curry_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) (Y : D) :
              ((curry.obj F).obj X).obj Y = F.obj (X, Y)
              source
              @[simp]
              theorem CategoryTheory.Functor.curry_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) :
              ((curry.obj F).obj X).map g = F.map (CategoryStruct.id X, g)
              source
              def CategoryTheory.Functor.currying {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
              Functor C (Functor D E) ≌ Functor (C × D) E

              The equivalence of functor categories given by currying/uncurrying.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_inverse_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) :
                  ((currying.inverse.obj F).obj X).map g = F.map (CategoryStruct.id X, g)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_functor_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) :
                  (currying.functor.obj F).obj X = (F.obj X.1).obj X.2
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_counitIso_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor (C × D) E) (X✝ : C × D) :
                  (currying.counitIso.hom.app X).app X✝ = CategoryStruct.id (X.obj (X✝.1, X✝.2))
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_inverse_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) :
                  ((currying.inverse.obj F).map f).app Y = F.map (f, CategoryStruct.id Y)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_inverse_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor (C × D) E} (T : X✝ ⟶ Y✝) (X : C) (Y : D) :
                  ((currying.inverse.map T).app X).app Y = T.app (X, Y)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_functor_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X ⟶ Y) :
                  (currying.functor.obj F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_inverse_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × D) E) (X : C) (Y : D) :
                  ((currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_functor_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (T : X✝ ⟶ Y✝) (X : C × D) :
                  (currying.functor.map T).app X = (T.app X.1).app X.2
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_unitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝ : D) :
                  ((currying.unitIso.inv.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_unitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝ : D) :
                  ((currying.unitIso.hom.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.currying_counitIso_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor (C × D) E) (X✝ : C × D) :
                  (currying.counitIso.inv.app X).app X✝ = CategoryStruct.id (X.obj (X✝.1, X✝.2))
                  source
                  def CategoryTheory.Functor.flipping {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                  Functor C (Functor D E) ≌ Functor D (Functor C E)

                  The equivalence of functor categories given by flipping.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_unitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝ : D) :
                      ((flipping.unitIso.inv.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_functor_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                      ((flipping.functor.obj F).obj k).map f = (F.map f).app k
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_inverse_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) (j : D) :
                      ((flipping.inverse.obj F).obj k).obj j = (F.obj j).obj k
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_functor_obj_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) (j : C) :
                      ((flipping.functor.obj F).obj k).obj j = (F.obj j).obj k
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_functor_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor C (Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) :
                      ((flipping.functor.map φ).app Y).app X = (φ.app X).app Y
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_unitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : C) (X✝ : D) :
                      ((flipping.unitIso.hom.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_functor_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) :
                      ((flipping.functor.obj F).map f).app j = (F.obj j).map f
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_inverse_obj_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
                      ((flipping.inverse.obj F).obj k).map f = (F.map f).app k
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_counitIso_inv_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor D (Functor C E)) (X✝ : D) (X✝ : C) :
                      ((flipping.counitIso.inv.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_inverse_map_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor D (Functor C E)} (φ : F₁ ⟶ F₂) (Y : C) (X : D) :
                      ((flipping.inverse.map φ).app Y).app X = (φ.app X).app Y
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_counitIso_hom_app_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (X : Functor D (Functor C E)) (X✝ : D) (X✝ : C) :
                      ((flipping.counitIso.hom.app X).app X✝).app X✝ = CategoryStruct.id ((X.obj X✝).obj X✝)
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.flipping_inverse_obj_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) :
                      ((flipping.inverse.obj F).map f).app j = (F.obj j).map f
                      source
                      def CategoryTheory.Functor.fullyFaithfulUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                      uncurry.FullyFaithful

                      The functor uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E is fully faithful.

                      Equations
                        Instances For
                          source
                          instance CategoryTheory.Functor.instFullProdUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                          uncurry.Full
                          source
                          instance CategoryTheory.Functor.instFaithfulProdUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                          uncurry.Faithful
                          source
                          def CategoryTheory.Functor.curryObjProdComp {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{u_3, u_1} C'] [Category.{u_4, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) :
                          curry.obj ((F₁.prod F₂).comp G) ≅ F₁.comp ((curry.obj G).comp ((whiskeringLeft C' D' E).obj F₂))

                          Given functors F₁ : C ⥤ D, F₂ : C' ⥤ D' and G : D × D' ⥤ E, this is the isomorphism between curry.obj ((F₁.prod F₂).comp G) and F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ in the category C ⥤ C' ⥤ E.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryObjProdComp_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{u_3, u_1} C'] [Category.{u_4, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) (X : C) (X✝ : C') :
                              ((F₁.curryObjProdComp F₂ G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))
                              source
                              @[simp]
                              theorem CategoryTheory.Functor.curryObjProdComp_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {C' : Type u_1} {D' : Type u_2} [Category.{u_3, u_1} C'] [Category.{u_4, u_2} D'] (F₁ : Functor C D) (F₂ : Functor C' D') (G : Functor (D × D') E) (X : C) (X✝ : C') :
                              ((F₁.curryObjProdComp F₂ G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X✝))
                              source
                              def CategoryTheory.Functor.flipIsoCurrySwapUncurry {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) :
                              F.flip ≅ curry.obj ((Prod.swap D C).comp (uncurry.obj F))

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

                              Equations
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.flipIsoCurrySwapUncurry_inv_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D) (X✝ : C) :
                                  (F.flipIsoCurrySwapUncurry.inv.app X).app X✝ = CategoryStruct.id ((F.obj X✝).obj X)
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Functor.flipIsoCurrySwapUncurry_hom_app_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D) (X✝ : C) :
                                  (F.flipIsoCurrySwapUncurry.hom.app X).app X✝ = CategoryStruct.id ((F.obj X✝).obj X)
                                  source
                                  def CategoryTheory.Functor.uncurryObjFlip {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) :
                                  uncurry.obj F.flip ≅ (Prod.swap D C).comp (uncurry.obj F)

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

                                  Equations
                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.uncurryObjFlip_inv_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D × C) :
                                      F.uncurryObjFlip.inv.app X = CategoryStruct.id ((F.obj X.2).obj X.1)
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.uncurryObjFlip_hom_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : D × C) :
                                      F.uncurryObjFlip.hom.app X = CategoryStruct.id ((F.obj X.2).obj X.1)
                                      source
                                      def CategoryTheory.Functor.whiskeringRight₂ (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] :
                                      Functor (Functor C (Functor D E)) (Functor (Functor B C) (Functor (Functor B D) (Functor B E)))

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

                                      Equations
                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.whiskeringRight₂_obj_map_app_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) {X✝ Y✝ : Functor B C} (f : X✝ ⟶ Y✝) (Y : Functor B D) (X✝¹ : B) :
                                          ((((whiskeringRight₂ B C D E).obj X).map f).app Y).app X✝¹ = (X.map (f.app X✝¹)).app (Y.obj X✝¹)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.whiskeringRight₂_obj_obj_map_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) {X✝¹ Y✝ : Functor B D} (g : X✝¹ ⟶ Y✝) (X✝ : B) :
                                          ((((whiskeringRight₂ B C D E).obj X).obj X✝).map g).app X✝ = (X.obj (X✝.obj X✝)).map (g.app X✝)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.whiskeringRight₂_map_app_app_app (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] {X✝ Y✝ : Functor C (Functor D E)} (f : X✝ ⟶ Y✝) (X : Functor B C) (Y : Functor B D) (c : B) :
                                          ((((whiskeringRight₂ B C D E).map f).app X).app Y).app c = (f.app (X.obj c)).app (Y.obj c)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.whiskeringRight₂_obj_obj_obj_obj (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) (Y : Functor B D) (X✝ : B) :
                                          ((((whiskeringRight₂ B C D E).obj X).obj X✝).obj Y).obj X✝ = (X.obj (X✝.obj X✝)).obj (Y.obj X✝)
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.whiskeringRight₂_obj_obj_obj_map (B : Type u₁) [Category.{v₁, u₁} B] (C : Type u₂) [Category.{v₂, u₂} C] (D : Type u₃) [Category.{v₃, u₃} D] (E : Type u₄) [Category.{v₄, u₄} E] (X : Functor C (Functor D E)) (X✝ : Functor B C) (Y : Functor B D) {X✝¹ Y✝ : B} (f : X✝¹ ⟶ Y✝) :
                                          ((((whiskeringRight₂ B C D E).obj X).obj X✝).obj Y).map f = CategoryStruct.comp ((X.map (X✝.map f)).app (Y.obj X✝¹)) ((X.obj (X✝.obj Y✝)).map (Y.map f))
                                          source
                                          theorem CategoryTheory.Functor.uncurry_obj_curry_obj {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor (B × C) D) :
                                          uncurry.obj (curry.obj F) = F
                                          source
                                          theorem CategoryTheory.Functor.curry_obj_injective {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {F₁ F₂ : Functor (C × D) E} (h : curry.obj F₁ = curry.obj F₂) :
                                          F₁ = F₂
                                          source
                                          theorem CategoryTheory.Functor.curry_obj_uncurry_obj {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor B (Functor C D)) :
                                          curry.obj (uncurry.obj F) = F
                                          source
                                          theorem CategoryTheory.Functor.uncurry_obj_injective {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {F₁ F₂ : Functor B (Functor C D)} (h : uncurry.obj F₁ = uncurry.obj F₂) :
                                          F₁ = F₂
                                          source
                                          theorem CategoryTheory.Functor.flip_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] (F : Functor B (Functor C D)) :
                                          F.flip.flip = F
                                          source
                                          theorem CategoryTheory.Functor.flip_injective {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {F₁ F₂ : Functor B (Functor C D)} (h : F₁.flip = F₂.flip) :
                                          F₁ = F₂
                                          source
                                          theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {H : Type u₅} [Category.{v₅, u₅} H] (F₁ : Functor B C) (F₂ : Functor D E) (G : Functor (C × E) H) :
                                          uncurry.obj (F₂.comp (F₁.comp (curry.obj G)).flip).flip = (F₁.prod F₂).comp G
                                          source
                                          theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip' {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] {H : Type u₅} [Category.{v₅, u₅} H] (F₁ : Functor B C) (F₂ : Functor D E) (G : Functor (C × E) H) :
                                          uncurry.obj (F₁.comp (F₂.comp (curry.obj G).flip).flip) = (F₁.prod F₂).comp G
                                          source
                                          def CategoryTheory.Functor.compFlipUncurryIso {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) :
                                          uncurry.obj (F.comp G).flip ≅ ((Functor.id C).prod F).comp (uncurry.obj G.flip)

                                          Natural isomorphism witnessing comp_flip_uncurry_eq.

                                          Equations
                                            Instances For
                                              source
                                              @[simp]
                                              theorem CategoryTheory.Functor.compFlipUncurryIso_inv_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) (X : C × B) :
                                              (F.compFlipUncurryIso G).inv.app X = CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)
                                              source
                                              @[simp]
                                              theorem CategoryTheory.Functor.compFlipUncurryIso_hom_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) (X : C × B) :
                                              (F.compFlipUncurryIso G).hom.app X = CategoryStruct.id ((G.obj (F.obj X.2)).obj X.1)
                                              source
                                              theorem CategoryTheory.Functor.comp_flip_uncurry_eq {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor B D) (G : Functor D (Functor C E)) :
                                              uncurry.obj (F.comp G).flip = ((Functor.id C).prod F).comp (uncurry.obj G.flip)
                                              source
                                              def CategoryTheory.Functor.curryObjCompIso {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) :
                                              (curry.obj (F.comp G)).flip ≅ (curry.obj F).flip.comp ((whiskeringRight C D E).obj G)

                                              Natural isomorphism witnessing comp_flip_curry_eq.

                                              Equations
                                                Instances For
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.curryObjCompIso_inv_app_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) (X : B) (X✝ : C) :
                                                  ((F.curryObjCompIso G).inv.app X).app X✝ = CategoryStruct.id (G.obj (F.obj (X✝, X)))
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.curryObjCompIso_hom_app_app {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) (X : B) (X✝ : C) :
                                                  ((F.curryObjCompIso G).hom.app X).app X✝ = CategoryStruct.id (G.obj (F.obj (X✝, X)))
                                                  source
                                                  theorem CategoryTheory.Functor.curry_obj_comp_flip {B : Type u₁} [Category.{v₁, u₁} B] {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor (C × B) D) (G : Functor D E) :
                                                  (curry.obj (F.comp G)).flip = (curry.obj F).flip.comp ((whiskeringRight C D E).obj G)
                                                  source
                                                  def CategoryTheory.Functor.flippingEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                                                  Functor C (Functor D E) ≃ Functor D (Functor C E)

                                                  The equivalence of types of bifunctors giving by flipping the arguments.

                                                  Equations
                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.flippingEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
                                                      ((flippingEquiv.symm F).obj k).map f = (F.map f).app k
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.flippingEquiv_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                                                      ((flippingEquiv F).obj k).map f = (F.map f).app k
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.flippingEquiv_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (k : D) (j : C) :
                                                      ((flippingEquiv F).obj k).obj j = (F.obj j).obj k
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.flippingEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) (k : C) (j : D) :
                                                      ((flippingEquiv.symm F).obj k).obj j = (F.obj j).obj k
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.flippingEquiv_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) :
                                                      ((flippingEquiv F).map f).app j = (F.obj j).map f
                                                      source
                                                      @[simp]
                                                      theorem CategoryTheory.Functor.flippingEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor D (Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) :
                                                      ((flippingEquiv.symm F).map f).app j = (F.obj j).map f
                                                      source
                                                      def CategoryTheory.Functor.curryingEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                                                      Functor C (Functor D E) ≃ Functor (C × D) E

                                                      The equivalence of types of bifunctors given by currying.

                                                      Equations
                                                        Instances For
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.curryingEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) :
                                                          ((curryingEquiv.symm G).obj X).map g = G.map (CategoryStruct.id X, g)
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.curryingEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) :
                                                          ((curryingEquiv.symm G).map f).app Y = G.map (f, CategoryStruct.id Y)
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.curryingEquiv_apply_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) {X Y : C × D} (f : X ⟶ Y) :
                                                          (curryingEquiv F).map f = CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.curryingEquiv_apply_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (F : Functor C (Functor D E)) (X : C × D) :
                                                          (curryingEquiv F).obj X = (F.obj X.1).obj X.2
                                                          source
                                                          @[simp]
                                                          theorem CategoryTheory.Functor.curryingEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (G : Functor (C × D) E) (X : C) (Y : D) :
                                                          ((curryingEquiv.symm G).obj X).obj Y = G.obj (X, Y)
                                                          source
                                                          def CategoryTheory.Functor.curryingFlipEquiv {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] :
                                                          Functor D (Functor C E) ≃ Functor (C × D) E

                                                          The flipped equivalence of types of bifunctors given by currying.

                                                          Equations
                                                            Instances For
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.curryingFlipEquiv_apply_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor D (Functor C E)) (X : C × D) :
                                                              (curryingFlipEquiv a✝).obj X = (a✝.obj X.2).obj X.1
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_obj {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) (k : D) (j : C) :
                                                              ((curryingFlipEquiv.symm a✝).obj k).obj j = a✝.obj (j, k)
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_map_app {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) :
                                                              ((curryingFlipEquiv.symm a✝).map f).app j = a✝.map (CategoryStruct.id j, f)
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.curryingFlipEquiv_symm_apply_obj_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor (C × D) E) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
                                                              ((curryingFlipEquiv.symm a✝).obj k).map f = a✝.map (f, CategoryStruct.id k)
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.Functor.curryingFlipEquiv_apply_map {C : Type u₂} [Category.{v₂, u₂} C] {D : Type u₃} [Category.{v₃, u₃} D] {E : Type u₄} [Category.{v₄, u₄} E] (a✝ : Functor D (Functor C E)) {X Y : C × D} (f : X ⟶ Y) :
                                                              (curryingFlipEquiv a✝).map f = CategoryStruct.comp ((a✝.map f.2).app X.1) ((a✝.obj Y.2).map f.1)