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