X Y X' Y' : InjectsInto X X' -> InjectsInto Y Y' -> InjectsInto (X + Y) (X' + Y'). Proof. intros H1 H2. eapply merely_destruct; try apply H1. intros [f Hf]. eapply merely_destruct; try apply H2. intros [g Hg]. apply tr. exists (fun z => match z with inl x => inl (f x) | inr y => inr (g y) end). intros [x|y] [x'|y'] H. - apply ap. apply Hf. apply path_sum_inl with Y'. apply H. - by apply inl_ne_inr in H. - by apply inr_ne_inl in H. - apply ap. apply Hg. apply path_sum_inr with X'. apply H. Qed.
From HoTT Require Import TruncType ExcludedMiddle abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Spaces.Nat.Core Spaces.Card. From HoTT Require Import Equiv.BiInv. From HoTT Require Import HIT.unique_choice. From HoTT.Sets Require Import Ordinals Hartogs Powers GCH AC.