proposition: Lemma path_V_eqimg {A B} {f : A -> V} {g : B -> V} : set f = set g -> equal_img f g.
proof: Proof. intro p. split. - intro a. assert (H : f a ∈ set g). { apply (snd extensionality p). apply tr; exists a; reflexivity. } generalize H; apply (Trunc_functor (-1)). intros [b p']. exists b; exact p'^. - intro b. assert (H : g b ∈ set f). { apply (snd extensionality p^). apply tr; exists b; reflexivity. } generalize H; apply (Trunc_functor (-1)). intros [a p']. exists a; exact p'. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient