A + B -> A' + B' := fun z => match z with inl z' => inl (f z') | inr z' => inr (g z') end.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.