fact: Definition isequiv_compose' {A B : Type} (f : A -> B) (_ : IsEquiv f) {C : Type} (g : B -> C) (_ : IsEquiv g) : IsEquiv (g o f) := isequiv_compose.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics