proposition: Lemma retr_f_g_isHSet_A_so_B {A B} (f : A -> B) (g : B -> A) : f o g == idmap -> IsHSet A -> IsHSet B.
proof: Proof. intros retr_f_g isHSet_A. srapply hset_axiomK. unfold axiomK. intros x p. assert (ap g p = 1) as g_p_is_1. - apply (axiomK_hset isHSet_A). - assert (1 = (retr_f_g x) ^ @ (ap f (ap g p)) @ (retr_f_g x)) as rhs_is_1. + rewrite g_p_is_1. simpl. rewrite concat_p1. rewrite concat_Vp. exact 1. + rewrite (rhs_is_1). apply (retr_f_g_path_in_B f g retr_f_g). 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)