Definition TopologyFromNeighborhood {X : hSet} (N : X → (X → hProp) → hProp) (H : isNeighborhood N) : TopologicalSpace. Proof. use make_TopologicalSpace. - apply X. - intros A. simple refine (make_hProp _ _). + apply (topologyfromneighborhood N A). + apply isaprop_topologyfromneighborhood. - apply topologyfromneighborhood_open. apply (pr1 H). - intros x _. apply (pr1 (pr2 H)). - intros A B Ha Hb x Hx. apply (pr1 (pr2 (pr2 H))). + now apply Ha, (pr1 Hx). + now apply Hb, (pr2 Hx). Defined.
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 _ _).