Lemma locally2d_correct {T S : TopologicalSpace} (x : T) (y : S) : ∏ P : T × S → hProp, locally2d x y P <-> locally (T := TopologyDirprod T S) (x,,y) P. Proof. intros P. split ; apply hinhuniv. - intros A. apply TopologyFromNeighborhood_correct. generalize (pr1 (pr2 (pr2 A))) (pr1 (pr2 (pr2 (pr2 A)))). apply hinhfun2. intros Ox Oy. exists (pr1 Ox), (pr1 Oy). repeat split. + exact (pr1 (pr2 Ox)). + exact (pr2 (pr1 Ox)). + exact (pr1 (pr2 Oy)). + exact (pr2 (pr1 Oy)). + intros x' y' Hx' Hy'. apply (pr2 (pr2 (pr2 (pr2 A)))). * now apply (pr2 (pr2 Ox)). * now apply (pr2 (pr2 Oy)). - intros O. generalize (pr2 (pr1 O) _ (pr1 (pr2 O))). apply hinhfun. intros A. exists (pr1 A), (pr1 (pr2 A)). repeat split. + apply (pr2 (neighborhood_isOpen _)). * exact (pr2 (pr1 (pr2 (pr2 A)))). * exact (pr1 (pr1 (pr2 (pr2 A)))). + apply (pr2 (neighborhood_isOpen _)). * exact (pr2 (pr1 (pr2 (pr2 (pr2 A))))). * exact (pr1 (pr1 (pr2 (pr2 (pr2 A))))). + intros x' y' Ax' Ay'. apply (pr2 (pr2 O)). now apply (pr2 (pr2 (pr2 (pr2 A)))). 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 _ _).