This file constructs products, sums, subtypes and quotients of topological spaces and sets up their basic theory, such as criteria for maps into or out of these constructions to be continuous; descriptions of the open sets, neighborhood filters, and generators of these constructions; and their behavior with respect to embeddings and other specific classes of maps.
The constructed topologies are defined using induced and coinduced topologies along with the complete lattice structure on topologies. Their universal properties (for example, a map X → Y × Z is continuous if and only if both projections X → Y, X → Z are) follow easily using order-theoretic descriptions of continuity. With more work we can also extract descriptions of the open sets, neighborhood filters and so on.
product, sum, disjoint union, subspace, quotient space
The first projection in a product of topological spaces sends open sets to open sets.
The second projection in a product of topological spaces sends open sets to open sets.
A product set is open in a product space if and only if each factor is open, or one of them is empty
A map out of a sum type is continuous if its restriction to each summand is.
The sum of embeddings is an embedding.