proposition: Lemma eq_img_untrunc : (forall a : Au, {a' : Au' & mu' a' = mu a}) * (forall a' : Au', {a : Au & mu a = mu' a'}).
proof: Proof. split. - intro a. exact (@untrunc_istrunc (-1) _ (mono' (mu a)) (transport (fun x => mu a ∈ x) (p^ @ p') (tr (a; 1)))). - intro a'. exact (@untrunc_istrunc (-1) _ (mono (mu' a')) (transport (fun x => mu' a' ∈ x) (p'^ @ p) (tr (a'; 1)))). Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient