Lemma topologygenerated_and : ∏ x : X, isfilter_and (topologygenerated x). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.DivisionRig. Require Import UniMath.Algebra.ConstructiveStructures. Section TopologyFromNeighborhood. End TopologyFromNeighborhood. Definition TopologyFromNeighborhood {X : hSet} Lemma TopologyFromNeighborhood_correct {X : hSet} N x P <-> neighborhood (T := TopologyFromNeighborhood N H) x P. simple refine (TopologyFromNeighborhood _ _). apply TopologyFromNeighborhood_correct. simple refine (TopologyFromNeighborhood _ _). apply TopologyFromNeighborhood_correct. simple refine (TopologyFromNeighborhood _ _).