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. intros f g F G H Hf Hg A Fa. specialize (Hg _ Fa). specialize (Hf _ Hg). apply Hf. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.