∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} (f : L.X₁ ⟶ L'.X₁)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam)
  (f_1 : L.X₁ ⟶ L'.X₁)
  (comm_1 :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f_1) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam),
  ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1)