Definition FilterIm {X Y : UU} (f : X → Y) (F : Filter X) : Filter Y. Proof. refine (tpair _ _ _). split. - apply (pr2 (PreFilterIm f F)). - apply filterim_notempty, filter_notempty. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.