`{Funext} {A B : pType} (f g h : A ->* B) (K : g ==* f) : f ==* h <~> g ==* h. Proof. refine ((equiv_path_pforall _ _)^-1%equiv oE _ oE equiv_path_pforall _ _). rapply equiv_concat_l. apply equiv_path_pforall. exact K. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.