proposition: Lemma isasetcoprod (X Y : UU) (isx : isaset X) (isy : isaset Y) : isaset (coprod X Y).
proof: Proof. intros. apply (isofhlevelssncoprod 0 _ _ isx isy). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom