A B C : (B + C) * A <~> (B * A) + (C * A). Proof. refine (Build_Equiv ((B + C) * A) ((B * A) + (C * A)) (fun abc => let (bc,a) := abc in match bc with | inl b => inl (b,a) | inr c => inr (c,a) end) _). simple refine (Build_IsEquiv ((B + C) * A) ((B * A) + (C * A)) _ (fun ax => match ax with | inl (b,a) => (inl b,a) | inr (c,a) => (inr c,a) end) _ _ _). - intros [[b a]|[c a]]; reflexivity. - intros [[b|c] a]; reflexivity. - intros [[b|c] a]; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.