A B C : A * (B + C) <~> (A * B) + (A * C). Proof. snrapply Build_Equiv. 2: snrapply Build_IsEquiv. - intros [a [b|c]]. + exact (inl@{u u} (a, b)). + exact (inr@{u u} (a, c)). - intros [[a b]|[a c]]. + exact (a, inl@{u u} b). + exact (a, inr@{u u} c). - intros [[a b]|[a c]]; reflexivity. - intros [a [b|c]]; reflexivity. - intros [a [b|c]]; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.