Definition cp_in_family (A:Type) (a1 a2:A) (T:Type) (t0 t1:T) (v:t0=t1) (p:T->a1=a2) (B:A->Type) (b1:B a1) (b2:B a2) (s : ∏ t, PathOver (p t) b1 b2) : cp (maponpaths p v) (s t0) = s t1. Proof. now induction v. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.