Sort u →
  {C : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      {W : CategoryTheory.MorphismProperty C} →
        {X Y : C} →
          W.LeftFraction X Y →
            {C' : Type u_1} →
              [inst' : CategoryTheory.Category.{v_1, u_1} C'] →
                {W' : CategoryTheory.MorphismProperty C'} → {X' Y' : C'} → W'.LeftFraction X' Y' → Sort u