proposition: Lemma Book_3_7_solution_1 (A B: Type) : IsHProp A -> IsHProp B -> ~(A*B) -> IsHProp (A+B).
proof: Proof. intros isHProp_A isProp_B nab. apply hprop_allpath. intros x y. destruct x as [a1|b1]; destruct y as [a2|b2]; apply path_sum; try apply path_ishprop. - exact (nab (a1,b2)). - exact (nab (a2,b1)). Defined.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)