{C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {motive : (C ≌ D) → Sort u} →
          (t : C ≌ D) →
            ((functor : CategoryTheory.Functor C D) →
                (inverse : CategoryTheory.Functor D C) →
                  (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) →
                    (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) →
                      (functor_unitIso_comp :
                          ∀ (X : C),
                            CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X))
                                (counitIso.hom.app (functor.obj X)) =
                              CategoryTheory.CategoryStruct.id (functor.obj X)) →
                        motive
                          { functor := functor, inverse := inverse, unitIso := unitIso, counitIso := counitIso,
                            functor_unitIso_comp := functor_unitIso_comp }) →
              motive t