How to prove in Lean that sums are distributive?

Question

Assume we are given three types in Lean.

constants A B C : Type

There is a canonical map of the following form.

definition can : sum (A × B) (A × C) → A × (sum B C) := 
  λ x , sum.cases_on x  (λ y : A × B, ⟨y.fst, sum.inl y.snd⟩) 
                        (λ y : A × C, ⟨y.fst, sum.inr y.snd⟩)

I believe that this map should have an inverse (according to B. Jacobs book Categorical Logic and Type Theory page 143 coproducts in type theory are automatically distributive). I have trouble constructing the inverse in Lean, because I do not understand how sum.rec works, and I have trouble relating Jacobs unpack P as ... notation to the inductive definition of sums in Lean.

Can someone show me how I can define the inverse of can in Lean using sum.rec?

Answer 1

Likely the most idiomatic option is the equation compiler:

variables {A B C : Type}

open sum

def can : sum (A × B) (A × C) → A × (sum B C)
| (inl ⟨a, b⟩) := ⟨a, inl b⟩
| (inr ⟨a, c⟩) := ⟨a, inr c⟩

It may also be worth writing the forward map like this:

variables {A B C : Type}

open sum

def can : sum (A × B) (A × C) → A × (sum B C)
| (inl ab) := ⟨ab.1, inl ab.2⟩
| (inr ac) := ⟨ac.1, inr ac.2⟩

as it probably has a better definitional expansion (Lean 3 doesn't have definitional eta, Lean4 does). I wonder if it's now clear how to write the inverse now, I'll attach it below if not:

 def nac : A × (sum B C) → sum (A × B) (A × C)
 | ⟨a, inl b⟩ := inl ⟨a, b⟩
 | ⟨a, inr c⟩ := inr ⟨a, c⟩
 

Answer 2

I have figured out how to write the inverse using @sum.cases_on. The rules of @sum.cases_on in lean are nearly identical as the rules of match in Jacobs book. The code is:

definition can (α : Type) (β : Type) (γ : Type)
  : sum (α × β) (α  × γ) → α × (sum β γ) := 
  λ x , sum.cases_on x  (λ y : α × β, ⟨y.fst, sum.inl y.snd⟩) 
                        (λ y : α × γ, ⟨y.fst, sum.inr y.snd⟩)

definition nac (α : Type) (β : Type) (γ : Type)
  : α × (sum β γ) → sum (α × β) (α × γ) :=
  λ v : α × (sum β γ), 
    sum.cases_on v.snd 
      (λ b : β, sum.inl ⟨v.fst,b⟩) (λ c : γ, sum.inr ⟨v.fst,c⟩)

I admit that it does not look as good as the version of It'sNotALie.