proposition: Lemma bisimulation_equiv_id : forall u v : V, (u = v) <~> (u ~~ v).
proof: 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient