A B (C : A + B -> Type) : { x : A+B & C x } <~> { a : A & C (inl a) } + { b : B & C (inr b) }. Proof. refine (Build_Equiv { x : A+B & C x } ({ a : A & C (inl a) } + { b : B & C (inr b) }) (fun xc => let (x,c) := xc in match x return C x -> ({ a : A & C (inl a) } + { b : B & C (inr b) }) with | inl a => fun c => inl (a;c) | inr b => fun c => inr (b;c) end c) _). simple refine (Build_IsEquiv { x : A+B & C x } ({ a : A & C (inl a) } + { b : B & C (inr b) }) _ (fun abc => match abc with | inl (a;c) => (inl a ; c) | inr (b;c) => (inr b ; c) end) _ _ _). - intros [[a c]|[b 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.