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