isequiv_commsq' {A B C D} (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D) (p : g o h == k o f) `{IsEquiv _ _ g} `{IsEquiv _ _ h} `{IsEquiv _ _ k} : IsEquiv f. Proof. refine (@cancelL_isequiv _ _ _ k f _ _). refine (isequiv_homotopic _ p). Defined.
Require Import