{A B} {f : A -> V} {g : B -> V} : set f = set g -> equal_img f g. 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.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.