Lemma ischoicebasecontr {X : UU} (is : iscontr X) : ischoicebase X. Proof. intros. apply (ischoicebaseweqb (weqcontrtounit is) ischoicebaseunit). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.