X : X + X = Bool * X. 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.
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.