fact: Definition equiv_ind `{IsEquiv A B f} (P : B -> Type) : (forall x:A, P (f x)) -> forall y:B, P y := fun g y => transport P (eisretr f y) (g (f^-1 y)).
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics