{α : Type u} →
  [toLinearPreorderPackage : Std.LinearPreorderPackage α] →
    (∀ (a b : α), a ≤ b → b ≤ a → a = b) →
      [toMin : Min α] →
        [toMax : Max α] →
          [toLawfulOrderMin : Std.LawfulOrderMin α] →
            [toLawfulOrderMax : Std.LawfulOrderMax α] → Std.LinearOrderPackage α