fact: Definition equiv_homotopic {A B : Type} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : f == g) : A <~> B := Build_Equiv _ _ g (isequiv_homotopic f h).
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics