Curry-howard isomorphism in object oriented programming languages
If you only consider terminating functions, then your axiomatisation works :-) Indeed, terminating functions have a resonable notion of equality:
If their return type has decidable equality then the functions have decidable equality.

Regarding your code, it could be rendered in an OOP-like fashion this way

record TopologicalSpace : Set₁ where

  field     
     BaseSet  : Set
     Topology : (BaseSet → Boolean) → Boolean

  Empty    = λ (x : BaseSet) → false
  Universe = λ (x : BaseSet) → true

  field
    axiom1   :       Topology Empty    ≡ true
                AND  Topology Universe ≡ true


This is a real programming language whose functions must always terminate: It is Agda; http://learnyouanagda.liamoc.net/

The source for the code can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/TopologicalSpaces.agda