proposition: Fact Cantor_path_injection {X Y} : (X -> HProp) = (X + Y) -> (X + X) = X -> Injection (X -> HProp) Y.
proof: Proof. intros H1 H2. assert (H : X + Y = (X -> HProp) * (X -> HProp)). - now rewrite <- H1, path_sum_prod, H2. - apply equiv_path in H as [f [g Hfg Hgf _]]. pose (f' x := fst (f (inl x))). destruct (hCantor f') as [p Hp]. pose (g' q := g (p, q)). assert (H' : forall q x, g' q <> inl x). + intros q x H. apply (Hp x). unfold f'. rewrite <- H. unfold g'. now rewrite Hfg. + exists (fun x => proj1 (clean_sum _ H' x)). intros q q' H. assert (Hqq' : g' q = g' q'). * destruct clean_sum as [z <-]. destruct clean_sum as [z' <-]. cbn in H. now rewrite H. * unfold g' in Hqq'. change (snd (p, q) = snd (p, q')). rewrite <- (Hfg (p, q)), <- (Hfg (p, q')). now rewrite Hqq'. 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)