Lemma isapropischoicebase (X : UU) : isaprop (ischoicebase_uu1 X). Proof. apply impred. intro P. apply impred. intro fs. apply (pr2 (ishinh _)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.