How does one prove unit ≠ bool

Stream: general

[Slavomir Kaslev]

I'm trying to prove

def unit_ne_bool : unit ≠ bool := sorry

and hoping there's a easy proof of this.

One possible direction is to prove that unit->unit is singleton but bool->bool is not but I was hoping for something more trivial.

[Reid Barton]

I don't see how introducing these functions could help because it's presumably simpler to prove that unit is a singleton but bool is not.

[Shing Tak Lam]

(Is this to do with the Kata?)

[Shing Tak Lam]

(deleted)

[Kevin Buzzard]

yeah this might be a kata spoiler

[Slavomir Kaslev]

It's not from the kata, I needed it for this proof https://github.com/skaslev/papers/blob/94950c7b7be5278561eab639d82b391872c3e042/kan.lean#L370

(kata spoilers ahead) this is what I came up with:

def iscontr (α : Type) := ∃ x : α, ∀ y : α, x = y

def iscontr_unit : iscontr unit :=
⟨unit.star, λ y, y.rec rfl⟩

def notcontr_bool : ¬iscontr bool
| ⟨bool.ff, h⟩ := bool.no_confusion (h bool.tt)
| ⟨bool.tt, h⟩ := bool.no_confusion (h bool.ff)

def unit_ne_bool : unit ≠ bool :=
λ h, notcontr_bool (h ▸ iscontr_unit)

Is there an easier proof?

[Reid Barton]

I think it would be slightly shorter to instead use the property forall x y, x = y but otherwise I think the answer is no.

[Kevin Buzzard]

You could use the subsingleton typeclass in Lean I guess, but your proof looks pretty direct.

[Kevin Buzzard]

Another proof, if you were prepared to use mathlib machinery, would be to use the fact that both bool and unit were known to be finite types, and bool has cardinality 2 whereas unit has cardinality 1.

[Rob Lewis]

Also if you're willing to use mathlib machinery, iscontr_unit and notcontr_bool are decidable, so proved by dec_trivial.

[Mario Carneiro]

theorem unit_ne_bool : unit ≠ bool :=
have ∀ {α} (h : unit = α) a, cast h () = a,
  by intros; cases h; cases a; refl,
λ h, by cases (this h tt).symm.trans (this h ff)