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