fact: Definition equiv_unfunctor_sum {A A' B B' : Type} (h : A + B <~> A' + B') (Ha : forall a:A, is_inl (h (inl a))) (Hb : forall b:B, is_inr (h (inr b))) : (A <~> A') * (B <~> B') := (equiv_unfunctor_sum_l h Ha Hb , equiv_unfunctor_sum_r h Ha Hb).
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall