{B : Type u} →
  [inst : Quiver B] →
    {motive :
        {a b : CategoryTheory.FreeBicategory B} →
          (a_1 a_2 : a ⟶ b) → CategoryTheory.FreeBicategory.Hom₂ a_1 a_2 → Sort u_1} →
      {a b : CategoryTheory.FreeBicategory B} →
        {a_1 a_2 : a ⟶ b} →
          (t : CategoryTheory.FreeBicategory.Hom₂ a_1 a_2) →
            ({a b : CategoryTheory.FreeBicategory B} →
                (f : a ⟶ b) → motive f f (CategoryTheory.FreeBicategory.Hom₂.id f)) →
              ({a b : CategoryTheory.FreeBicategory B} →
                  {f g h : a ⟶ b} →
                    (η : CategoryTheory.FreeBicategory.Hom₂ f g) →
                      (θ : CategoryTheory.FreeBicategory.Hom₂ g h) →
                        motive f g η → motive g h θ → motive f h (η.vcomp θ)) →
                ({a b c : CategoryTheory.FreeBicategory B} →
                    (f : a ⟶ b) →
                      {g h : b ⟶ c} →
                        (η : CategoryTheory.FreeBicategory.Hom₂ g h) →
                          motive g h η →
                            motive (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f h)
                              (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η)) →
                  ({a b c : CategoryTheory.FreeBicategory B} →
                      {f g : a ⟶ b} →
                        (h : b ⟶ c) →
                          (η : CategoryTheory.FreeBicategory.Hom₂ f g) →
                            motive f g η →
                              motive (CategoryTheory.FreeBicategory.Hom.comp f h)
                                (CategoryTheory.FreeBicategory.Hom.comp g h)
                                (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η)) →
                    ({a b c d : CategoryTheory.FreeBicategory B} →
                        (f : a ⟶ b) →
                          (g : b ⟶ c) →
                            (h : c ⟶ d) →
                              motive (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
                                (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
                                (CategoryTheory.FreeBicategory.Hom₂.associator f g h)) →
                      ({a b c d : CategoryTheory.FreeBicategory B} →
                          (f : a ⟶ b) →
                            (g : b ⟶ c) →
                              (h : c ⟶ d) →
                                motive (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
                                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
                                  (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h)) →
                        ({a b : CategoryTheory.FreeBicategory B} →
                            (f : a ⟶ b) →
                              motive (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) f
                                (CategoryTheory.FreeBicategory.Hom₂.right_unitor f)) →
                          ({a b : CategoryTheory.FreeBicategory B} →
                              (f : a ⟶ b) →
                                motive f (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))
                                  (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f)) →
                            ({a b : CategoryTheory.FreeBicategory B} →
                                (f : a ⟶ b) →
                                  motive (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) f
                                    (CategoryTheory.FreeBicategory.Hom₂.left_unitor f)) →
                              ({a b : CategoryTheory.FreeBicategory B} →
                                  (f : a ⟶ b) →
                                    motive f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)
                                      (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f)) →
                                motive a_1 a_2 t