{u v w : V} : V_pair u v = V_singleton w <-> (u = w) * (v = w). 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.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.