{A B} : A + B -> Type0 := is_inr_and (fun _ => Unit). Global Instance ishprop_is_inl {A B} (x : A + B) : IsHProp (is_inl x). Proof. destruct x; exact _. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.