proposition: Lemma pair_eq_singleton {u v w : V} : V_pair u v = V_singleton w <-> (u = w) * (v = w).
proof: Proof. split. + intro H. destruct (path_V_eqimg H) as (H1, H2). refine (Trunc_rec _ (H1 true)). intros [t p]; destruct t. refine (Trunc_rec _ (H1 false)). intros [t p']; destruct t. split; [exact p| exact p']. + intros (p1, p2). apply setext'; split. * intro a; apply tr; exists tt. destruct a; [exact p1 | exact p2]. * intro t; apply tr; exists true. destruct t; exact p1. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient