proposition: Lemma ischoicebasecoprod {X Y : UU} (isx : ischoicebase X) (isy : ischoicebase Y) : ischoicebase (coprod X Y).
proof: Proof. intros. unfold ischoicebase. intros P fs. apply (hinhfun (invweq (weqsecovercoprodtoprod P))). apply hinhand. apply (isx _ (λ x : X, fs (ii1 x))). apply (isy _ (λ y : Y, fs (ii2 y))). Defined.
imports: UniMath.Foundations.Propositions