{A B} (f : A -> B) `{IsTruncMap (-2) A B f} : IsEquiv f. Proof. srapply Build_IsEquiv. - intros b; exact (center {a : A & f a = b}).1. - intros b. exact (center {a : A & f a = b}).2. - intros a. exact (@contr {x : A & f x = f a} _ (a;1))..1. - intros a; cbn. apply moveL_M1. lhs_V nrapply transport_paths_l. lhs_V nrapply transport_compose. exact ((@contr {x : A & f x = f a} _ (a;1))..2). Defined.
Require Import HoTT.Basics. Require Import Types.Sigma Types.Forall Types.Arrow Types.Paths.