Lemma eqweqmap_pathscomp0 {A B C : UU} (p : A = B) (q : B = C) : weqcomp (eqweqmap p) (eqweqmap q) = eqweqmap (pathscomp0 p q). Proof. induction p. induction q. apply pair_path_in2. apply isapropisweq. Defined.