{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A B X Y : C} →
      {f : A ⟶ X} →
        {i : A ⟶ B} → {p : X ⟶ Y} → {g : B ⟶ Y} → {sq : CategoryTheory.CommSq f i p g} → sq.LiftStruct → (B ⟶ X)