(A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f} : DecidablePaths A -> DecidablePaths B. Proof. intros d x y. destruct (d (f^-1 x) (f^-1 y)) as [e|ne]. - apply inl. exact ((eisretr f x)^ @ ap f e @ eisretr f y). - apply inr; intros p. apply ne, ap, p. Defined.
Require Import