proposition: Lemma filterlim_comp {X Y Z : UU} : ∏ (f : X → Y) (g : Y → Z) (F : PreFilter X) (G : PreFilter Y) (H : PreFilter Z), filterlim f F G → filterlim g G H → filterlim (funcomp f g) F H.
proof: Proof. intros f g F G H Hf Hg A Fa. specialize (Hg _ Fa). specialize (Hf _ Hg). apply Hf. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA