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