Lemma filtergenerated_and : isfilter_and filtergenerated. Proof. intros A B. apply hinhfun2. intros Ha Hb. exists (concatenate (pr1 Ha) (pr1 Hb)). split. + simpl ; intros m. unfold concatenate'. set (Hm := (weqfromcoprodofstn_invmap (length (pr1 Ha)) (length (pr1 Hb))) m). change ((weqfromcoprodofstn_invmap (length (pr1 Ha)) (length (pr1 Hb))) m) with Hm. induction Hm as [Hm | Hm]. * rewrite coprod_rect_compute_1. apply (pr1 (pr2 Ha)). * rewrite coprod_rect_compute_2. apply (pr1 (pr2 Hb)). + intros x Hx. simpl in Hx. unfold concatenate' in Hx. split. * apply (pr2 (pr2 Ha)). intros m. specialize (Hx (weqfromcoprodofstn_map _ _ (ii1 m))). rewrite (weqfromcoprodofstn_eq1 _ _), coprod_rect_compute_1 in Hx. exact Hx. * apply (pr2 (pr2 Hb)). intros m. specialize (Hx (weqfromcoprodofstn_map _ _ (ii2 m))). rewrite (weqfromcoprodofstn_eq1 _ _), coprod_rect_compute_2 in Hx. exact Hx. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.