proposition: Lemma extensionality : forall {x y : V}, (x ⊆ y * y ⊆ x) <-> x = y.
proof: 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient