# Zulip Chat Archive

## Stream: new members

### Topic: Sum type cancellation

#### Grayson Burton (Mar 02 2020 at 01:28):

Hello. This is my first time posting here (or on Zulip at all) so if I should've put this somewhere else or done this differently, my bad.

I've been fairly stuck trying to prove this theorem that I *believe* is correct. I really want to stick to computable proofs as well, but I'm happy to bend that if need be.

-- Type isomorphism. Classically is equivalent to bijection but this allows me to use the inverse function `g` while staying computable. def type_iso (α β : Type) : Prop := ∃ (f : α → β) (g : β → α), function.left_inverse f g ∧ function.right_inverse f g theorem sum_cancel {α β γ : Type} (hsum : type_iso (α ⊕ β) (α ⊕ γ)) : type_iso β γ := begin cases hsum with fs gshfs, cases gshfs with gs hfs, let f : β → γ := λ x, sum.cases_on (fs $ sum.inr x) (λ a, sorry) id, let g : γ → β := λ x, sum.cases_on (gs $ sum.inr x) (λ a, sorry) id, existsi f, existsi g, split, begin intro x, sorry end, begin intro x, sorry end end

(I could've used `rintros`

for `sum_cancel`

but am using the Lean web editor to draft this)

Can someone point me in the right direction? Thanks!

#### Mario Carneiro (Mar 02 2020 at 01:51):

The theorem is false. `nat ⊕ empty`

is isomorphic to `nat ⊕ nat`

#### Mario Carneiro (Mar 02 2020 at 01:52):

By the way, the computable version of `bijection`

is called `equiv`

and there is a sizeable mathlib file about it

#### Bryan Gin-ge Chen (Mar 02 2020 at 01:54):

(You can use `rintros`

in the community web editor if you `import tactic`

.)

#### Grayson Burton (Mar 02 2020 at 02:01):

Oh cool. Thanks! @Mario Carneiro @Bryan Gin-ge Chen

#### Mario Carneiro (Mar 02 2020 at 02:02):

The theorem is true for cancelling `option`

, or more generally if `α`

is finite, but I don't think it is computable

#### Mario Carneiro (Mar 02 2020 at 02:06):

Actually, I think it might be computable. If `f : option A -> option B`

has an inverse `g`

, and you want to construct a function `A -> B`

, you check if `f (some a) = some b`

so you are done, or `f (some a) = none`

in which case `f none = some b`

. (`f none`

cannot be `none`

in this case since `f`

is injective.)

#### Grayson Burton (Mar 02 2020 at 02:11):

I'll have to see about using `data.equiv`

, it seems to have gotten most of the boilerplate out of the way (like proving type isomorphism an equivalence relation).

#### Grayson Burton (Mar 02 2020 at 06:49):

Product types aren't cancellative either. :( There go my dreams of embedding the commutative semiring of types in a signed type commutative ring

#### Reid Barton (Mar 02 2020 at 16:21):

https://ncatlab.org/nlab/show/Eilenberg+swindle

Last updated: May 09 2021 at 19:11 UTC