A {B} (f : A -> B) `{IsTrunc n A} `{IsEquiv A B f} : IsTrunc n B. Proof. generalize dependent B; generalize dependent A. simple_induction n n IH; simpl; intros A ? B f ?. - exact (contr_equiv _ f). - apply istrunc_S. intros x y. refine (IH _ _ _ (ap (f^-1))^-1 _). Defined.
Require Import