fixing some docs

theories/topology_theory/subtype_topology.v

@@ -7,16 +7,22 @@ From mathcomp Require Import product_topology subspace_topology.
 (**md**************************************************************************)
 (* # Subtypes of topological spaces                                           *)
 (* We have two distinct ways of building topologies as subsets of a           *)
-(* topological space `X`. One is the `subspace topology`, which builds a new  *)
-(* topology on X which 'isolates' a set A. The other considers the sigma      *)
-(* type `set_type` in the weak topology by the inclusion. Note `subspace A`   *)
-(* has the advantage that it preserves all the algebraic structure on X, and  *)
-(* the relevant local behavior A (in particular, continuity). On the other    *)
-(* hand `set_val A` has the right global properties you'd expect for the      *)
-(* subset topology. But you can't easily add two elements of `set_val [0,1]`. *)
+(* topological space `X`. One is the `subspace topology`, which is defined in *)
+(* `subspace_topology.v`. It builds a topology on X which 'isolates' a set A. *)
+(* Ther other, defined in this file, defines a topology on the sigma type     *)
+(* `set_type` in the weak topology by the inclusion. Note `subspace A` has    *)
+(* the advantage that it preserves all the algebraic structure on X, but only *)
+(* the local behavior A (in particular, continuity). On the other hand        *)
+(* `set_type A` has the right global properties you'd expect for the subset   *)
+(* topology. But you can't easily add two elements of `set_val [0,1]`.        *)
 (* Note the implicit coercion from sets to `set_val` from `classical`.        *)
 (*                                                                            *)
 (* This file provides `set_type` with a topology, and some theory.            *)
+(* ```                                                                        *)
+(*           sigT_of_setX == commutes `set_type` and product topologies       *)
+(*           setX_of_sigT == commutes product and `set_type` topologies       *)
+(* ```                                                                        *)
+(*                                                                            *)
 (******************************************************************************)
 
 Local Open Scope classical_set_scope.