proposition: Lemma path_sum_bool X : X + X = Bool * X.
proof: Proof. apply path_universe_uncurried. srapply equiv_adjointify. - exact (fun x => match x with inl x => (true, x) | inr x => (false, x) end). - exact (fun x => match x with (true, x) => inl x | (false, x) => inr x end). - intros [[]]; reflexivity. - intros []; reflexivity. 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)