Lemma neighborhood_equiv {T : TopologicalSpace} (x : T) (B : base_of_neighborhood x) : ∏ P, neighborhood' x B P <-> neighborhood x P. Proof. split. - apply hinhuniv. intros O. generalize ((pr1 (pr2 B)) (pr1 O) (pr1 (pr2 O))). apply neighborhood_imply. exact (pr2 (pr2 O)). - intros Hp. generalize (pr2 (pr2 B) P Hp). apply hinhfun. intros O. exists (pr1 O). exact (pr2 O). 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 _ _).