fact: Definition equiv_ap10 {A B : Type} f g : (f = g) <~> (f == g) := Build_Equiv _ _ (@ap10 A B f g) _.
imports: Basics.Overture Basics.PathGroupoids Basics.Decidable Basics.Equivalences Basics.Trunc Basics.Tactics Types.Forall