Lemma ischoicebaseweqb {X Y : UU} (w : X ≃ Y) (is : ischoicebase Y) : ischoicebase X. Proof. intros. apply (ischoicebaseweqf (invweq w) is). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.