proposition: Lemma topologygenerated_and : ∏ x : X, isfilter_and (topologygenerated x).
proof: Proof. intros x A B. apply hinhfun2. intros La Lb. exists (concatenate (pr1 La) (pr1 Lb)). repeat split. - simpl ; intro. apply (coprod_rect (λ x, O (coprod_rect _ _ _ x))) ; intros m. + rewrite coprod_rect_compute_1. exact (pr1 (pr2 La) _). + rewrite coprod_rect_compute_2. exact (pr1 (pr2 Lb) _). - simpl ; intro. apply (coprod_rect (λ y, (coprod_rect (λ _ : stn (length (pr1 La)) ⨿ stn (length (pr1 Lb)), X → hProp) (λ j : stn (length (pr1 La)), (pr1 La) j) (λ k : stn (length (pr1 Lb)), (pr1 Lb) k) y) x)) ; intros m. + rewrite coprod_rect_compute_1. exact (pr1 (pr2 (pr2 La)) _). + rewrite coprod_rect_compute_2. exact (pr1 (pr2 (pr2 Lb)) _). - apply (pr2 (pr2 (pr2 La))). intros n. simpl in X0. unfold concatenate' in X0. specialize (X0 (weqfromcoprodofstn_map (length (pr1 La)) (length (pr1 Lb)) (ii1 n))). now rewrite (weqfromcoprodofstn_eq1 _ _) , coprod_rect_compute_1 in X0. - apply (pr2 (pr2 (pr2 Lb))). intros n. simpl in X0. unfold concatenate' in X0. specialize (X0 (weqfromcoprodofstn_map (length (pr1 La)) (length (pr1 Lb)) (ii2 n))). now rewrite (weqfromcoprodofstn_eq1 _ _), coprod_rect_compute_2 in X0. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Topology.Filters UniMath.Algebra.Groups UniMath.Algebra.DivisionRig UniMath.Algebra.ConstructiveStructures