Definition inverse_cp_p'' (A:Type) (B:A->Type) (a1 a2:A) (b1:B a1) (b2:B a2) (p q:a1=a2) (α : p=q) (t : PathOver p b1 b2) (u : PathOver q b1 b2) : PathOver (Y := λ pq, PathOver pq _ _) α t u -> PathOver (Y := λ pq, PathOver pq _ _) (!α) u t. Proof. intros k. induction α, p, k. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.