sum_empty_l@{u|} (A : Type@{u}) : Equiv@{u u} (Empty + A) A. Proof. snrapply equiv_adjointify@{u u}. - intros [e|a]; [ exact (Empty_rec@{u} e) | exact a ]. - intros a; exact (inr@{Set u} a). - intro x; exact idpath@{u}. - intros [e|z]; [ elim e | exact idpath@{u}]. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.