{A B} (z : A + B) : is_inl z -> A. Proof. destruct z as [a|b]. - intros; exact a. - intros e; elim e. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.