Definition cp_left (A:Type) (a2 a3:A) (p p':a2=a3) (α:p=p') (B:A->Type) (b1 b2:B a2) (b3:B a3) (r:PathOver (idpath a2) b1 b2) (q:PathOver p b2 b3) : r * cp α q = cp α (r*q). Proof. now induction r, α. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.