Add that a map that is a homeomorphism onto its image is referred to as a subspace inclusion (this term is referenced in Section 3).
]]>Changed S -> Y in the first paragraph, to match the rest of the exposition (which uses Y for the subset/subspace).
]]>added statement of the universal property (here), first in classical form, then using the sharp modality, and added remark that this should be the categorical semantics of Mike’s remark 3.14 in arXiv:1509.07584
(also replaced the Definition-paragraph with a slightly beautified version)
]]>