A B (x : A + B) : { b : Bool & if b then A else B } := (_; match x as s return (if match s with | inl _ => true | inr _ => false end then A else B) with | inl a => a | inr b => b end).
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.