proposition: Lemma pairing : forall u v, hexists (fun w => forall x, x ∈ w <-> hor (x = u) (x = v)).
proof: Proof. intros u v. apply tr. exists (V_pair u v). intro; split; apply (Trunc_functor (-1)). - intros [[|] p]; [left|right]; exact p^. - intros [p | p]; [exists true | exists false]; exact p^. Qed.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient