proposition: Lemma path_sum_prod X Y Z : (X -> Z) * (Y -> Z) = ((X + Y) -> Z).
proof: Proof. apply path_universe_uncurried. apply equiv_sum_distributive. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)