fact: Definition equiv_path_arrow {A B : Type} (f g : A -> B) : (f == g) <~> (f = g) := equiv_path_forall f g.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall