namespace http://mathhub.info/MitM/core/topology ❚
import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/core/typedsets ❚

theory neighborhoodSystem : base:?Logic =
    include sets:?filter ❙

    universe : type ❘ # X ❙
    nhsys : X ⟶ powerset (set X) ❘ # N ❙
    axiom_filter : ⊦ ∀ [x] isFilter (N x)❙ // maybe better use a predicate subtype for N? ❙
    axiom_nhsys1 :  ⊦ ∀ [x] ∀ [U] U ∈ (N x) ⇒ x ∈ U ❙
    axiom_nhsys2 : ⊦ ∀ [x] ∀ [U] U ∈ (N x) ⇒ ∃ [V] (N x) ∧ ∀ [y] y ∈ V ⇒ U ∈ (N y) ❙
    isOpen : (set X) ⟶ bool ❘ = [S]  ∀ [x] x ∈ S ⇒ ∃ [U] U ∈ (N x) ∧ U ⊑ S❙
❚

// view topologyFromNHsystem: ?topology_theory -> ?neighborhoodSystem =
//   universe := universe ❙
//   topology := isOpen ❙
❚