Lemma ischoicebaseweqf {X Y : UU} (w : X ≃ Y) (is : ischoicebase X) : ischoicebase Y. Proof. intros. unfold ischoicebase. intros Q fs. apply (hinhfun (invweq (weqonsecbase Q w))). apply (is (funcomp w Q) (λ x : X, fs (w x))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.