forall {x y : V}, (x ⊆ y * y ⊆ x) <-> x = y. Proof. refine (V_ind_hprop _ _ _). intros A f _. refine (V_ind_hprop _ _ _). intros B g _. split. - intros [H1 H2]. apply setext'. split. + intro. refine (Trunc_rec _ (H1 (f a) (tr (a;1)))). intros [b p]. apply tr. exists b. exact p^. + intro. apply (H2 (g b)). apply tr; exists b; reflexivity. - intro p; split. + intros z Hz. apply (transport (fun x => z ∈ x) p Hz). + intros z Hz. apply (transport (fun x => z ∈ x) p^ Hz). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.