∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₂} D] (_F _F_1 : C → D),
  _F = _F_1 →
    ∀ (_P _P_1 : CategoryTheory.MorphismProperty D) (e__P : _P = _P_1) [inst_1 : _P.IsMultiplicative],
      CategoryTheory.InducedWideCategory D _F _P = CategoryTheory.InducedWideCategory D _F_1 _P_1