forall u v : V, (u = v) <~> (u ~~ v). Proof. intros u v. apply equiv_iff_hprop. - intro p; exact (transport (fun x => u ~~ x) p (reflexive_bisimulation u)). - generalize u v. refine (V_ind_hprop _ _ _); intros A f H_f. refine (V_ind_hprop _ _ _); intros B g _. simpl; intros [H1 H2]. apply setext'. split. + intro a. generalize (H1 a). apply (Trunc_functor (-1)). intros [b h]. exists b; exact (H_f a (g b) h). + intro b. generalize (H2 b). apply (Trunc_functor (-1)). intros [a h]. exists a; exact (H_f a (g b) h). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.