proposition: Lemma total2_paths2_b {A : UU} {B : A -> UU} {a1 : A} {b1 : B a1} {a2 : A} {b2 : B a2} (p : a1 = a2) (q : b1 = transportb B p b2) : a1,,b1 = a2,,b2.
proof: Proof. intros. exact (two_arg_paths_b p q). Defined.
imports: UniMath.Foundations.Preamble