proposition: Lemma Book_3_2_solution_2 (A B : Type) : IsHSet A -> IsHSet B -> IsHSet (A+B).
proof: Proof. intros isHSet_A isHSet_B. srapply hset_axiomK. unfold axiomK. intros x p. destruct x. - rewrite (inverse (eisretr_path_sum p)). rewrite (axiomK_hset isHSet_A a (path_sum_inv p)). simpl; exact idpath. - rewrite (inverse (eisretr_path_sum p)). rewrite (axiomK_hset isHSet_B b (path_sum_inv p)). simpl; exact idpath. 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)