-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
Goal:
X X' Y Y' Z : Truncated 2
x₀ x₁ x₂ :
  X.obj
    (Opposite.op
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
w :
  ∀ (y : Y.HomotopyCategory),
    Eq (α :=
      Quiver.Hom (V := (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
        (Functor.obj
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (lift
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    mk (x, y))
                  (fun
                      {y₀ y₁ :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))}
                      (e : Edge y₀ y₁) ↦
                    homMk ((Edge.id x).tensor e))
                  ⋯ ⋯ :
                Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
            x₀)
          y)
        (Functor.obj
          ((fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (lift
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    mk (x, y))
                  (fun
                      {y₀ y₁ :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))}
                      (e : Edge y₀ y₁) ↦
                    homMk ((Edge.id x).tensor e))
                  ⋯ ⋯ :
                Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
            x₂)
          y))
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          (fun
                (x :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              (lift
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    mk (x, y))
                  (fun
                      {y₀ y₁ :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))}
                      (e : Edge y₀ y₁) ↦
                    homMk ((Edge.id x).tensor e))
                  ⋯ ⋯ :
                Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
            x₁)
          ((fun
                {x₀ x₁ :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))}
                (e : Edge x₀ x₁) ↦
              (mkNatTrans
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    homMk (e.tensor (Edge.id y)))
                  ⋯ :
                Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₀)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₁)))
            e₀₁)
          ((fun
                {x₀ x₁ :
                  X.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))}
                (e : Edge x₀ x₁) ↦
              (mkNatTrans
                  (fun
                      (y :
                        Y.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    homMk (e.tensor (Edge.id y)))
                  ⋯ :
                Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₀)
                  ((fun
                        (x :
                          X.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      (lift
                          (fun
                              (y :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))) ↦
                            mk (x, y))
                          (fun
                              {y₀ y₁ :
                                Y.obj
                                  (Opposite.op
                                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                      OneTruncation₂._proof_1))}
                              (e : Edge y₀ y₁) ↦
                            homMk ((Edge.id x).tensor e))
                          ⋯ ⋯ :
                        Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                    x₁)))
            e₁₂))
        y)
      (NatTrans.app
        ((fun
              {x₀ x₁ :
                X.obj
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      OneTruncation₂._proof_1))}
              (e : Edge x₀ x₁) ↦
            (mkNatTrans
                (fun
                    (y :
                      Y.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  homMk (e.tensor (Edge.id y)))
                ⋯ :
              Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₀)
                ((fun
                      (x :
                        X.obj
                          (Opposite.op
                            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                              OneTruncation₂._proof_1))) ↦
                    (lift
                        (fun
                            (y :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))) ↦
                          mk (x, y))
                        (fun
                            {y₀ y₁ :
                              Y.obj
                                (Opposite.op
                                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                    OneTruncation₂._proof_1))}
                            (e : Edge y₀ y₁) ↦
                          homMk ((Edge.id x).tensor e))
                        ⋯ ⋯ :
                      Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                  x₁)))
          e₀₂)
        y)
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
      ((fun
            (x :
              X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          (lift
              (fun
                  (y :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                mk (x, y))
              (fun
                  {y₀ y₁ :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))}
                  (e : Edge y₀ y₁) ↦
                homMk ((Edge.id x).tensor e))
              ⋯ ⋯ :
            Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
        x₀)
      ((fun
            (x :
              X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          (lift
              (fun
                  (y :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                mk (x, y))
              (fun
                  {y₀ y₁ :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))}
                  (e : Edge y₀ y₁) ↦
                homMk ((Edge.id x).tensor e))
              ⋯ ⋯ :
            Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
        x₂))
    (CategoryStruct.comp (Y :=
      (fun
            (x :
              X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))) ↦
          (lift
              (fun
                  (y :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                mk (x, y))
              (fun
                  {y₀ y₁ :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))}
                  (e : Edge y₀ y₁) ↦
                homMk ((Edge.id x).tensor e))
              ⋯ ⋯ :
            Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
        x₁)
      ((fun
            {x₀ x₁ :
              X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))}
            (e : Edge x₀ x₁) ↦
          (mkNatTrans
              (fun
                  (y :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                homMk (e.tensor (Edge.id y)))
              ⋯ :
            Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (lift
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mk (x, y))
                      (fun
                          {y₀ y₁ :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))}
                          (e : Edge y₀ y₁) ↦
                        homMk ((Edge.id x).tensor e))
                      ⋯ ⋯ :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₀)
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (lift
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mk (x, y))
                      (fun
                          {y₀ y₁ :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))}
                          (e : Edge y₀ y₁) ↦
                        homMk ((Edge.id x).tensor e))
                      ⋯ ⋯ :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₁)))
        e₀₁)
      ((fun
            {x₀ x₁ :
              X.obj
                (Opposite.op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    OneTruncation₂._proof_1))}
            (e : Edge x₀ x₁) ↦
          (mkNatTrans
              (fun
                  (y :
                    Y.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                homMk (e.tensor (Edge.id y)))
              ⋯ :
            Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (lift
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mk (x, y))
                      (fun
                          {y₀ y₁ :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))}
                          (e : Edge y₀ y₁) ↦
                        homMk ((Edge.id x).tensor e))
                      ⋯ ⋯ :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₀)
              ((fun
                    (x :
                      X.obj
                        (Opposite.op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            OneTruncation₂._proof_1))) ↦
                  (lift
                      (fun
                          (y :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))) ↦
                        mk (x, y))
                      (fun
                          {y₀ y₁ :
                            Y.obj
                              (Opposite.op
                                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                  OneTruncation₂._proof_1))}
                          (e : Edge y₀ y₁) ↦
                        homMk ((Edge.id x).tensor e))
                      ⋯ ⋯ :
                    Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
                x₁)))
        e₁₂))
    ((fun
          {x₀ x₁ :
            X.obj
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                  OneTruncation₂._proof_1))}
          (e : Edge x₀ x₁) ↦
        (mkNatTrans
            (fun
                (y :
                  Y.obj
                    (Opposite.op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        OneTruncation₂._proof_1))) ↦
              homMk (e.tensor (Edge.id y)))
            ⋯ :
          Quiver.Hom (V := Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory)
            ((fun
                  (x :
                    X.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (lift
                    (fun
                        (y :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      mk (x, y))
                    (fun
                        {y₀ y₁ :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))}
                        (e : Edge y₀ y₁) ↦
                      homMk ((Edge.id x).tensor e))
                    ⋯ ⋯ :
                  Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
              x₀)
            ((fun
                  (x :
                    X.obj
                      (Opposite.op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          OneTruncation₂._proof_1))) ↦
                (lift
                    (fun
                        (y :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))) ↦
                      mk (x, y))
                    (fun
                        {y₀ y₁ :
                          Y.obj
                            (Opposite.op
                              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                                OneTruncation₂._proof_1))}
                        (e : Edge y₀ y₁) ↦
                      homMk ((Edge.id x).tensor e))
                    ⋯ ⋯ :
                  Y.HomotopyCategory ⥤ (tensorObj (𝒞 := Functor.category) X Y).HomotopyCategory))
              x₁)))
      e₀₂)

Tactic:
ext y