{A A' B B' : Type} (h : A + B -> A' + B') (Ha : forall a:A, is_inl (h (inl a))) : A -> A' := fun a => un_inl (h (inl a)) (Ha a).
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.