## Stream: new members

### Topic: Category of Topological Spaces

#### Ken Lee (Jun 13 2019 at 17:28):

Where can I find the definition of the category of topological spaces in mathlib? It doesn't seem to be in category_theory.

#### Kenny Lau (Jun 13 2019 at 17:30):

/-- The category of topological spaces and continuous maps. -/
@[reducible] def Top : Type (u+1) := bundled topological_space


#### Kenny Lau (Jun 13 2019 at 17:30):

https://github.com/leanprover-community/mathlib/blob/master/src/topology/Top/basic.lean#L14

#### Kenny Lau (Jun 13 2019 at 17:30):

Last updated: May 08 2021 at 10:12 UTC