fact: Definition equiv_apD10 {A : Type} (P : A -> Type) f g : (f = g) <~> (f == g) := Build_Equiv _ _ (@apD10 A P f g) _.
imports: Basics.Overture Basics.Equivalences Basics.PathGroupoids Basics.Tactics Basics.Trunc Basics.Contractible Basics.Trunc (istrunc_forall)