{B : Type u} →
  {inst : Quiver B} →
    {P : Sort u_1} →
      {a b c d : CategoryTheory.FreeBicategory B} →
        {f : a ⟶ b} →
          {g : b ⟶ c} →
            {h : c ⟶ d} →
              {a' b' c' d' : CategoryTheory.FreeBicategory B} →
                {f' : a' ⟶ b'} →
                  {g' : b' ⟶ c'} →
                    {h' : c' ⟶ d'} →
                      a = a' →
                        d = d' →
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ≍
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g') h' →
                            CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ≍
                                CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h') →
                              CategoryTheory.FreeBicategory.Hom₂.associator f g h ≍
                                  CategoryTheory.FreeBicategory.Hom₂.associator f' g' h' →
                                (a ≍ a' → b ≍ b' → c ≍ c' → d ≍ d' → f ≍ f' → g ≍ g' → h ≍ h' → P) → P