Lemma neighborhood_isOpen (P : T → hProp) : (∏ x, P x → neighborhood x P) <-> isOpen P. Proof. split. - intros Hp. assert (H : ∏ A : T → hProp, isaprop (∏ y : T, A y → P y)). { intros A. apply impred_isaprop. intro y. apply isapropimpl. apply propproperty. } set (Q := λ A : T → hProp, isOpen A ∧ (make_hProp (∏ y : T, A y → P y) (H A))). assert (X : P = (union Q)). { apply funextfun. intros x. apply hPropUnivalence. - intros Px. generalize (Hp _ Px). apply hinhfun. intros A. exists (pr1 A) ; split. + split. * apply (pr2 (pr1 A)). * exact (pr2 (pr2 A)). + exact (pr1 (pr2 A)). - apply hinhuniv. intros A. apply (pr2 (pr1 (pr2 A))). exact (pr2 (pr2 A)). } rewrite X. apply isOpen_union. intros A Ha. apply (pr1 Ha). - intros Hp x Px. apply hinhpr. exists (P,,Hp). split. + exact Px. + intros y Py. exact Py. 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 _ _).