topological_space.opens.map

opens.map f gives the functor from open sets in Y to open set in X, given by taking preimages under f.