Lemma Lemma023 (A:Type) (B:A->Type) (a1 a2 a3:A) (b1:B a1) (b2:B a2) (b3:B a3) (p1:a1=a2) (p2:a2=a3) (q:PathOver p1 b1 b2) : isweq (composePathOver q : PathOver p2 b2 b3 -> PathOver (p1@p2) b1 b3). Proof. induction p1, p2, q. apply idisweq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.