proposition: Lemma retr_f_g_path_in_B {A B} (f : A -> B) (g : B -> A) (alpha : f o g == idmap) (x y : B) (p : x = y) : p = (alpha x)^ @ (ap f (ap g p)) @ (alpha y).
proof: Proof. destruct p. simpl. rewrite concat_p1. rewrite concat_Vp. exact 1. 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)