# Zulip Chat Archive

## Stream: general

### Topic: How does one prove unit ≠ bool

#### Slavomir Kaslev (Apr 23 2020 at 13:11):

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 (Apr 23 2020 at 13:14):

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 (Apr 23 2020 at 13:17):

(Is this to do with the Kata?)

#### Shing Tak Lam (Apr 23 2020 at 13:27):

(deleted)

#### Kevin Buzzard (Apr 23 2020 at 13:28):

yeah this might be a kata spoiler

#### Slavomir Kaslev (Apr 23 2020 at 13:46):

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 (Apr 23 2020 at 13:47):

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 (Apr 23 2020 at 13:50):

You could use the `subsingleton`

typeclass in Lean I guess, but your proof looks pretty direct.

#### Kevin Buzzard (Apr 23 2020 at 13:50):

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 (Apr 23 2020 at 14:00):

Also if you're willing to use mathlib machinery, `iscontr_unit`

and `notcontr_bool`

are decidable, so proved by `dec_trivial`

.

#### Mario Carneiro (Apr 23 2020 at 14:03):

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)

Last updated: May 15 2021 at 00:39 UTC