proposition: Lemma path_pair {u v u' v' : V@{U' U}} : (u = u') * (v = v') -> V_pair u v = V_pair u' v'.
proof: Proof. intros (H1, H2). apply setext'. split. + apply Bool_ind. * apply tr; exists true. assumption. * apply tr; exists false; assumption. + apply Bool_ind. * apply tr; exists true; assumption. * apply tr; exists false; assumption. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient