(forall a : Au, {a' : Au' & mu' a' = mu a}) * (forall a' : Au', {a : Au & mu a = mu' a'}). 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.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.