Definition cp_apstar' (A:Type) (B:A->Type) (a1 a2:A) (p:a2=a1) (p':a1=a2) (α : !p=p') (b1:B a1) (b2:B a2) (pp : PathOver (Y:=B) p b2 b1) : cp α (pp^-1) = inversePathOver' (cp (invrot α) pp). Proof. now induction α, p. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.