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