## 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