Relationships between spaces

[jamesdabbs]

We eventually want to support full-on automated theorem prover integration, but would it be possible to model a handful of simple relationships between spaces ("is a (closed) subspace of", "is a product of")?

[StevenClontz]

On a related note, I'm also imagining a functor model, that does things like send X \mapsto C_p(X). C_p theory in particular has lots of nice results such as when X is T_{3.5}, X is sigma-compact if and only if C_p(X) is Markov countably fan tight. So if S42 represents X and F13 represents applying C_p, we could have "spaces" like S42+F13 to represent C_p(X), and pi-base automatically converts the properties of X into the properties of C_p(X). In the case that C_p(X) is has been specifically studied in the literature and additional results not characterized by the functor itself are known, then a new space (and new uid) should be added to the database, and S42+F13 could redirect to it.