Definition PreFilterIm {X Y : UU} (f : X → Y) (F : PreFilter X) : PreFilter Y. Proof. simple refine (make_PreFilter _ _ _ _). - exact (filterim f F). - apply filterim_imply, filter_imply. - apply filterim_htrue, filter_htrue. - apply filterim_and, filter_and. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.