Documentation

Mathlib.CategoryTheory.Functor.Trifunctor

Trifunctors obtained by composition of bifunctors #

Given two bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄, we define the trifunctor bifunctorComp₁₂ F₁₂ G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends three objects X₁ : C₁, X₂ : C₂ and X₃ : C₃ to G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃.

Similarly, given two bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃, we define the trifunctor bifunctorComp₂₃ F G₂₃ : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends three objects X₁ : C₁, X₂ : C₂ and X₃ : C₃ to (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃).

source
def CategoryTheory.bifunctorComp₁₂Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) (X₁ : C₁) :
Functor C₂ (Functor C₃ C₄)

Auxiliary definition for bifunctorComp₁₂.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.bifunctorComp₁₂Obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) (X₁ : C₁) {X₂ Y₂ : C₂} (φ : X₂ ⟶ Y₂) (X₃ : C₃) :
    ((bifunctorComp₁₂Obj F₁₂ G X₁).map φ).app X₃ = (G.map ((F₁₂.obj X₁).map φ)).app X₃
    source
    @[simp]
    theorem CategoryTheory.bifunctorComp₁₂Obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
    ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).obj X₃ = (G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃
    source
    @[simp]
    theorem CategoryTheory.bifunctorComp₁₂Obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) {x✝ x✝¹ : C₃} (φ : x✝ ⟶ x✝¹) :
    ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).map φ = (G.obj ((F₁₂.obj X₁).obj X₂)).map φ
    source
    def CategoryTheory.bifunctorComp₁₂ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) :
    Functor C₁ (Functor C₂ (Functor C₃ C₄))

    Given two bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄, this is the trifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ obtained by composition.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.bifunctorComp₁₂_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) {X₁ Y₁ : C₁} (φ : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃) :
      (((bifunctorComp₁₂ F₁₂ G).map φ).app X₂).app X₃ = (G.map ((F₁₂.map φ).app X₂)).app X₃
      source
      @[simp]
      theorem CategoryTheory.bifunctorComp₁₂_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) (X₁ : C₁) :
      (bifunctorComp₁₂ F₁₂ G).obj X₁ = bifunctorComp₁₂Obj F₁₂ G X₁
      source
      def CategoryTheory.bifunctorComp₁₂FunctorObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) :
      Functor (Functor C₁₂ (Functor C₃ C₄)) (Functor C₁ (Functor C₂ (Functor C₃ C₄)))

      Auxiliary definition for bifunctorComp₁₂Functor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.bifunctorComp₁₂FunctorObj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ C₄)) :
        (bifunctorComp₁₂FunctorObj F₁₂).obj G = bifunctorComp₁₂ F₁₂ G
        source
        @[simp]
        theorem CategoryTheory.bifunctorComp₁₂FunctorObj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) {G G' : Functor C₁₂ (Functor C₃ C₄)} (φ : G ⟶ G') (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
        ((((bifunctorComp₁₂FunctorObj F₁₂).map φ).app X₁).app X₂).app X₃ = (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃
        source
        def CategoryTheory.bifunctorComp₁₂FunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] {F₁₂ F₁₂' : Functor C₁ (Functor C₂ C₁₂)} (φ : F₁₂ ⟶ F₁₂') :
        bifunctorComp₁₂FunctorObj F₁₂ ⟶ bifunctorComp₁₂FunctorObj F₁₂'

        Auxiliary definition for bifunctorComp₁₂Functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.bifunctorComp₁₂FunctorMap_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] {F₁₂ F₁₂' : Functor C₁ (Functor C₂ C₁₂)} (φ : F₁₂ ⟶ F₁₂') (G : Functor C₁₂ (Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
          ((((bifunctorComp₁₂FunctorMap φ).app G).app X₁).app X₂).app X₃ = (G.map ((φ.app X₁).app X₂)).app X₃
          source
          def CategoryTheory.bifunctorComp₁₂Functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] :
          Functor (Functor C₁ (Functor C₂ C₁₂)) (Functor (Functor C₁₂ (Functor C₃ C₄)) (Functor C₁ (Functor C₂ (Functor C₃ C₄))))

          The functor (C₁ ⥤ C₂ ⥤ C₁₂) ⥤ (C₁₂ ⥤ C₃ ⥤ C₄) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄ to the functor bifunctorComp₁₂ F₁₂ G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.bifunctorComp₁₂Functor_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] {X✝ Y✝ : Functor C₁ (Functor C₂ C₁₂)} (φ : X✝ ⟶ Y✝) :
            bifunctorComp₁₂Functor.map φ = bifunctorComp₁₂FunctorMap φ
            source
            @[simp]
            theorem CategoryTheory.bifunctorComp₁₂Functor_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_5} C₁₂] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) :
            bifunctorComp₁₂Functor.obj F₁₂ = bifunctorComp₁₂FunctorObj F₁₂
            source
            def CategoryTheory.bifunctorComp₂₃Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X₁ : C₁) :
            Functor C₂ (Functor C₃ C₄)

            Auxiliary definition for bifunctorComp₂₃.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.bifunctorComp₂₃Obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) {X✝ Y✝ : C₃} (φ : X✝ ⟶ Y✝) :
              ((bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).map φ = (F.obj X₁).map ((G₂₃.obj X₂).map φ)
              source
              @[simp]
              theorem CategoryTheory.bifunctorComp₂₃Obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
              ((bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).obj X₃ = (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃)
              source
              @[simp]
              theorem CategoryTheory.bifunctorComp₂₃Obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X₁ : C₁) {X₂ Y₂ : C₂} (φ : X₂ ⟶ Y₂) (X₃ : C₃) :
              ((bifunctorComp₂₃Obj F G₂₃ X₁).map φ).app X₃ = (F.obj X₁).map ((G₂₃.map φ).app X₃)
              source
              def CategoryTheory.bifunctorComp₂₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) :
              Functor C₁ (Functor C₂ (Functor C₃ C₄))

              Given two bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₄, this is the trifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ obtained by composition.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.bifunctorComp₂₃_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) {X₁ Y₁ : C₁} (φ : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃) :
                (((bifunctorComp₂₃ F G₂₃).map φ).app X₂).app X₃ = (F.map φ).app ((G₂₃.obj X₂).obj X₃)
                source
                @[simp]
                theorem CategoryTheory.bifunctorComp₂₃_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X₁ : C₁) :
                (bifunctorComp₂₃ F G₂₃).obj X₁ = bifunctorComp₂₃Obj F G₂₃ X₁
                source
                def CategoryTheory.bifunctorComp₂₃FunctorObj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) :
                Functor (Functor C₂ (Functor C₃ C₂₃)) (Functor C₁ (Functor C₂ (Functor C₃ C₄)))

                Auxiliary definition for bifunctorComp₂₃Functor.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.bifunctorComp₂₃FunctorObj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) :
                  (bifunctorComp₂₃FunctorObj F).obj G₂₃ = bifunctorComp₂₃ F G₂₃
                  source
                  @[simp]
                  theorem CategoryTheory.bifunctorComp₂₃FunctorObj_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) {G₂₃ G₂₃' : Functor C₂ (Functor C₃ C₂₃)} (φ : G₂₃ ⟶ G₂₃') (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
                  ((((bifunctorComp₂₃FunctorObj F).map φ).app X₁).app X₂).app X₃ = (F.obj X₁).map ((φ.app X₂).app X₃)
                  source
                  def CategoryTheory.bifunctorComp₂₃FunctorMap {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] {F F' : Functor C₁ (Functor C₂₃ C₄)} (φ : F ⟶ F') :
                  bifunctorComp₂₃FunctorObj F ⟶ bifunctorComp₂₃FunctorObj F'

                  Auxiliary definition for bifunctorComp₂₃Functor.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.bifunctorComp₂₃FunctorMap_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] {F F' : Functor C₁ (Functor C₂₃ C₄)} (φ : F ⟶ F') (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
                    ((((bifunctorComp₂₃FunctorMap φ).app G₂₃).app X₁).app X₂).app X₃ = (φ.app X₁).app ((G₂₃.obj X₂).obj X₃)
                    source
                    def CategoryTheory.bifunctorComp₂₃Functor {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] :
                    Functor (Functor C₁ (Functor C₂₃ C₄)) (Functor (Functor C₂ (Functor C₃ C₂₃)) (Functor C₁ (Functor C₂ (Functor C₃ C₄))))

                    The functor (C₁ ⥤ C₂₃ ⥤ C₄) ⥤ (C₂ ⥤ C₃ ⥤ C₂₃) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃ to the functor bifunctorComp₂₃ F G₂₃ : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.bifunctorComp₂₃Functor_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] (F : Functor C₁ (Functor C₂₃ C₄)) :
                      bifunctorComp₂₃Functor.obj F = bifunctorComp₂₃FunctorObj F
                      source
                      @[simp]
                      theorem CategoryTheory.bifunctorComp₂₃Functor_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [Category.{u_7, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_9, u_3} C₃] [Category.{u_10, u_4} C₄] [Category.{u_11, u_6} C₂₃] {X✝ Y✝ : Functor C₁ (Functor C₂₃ C₄)} (φ : X✝ ⟶ Y✝) :
                      bifunctorComp₂₃Functor.map φ = bifunctorComp₂₃FunctorMap φ