Definition cp_apstar (A:Type) (B:A->Type) (a1 a2 a3:A) (p p':a1=a2) (q q':a2=a3) (α : p=p') (β : q=q') (b1:B a1) (b2:B a2) (b3:B a3) (pp : PathOver p b1 b2) (qq : PathOver q b2 b3) : cp (apstar α β) (pp * qq) = cp α pp * cp β qq. Proof. now induction p, α, β. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.