forall u v, hexists (fun w => forall x, x ∈ w <-> hor (x = u) (x = v)). 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.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.