Sum type cancellation

Stream: new members

[Grayson Burton]

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]

The theorem is false. nat ⊕ empty is isomorphic to nat ⊕ nat

[Mario Carneiro]

By the way, the computable version of bijection is called equiv and there is a sizeable mathlib file about it

[Bryan Gin-ge Chen]

(You can use rintros in the community web editor if you import tactic.)

[Grayson Burton]

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

[Mario Carneiro]

The theorem is true for cancelling option, or more generally if α is finite, but I don't think it is computable

[Mario Carneiro]

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]

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]

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]

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