∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).hom = CategoryTheory.eqToHom ⋯