Definition cp_idpath (A:Type) (a1 a2:A) (p:a1=a2) (B:A->Type) (b1:B a1) (b2:B a2) (u:PathOver p b1 b2) : cp (idpath p) u = u. Proof. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.