{A B} (P : B -> Type@{p}) : A + B -> Type@{p} := fun x => match x with inl _ => Empty | inr b => P b end.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.