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