Definition pair_path2 {A} {B:A->UU} {a a1 a2} {b1:B a1} {b2:B a2} (p:a1 = a) (q:a2 = a) (e:p#b1 = q#b2) : a1,,b1 = a2,,b2. Proof. intros. induction p,q; compute in e. induction e. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.