prod.nonempty

Stream: general

[Kevin Buzzard]

What's the sensible proof of

example (X Y : Type) (hX : nonempty X) (hY : nonempty Y) : nonempty (X × Y) :=
begin
  tactic.unfreeze_local_instances,
  cases hX with x,
  cases hY with y,
  constructor,
  exact ⟨x,y⟩,
end

[Mario Carneiro]

example (X Y : Type) : nonempty X → nonempty Y → nonempty (X × Y)
| ⟨x⟩ ⟨y⟩ := ⟨(x, y)⟩

[Kevin Buzzard]

Should this be an instance?

[Mario Carneiro]

yes, this looks like a good instance

[Kevin Buzzard]

Should this be a class:

class bounded_above (X : set ℝ) : Prop :=
(is_bounded_above : bounded (≤) X)

[Kevin Buzzard]

I'm trying to understand the fact that a non-empty bounded-above set has a unique least upper bound.

[Kevin Buzzard]

If $X$ and $Y$ are non-empty bounded-above sets of reals then so is $X+Y$. I'm wondering if typeclass inference has any business knowing this.

[Mario Carneiro]

it's debatable, but to me it seems like much ado about one theorem

[Mario Carneiro]

sometimes I wish we could just let theorems be theorems

[Mario Carneiro]

and just use them by name like normal people instead of going to incredible lengths to make everything appear wordless

[Reid Barton]

Names are annoying, but using type classes for theorems is worse

[Kevin Buzzard]

But the name of each of these theorems is NaN

[Kevin Buzzard]

I guess I do see your point.