fact: Definition decidablepaths_equiv' (A : Type) {B : Type} (f : A <~> B) : DecidablePaths A -> DecidablePaths B := decidablepaths_equiv A f.
imports: Basics.Overture Basics.PathGroupoids Basics.Trunc Basics.Tactics