∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁) (f₂ : X₂.Hom Y₂) (g₁ : Y₁.Hom Z₁)
  (g₂ : Y₂.Hom Z₂), CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯