Lemma ischoicebasecoprod {X Y : UU} (isx : ischoicebase X) (isy : ischoicebase Y) : ischoicebase (coprod X Y). 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.
Require Import UniMath.Foundations.UnivalenceAxiom.