Definition cp (A:Type) (a1 a2:A) (p q:a1=a2) (α : p=q) (B:A->Type) (b1:B a1) (b2:B a2) : PathOver p b1 b2 ≃ PathOver q b1 b2 := make_weq (transportf (λ pq, PathOver pq b1 b2) α) (Lemma0_2_4 α).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.