diff --git a/theories/cantor.v b/theories/cantor.v
index 21e0b1b10..11658adae 100644
--- a/theories/cantor.v
+++ b/theories/cantor.v
@@ -64,6 +64,8 @@ Proof. by []. Qed.
 Definition pointed_discrete_topology (P : pointedType) : Type :=
   discrete_topology (discrete_pointed_subproof P).
 
+HB.instance Definition _ P := Pointed.on (pointed_discrete_topology P).
+
 End discrete_topology_for_pointed_types.
 (* note that in topology.v, we already have:
 HB.instance Definition _ := discrete_uniform_mixin.
@@ -128,6 +130,15 @@ split.
 - exact: cantor_zero_dimensional.
 Qed.
 
+HB.instance Definition _ (U : Type) (T : U -> ptopologicalType) :=
+  Pointed.copy (forall x : U, T x) (prod_topology T).
+
+Global Instance prod_topology_filter (U : Type) (T : U -> ptopologicalType) (f : prod_topology T) :
+  ProperFilter (nbhs f).
+Proof.
+exact: nbhs_pfilter.
+Qed.
+
 (**md**************************************************************************)
 (* ## Part 1                                                                  *)
 (*                                                                            *)
@@ -143,7 +154,7 @@ Qed.
 (*                                                                            *)
 (******************************************************************************)
 Section topological_trees.
-Context {K : nat -> topologicalType} {X : topologicalType}
+Context {K : nat -> ptopologicalType} {X : ptopologicalType}
         (refine_apx : forall n, set X -> K n -> set X)
         (tree_invariant : set X -> Prop).
 
@@ -233,7 +244,8 @@ elim: n => [|n IH]; first by near=> z => ?; rewrite ltn0.
 near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z).
 move=> [->]; near: z; exists (proj n @^-1` [set b n]).
 split => //; suff : @open T (proj n @^-1` [set b n]) by [].
-by apply: open_comp; [move=> + _; exact: proj_continuous| exact: discrete_open].
+apply: open_comp; [move=> + _; exact: proj_continuous| apply: discrete_open].
+exact: discreteK.
 Unshelve. all: end_near. Qed.
 
 Let apx_prefix b c n :
@@ -253,7 +265,6 @@ Qed.
 Local Lemma tree_map_cts : continuous tree_map.
 Proof.
 move=> b U /cvg_tree_map [n _] /filterS; apply.
-  exact/fmap_filter/nbhs_filter.
 rewrite nbhs_simpl /=; near_simpl; have := tree_prefix b n; apply: filter_app.
 by near=> z => /apx_prefix ->; exact: tree_map_apx.
 Unshelve. all: end_near. Qed.
@@ -299,7 +310,7 @@ End topological_trees.
 (******************************************************************************)
 
 Section TreeStructure.
-Context {R : realType} {T : pseudoMetricType R}.
+Context {R : realType} {T : pseudoPMetricType R}.
 Hypothesis cantorT : cantor_like T.
 
 Let dsctT : zero_dimensional T.   Proof. by case: cantorT. Qed.
@@ -395,13 +406,20 @@ End TreeStructure.
 (* ## Part 3: Finitely branching trees are Cantor-like                        *)
 (******************************************************************************)
 Section FinitelyBranchingTrees.
-Context {R : realType}.
 
-Definition tree_of (T : nat -> pointedType) : pseudoMetricType R :=
-  [the pseudoMetricType R of prod_topology
-    (fun n => pointed_discrete_topology (T n))].
+Definition tree_of (T : nat -> pointedType) : Type :=
+  prod_topology (fun n => pointed_discrete_topology (T n)).
+
+HB.instance Definition _ (T : nat -> pointedType) : Pointed (tree_of T):= 
+  Pointed.on (tree_of T).
+
+HB.instance Definition _ (T : nat -> pointedType) := Uniform.on (tree_of T).
+
+HB.instance Definition _ {R : realType} (T : nat -> pointedType) : 
+    @PseudoMetric R _ :=
+   @PseudoMetric.on (tree_of T).
 
-Lemma cantor_like_finite_prod (T : nat -> topologicalType) :
+Lemma cantor_like_finite_prod (T : nat -> ptopologicalType) :
   (forall n, finite_set [set: pointed_discrete_topology (T n)]) ->
   (forall n, (exists xy : T n * T n, xy.1 != xy.2)) ->
   cantor_like (tree_of T).
@@ -426,7 +444,7 @@ Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
 (* ## Part 4: Building a finitely branching tree to cover `T`                 *)
 (******************************************************************************)
 Section alexandroff_hausdorff.
-Context {R : realType} {T : pseudoMetricType R}.
+Context {R : realType} {T : pseudoPMetricType R}.
 
 Hypothesis cptT : compact [set: T].
 Hypothesis hsdfT : hausdorff_space T.
@@ -506,7 +524,7 @@ HB.instance Definition _ n := gen_choiceMixin (K' n).
 HB.instance Definition _ n := isPointed.Build (K' n) (K'p n).
 
 Let K n := [the pointedType of K' n].
-Let Tree := @tree_of R K.
+Let Tree := @tree_of K.
 
 Let embed_refine n (U : set T) (k : K n) :=
   (if pselect (projT1 k `&` U !=set0)
@@ -566,7 +584,7 @@ Local Lemma cantor_surj_pt2 :
   exists f : {surj [set: cantor_space] >-> [set: Tree]}, continuous f.
 Proof.
 have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f.
-apply: (@cantor_like_finite_prod _ (pointed_discrete_topology \o K)) => [n /=|n].
+apply: (@cantor_like_finite_prod (pointed_discrete_topology \o K)) => [n /=|n].
   have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
   suff -> : [set: {classic K' n}] =
       (@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))).
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
index 239114b4f..9e69ecd16 100644
--- a/theories/function_spaces.v
+++ b/theories/function_spaces.v
@@ -112,7 +112,7 @@ Variable I : Type.
 
 Definition product_topology_def (T : I -> topologicalType) :=
   sup_topology (fun i => Topological.class
-    (weak_topology (fun f : [the pointedType of forall i, T i] => f i))).
+    (weak_topology (fun f : [the choiceType of forall i, T i] => f i))).
 
 HB.instance Definition _ (T : I -> topologicalType) :=
   Topological.copy (prod_topology T) (product_topology_def T).
@@ -155,7 +155,7 @@ Proof.
 move=> f; have /cvg_sup/(_ i)/cvg_image : f --> f by apply: cvg_id.
 move=> h; apply: cvg_trans (h _) => {h}.
   by move=> Q /= [W nbdW <-]; apply: filterS nbdW; exact: preimage_image.
-rewrite eqEsubset; split => y //; exists (dfwith (fun=> point) i y) => //.
+rewrite eqEsubset; split => y //; exists (dfwith f i y) => //.
 by rewrite dfwithin.
 Qed.
 
@@ -204,7 +204,9 @@ Lemma tychonoff (I : eqType) (T : I -> topologicalType)
   (forall i, compact (A i)) ->
   compact [set f : forall i, T i | forall i, A i (f i)].
 Proof.
-move=> Aco; rewrite compact_ultra => F FU FA.
+case: (pselect ([set f : forall i, T i | forall i, A i (f i)] == set0)). 
+  move/eqP => -> _; exact: compact0.
+case/negP/set0P=> a0 Aa0 Aco; rewrite compact_ultra => F FU FA.
 set subst_coord := fun (i : I) (pi : T i) (f : forall x : I, T x) (j : I) =>
   if eqP is ReflectT e then ecast i (T i) (esym e) pi else f j.
 have subst_coordT i pi f : subst_coord i pi f i = pi.
@@ -215,7 +217,7 @@ have subst_coordN i pi f j : i != j -> subst_coord i pi f j = f j.
   by move: inej; rewrite {1}e => /negP.
 have pr_surj i : @^~ i @` [set: forall i, T i] = setT.
   rewrite predeqE => pi; split=> // _.
-  by exists (subst_coord i pi (fun=> point)) => //; rewrite subst_coordT.
+  by exists (subst_coord i pi a0) => //; rewrite subst_coordT.
 pose pF i : set_system _ := [set @^~ i @` B | B in F].
 have pFultra i : UltraFilter (pF i) by exact: ultra_image (pr_surj i).
 have pFA i : pF i (A i).
@@ -227,9 +229,10 @@ have pFA i : pF i (A i).
   by move=> /subst_coordN ->; apply: Af.
 have cvpFA i : A i `&` [set p | pF i --> p] !=set0.
   by rewrite -ultra_cvg_clusterE; apply: Aco.
-exists (fun i => get (A i `&` [set p | pF i --> p])).
-split=> [i|]; first by have /getPex [] := cvpFA i.
-by apply/cvg_sup => i; apply/cvg_image=> //; have /getPex [] := cvpFA i.
+exists (fun i => xget (a0 i) (A i `&` [set p | pF i --> p])).
+split=> [i|]; first by have /(xgetPex (a0 i)) [] := cvpFA i.
+apply/cvg_sup => i; apply/cvg_image=> //. 
+by have /(xgetPex (a0 i)) [] := cvpFA i.
 Qed.
 
 Lemma perfect_prod {I : Type} (i : I) (K : I -> topologicalType) :
@@ -440,13 +443,16 @@ Qed.
 
 Definition arrow_uniform_type : Type := T -> U.
 
-#[export] HB.instance Definition _ := Pointed.on arrow_uniform_type.
+#[export] HB.instance Definition _ := Choice.on arrow_uniform_type.
 #[export] HB.instance Definition _ := isUniform.Build arrow_uniform_type
   fct_ent_filter fct_ent_refl fct_ent_inv fct_ent_split.
 
 #[export] HB.instance Definition _ := Uniform.on arrow_uniform_type.
 End fct_Uniform.
 
+#[export] HB.instance Definition _ {T : choiceType} {U : puniformType} := 
+  Pointed.on (arrow_uniform_type T U).
+
 Lemma cvg_fct_entourageP (T : choiceType) (U : uniformType)
     (F : set_system (arrow_uniform_type T U)) (FF : Filter F)
     (f : arrow_uniform_type T U) :
@@ -597,10 +603,14 @@ split=> [[Q [[/= W oW <- /=] Wf subP]]|[E [entE subP]]].
   case: (oW _ Wf) => ? [ /= E entE] Esub subW.
   exists E; split=> // h Eh; apply/subP/subW/Esub => /= [[u Au]].
   by apply: Eh => /=; rewrite -inE.
-near=> g; apply: subP => y /mem_set Ay; rewrite -!(sigLE A).
+case : (pselect (exists (u : U), True)); first last.
+  move=> nU; apply: (filterS subP); apply: (@filterS _ _ _ setT).
+  by move=> t _ /= y; move: nU; apply: absurd; exists y.
+  exact: filterT.
+case=> u0 _; near=> g; apply: subP => y /mem_set Ay; rewrite -!(sigLE A).
 move: (SigSub _); near: g.
 have := (@cvg_image _ _ (@sigL_arrow _ A V) _ f (nbhs_filter f)
-  (image_sigL point)).1 cvg_id [set h | forall y, E (sigL A f y, h y)].
+  (image_sigL (f u0))).1 cvg_id [set h | forall y, E (sigL A f y, h y)].
 case; first by exists [set fg | forall y, E (fg.1 y, fg.2 y)]; [exists E|].
 move=> B nbhsB rBrE; apply: (filterS _ nbhsB) => g Bg [y yA].
 by move: rBrE; rewrite eqEsubset; case => [+ _]; apply; exists g.
@@ -725,25 +735,6 @@ exists (g u); split; [apply: X'X| apply: Y'Y]; last exact: entourage_refl.
 apply: (C [set fg | forall y, A y -> X' (fg.1 y, fg.2 y)]) => //=.
 by rewrite uniform_entourage; exists X'.
 Qed.
-Lemma uniform_restrict_cvg
-    (F : set_system (U -> V)) (f : U -> V) A : Filter F ->
-  {uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
-Proof.
-move=> FF; rewrite cvg_sigL; split.
-- rewrite -sigLK; move/(cvg_app valL) => D.
-  apply: cvg_trans; first exact: D.
-  move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
-  apply/uniform_nbhs; exists E; split=> //= h /=.
-  rewrite /sigL => R u _; rewrite oinv_set_val.
-  by case: insubP=> /= *; [apply: R|apply: entourage_refl].
-- move/(@cvg_app _ _ _ _ (sigL A)).
-  rewrite -fmap_comp sigL_restrict => D.
-  apply: cvg_trans; first exact: D.
-  move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
-  apply/uniform_nbhs; exists E; split=> //= h /=.
-  rewrite /sigL => R [u Au] _ /=.
-  by have := R u I; rewrite /patch Au.
-Qed.
 
 Lemma uniform_nbhsT (f : U -> V) :
   (nbhs (f : {uniform U -> V})) = nbhs (f : arrow_uniform_type U V).
@@ -817,6 +808,27 @@ Qed.
 
 End UniformCvgLemmas.
 
+Lemma uniform_restrict_cvg {U : choiceType} {V : puniformType}
+    (F : set_system (U -> V)) (f : U -> V) A : Filter F ->
+  {uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
+Proof.
+move=> FF; rewrite cvg_sigL; split.
+- rewrite -sigLK; move/(cvg_app valL) => D.
+  apply: cvg_trans; first exact: D.
+  move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
+  apply/uniform_nbhs; exists E; split=> //= h /=.
+  rewrite /sigL => R u _; rewrite oinv_set_val.
+  by case: insubP=> /= *; [apply: R|apply: entourage_refl].
+- move/(@cvg_app _ _ _ _ (sigL A)).
+  rewrite -fmap_comp sigL_restrict => D.
+  apply: cvg_trans; first exact: D.
+  move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
+  apply/uniform_nbhs; exists E; split=> //= h /=.
+  rewrite /sigL => R [u Au] _ /=.
+  by have := R u I; rewrite /patch Au.
+Qed.
+
+
 Section FamilyConvergence.
 
 Lemma fam_cvgE {U : choiceType} {V : uniformType} (F : set_system (U -> V))
@@ -881,7 +893,7 @@ move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split.
 by move=> g /= gPQ; split; exact: (subset_trans gPQ).
 Qed.
 
-HB.instance Definition _ := Pointed.on compact_openK.
+HB.instance Definition _ := Choice.on compact_openK.
 
 HB.instance Definition _ := hasNbhs.Build compact_openK compact_openK_nbhs.
 
@@ -908,8 +920,6 @@ HB.instance Definition _ :=
 
 End compact_open_setwise.
 
-HB.instance Definition _ := Pointed.on compact_open.
-
 Definition compact_open_def :=
   sup_topology (fun i : sigT (@compact T) =>
     Topological.class (@compact_openK (projT1 i))).
@@ -942,12 +952,19 @@ Qed.
 
 End compact_open.
 
+HB.instance Definition _ {U : topologicalType} {V : ptopologicalType} K := 
+    Pointed.on (@compact_openK U V K).
+
+HB.instance Definition _ {U : topologicalType} {V : ptopologicalType} := 
+  Pointed.on (@compact_open U V).
+
+
 Notation "{ 'compact-open' , U -> V }" := (@compact_open U V).
 Notation "{ 'compact-open' , F --> f }" :=
   (F --> (f : @compact_open _ _)).
 
 Section compact_open_uniform.
-Context {U : topologicalType} {V : uniformType}.
+Context {U : topologicalType} {V : puniformType}.
 
 Let small_ent_sub := @small_set_sub _ (@entourage V).
 
@@ -1029,7 +1046,7 @@ apply/Ff/uniform_nbhs; exists (split_ent (split_ent A))^-1%classic.
 by split; [exact: entourage_inv | move=> g fg; near_simpl; near=> z; exact: fg].
 Unshelve. all: end_near. Qed.
 
-Lemma uniform_limit_continuous_subspace {U : topologicalType} {V : uniformType}
+Lemma uniform_limit_continuous_subspace {U : topologicalType} {V : puniformType}
     (K : set U) (F : set_system (U -> V)) (f : subspace K -> V) :
   ProperFilter F -> (\forall g \near F, continuous (g : subspace K -> V)) ->
   {uniform K, F --> f} -> {within K, continuous f}.
@@ -1085,7 +1102,7 @@ Qed.
 End UniformPointwise.
 
 Section ArzelaAscoli.
-Context {X : topologicalType} {Y : uniformType} {hsdf : hausdorff_space Y}.
+Context {X : topologicalType} {Y : puniformType} {hsdf : hausdorff_space Y}.
 Implicit Types (I : Type).
 
 (** The key condition in Arzela-Ascoli that, like uniform continuity, moves a
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 6eb2297f3..a0875bd09 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -229,13 +229,13 @@ by rewrite opprK.
 Qed.
 
 HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
-    of Num.NormedZmodule R T & PseudoMetric R T := {
+    of Num.NormedZmodule R T & PseudoPointedMetric R T := {
   pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)
 }.
 
 #[short(type="pseudoMetricNormedZmodType")]
 HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
-  {T of Num.NormedZmodule R T & PseudoMetric R T
+  {T of Num.NormedZmodule R T & PseudoPointedMetric R T
    & NormedZmod_PseudoMetric_eq R T}.
 
 Section pseudoMetricnormedzmodule_lemmas.
@@ -2743,17 +2743,25 @@ Lemma continuousZl s a x :
   {for x, continuous s} -> {for x, continuous (fun z => s z *: a)}.
 Proof. by move=> ?; apply: cvgZl. Qed.
 
-Lemma continuousM s t x :
-  {for x, continuous s} -> {for x, continuous t} ->
-  {for x, continuous (s * t)}.
-Proof. by move=> f_cont g_cont; apply: cvgM. Qed.
-
 Lemma continuousV s x : s x != 0 ->
   {for x, continuous s} -> {for x, continuous (fun x => (s x)^-1%R)}.
 Proof. by move=> ?; apply: cvgV. Qed.
 
 End local_continuity.
 
+(* TODO: we need `ptopological` only because need to inherit the semiring structure. 
+         if that is ever fixed upstream, we can eliminate this section *)
+Section local_continuity_ring.
+Context {K : numFieldType} {V : normedModType K} {T : ptopologicalType}.
+Implicit Types (f g : T -> V) (s t : T -> K) (x : T) (k : K) (a : V).
+
+Lemma continuousM s t x :
+  {for x, continuous s} -> {for x, continuous t} ->
+  {for x, continuous (s * t)}.
+Proof. by move=> f_cont g_cont; apply: cvgM. Qed.
+End local_continuity_ring.
+
+
 Section nbhs_ereal.
 Context {R : numFieldType} (P : \bar R -> Prop).
 
@@ -3609,11 +3617,11 @@ Qed.
 
 Definition urysohnType : Type := T.
 
-HB.instance Definition _ := Pointed.on urysohnType.
-
+HB.instance Definition _ := Choice.on urysohnType.
 HB.instance Definition _ :=
   isUniform.Build urysohnType ury_unif_filter ury_unif_refl ury_unif_inv
   ury_unif_split.
+HB.instance Definition _ {p : Pointed T} := Pointed.copy urysohnType (Pointed.Pack p).
 
 Lemma normal_uniform_separator (B : set T) :
   closed A -> closed B -> A `&` B = set0 -> uniform_separator A B.
@@ -4923,7 +4931,7 @@ have : n \in enum_fset D by [].
 by rewrite enum_fsetE => /mapP[/= i iD ->]; exact/le_bigmax.
 Qed.
 
-Lemma rV_compact (T : topologicalType) n (A : 'I_n.+1 -> set T) :
+Lemma rV_compact (T : ptopologicalType) n (A : 'I_n.+1 -> set T) :
   (forall i, compact (A i)) ->
   compact [ set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)].
 Proof.
@@ -5447,7 +5455,7 @@ Notation linear_continuous0 := __deprecated__linear_continuous0 (only parsing).
 Notation linear_bounded0 := __deprecated__linear_bounded0 (only parsing).
 
 Section center_radius.
-Context {R : numDomainType} {M : pseudoMetricType R}.
+Context {R : numDomainType} {M : pseudoPMetricType R}.
 Implicit Types A : set M.
 
 (* NB: the identifier "center" is already taken! *)
diff --git a/theories/sequences.v b/theories/sequences.v
index c24fd7ac7..e72eabe79 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -340,7 +340,7 @@ Section sequences_patched.
 
 Section NatShift.
 
-Variables (N : nat) (V : topologicalType).
+Variables (N : nat) (V : ptopologicalType).
 Implicit Types (f : nat -> V) (u : V ^nat)  (l : V).
 
 Lemma cvg_restrict f u_ l :
@@ -377,7 +377,7 @@ Unshelve. all: by end_near. Qed.
 
 End NatShift.
 
-Variables (V : topologicalType).
+Variables (V : ptopologicalType).
 
 Lemma cvg_shiftS u_ (l : V) :
   ([sequence u_ n.+1]_n @ \oo --> l) = (u_ @ \oo --> l).
diff --git a/theories/topology.v b/theories/topology.v
index 691d1089b..5d2e482ea 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -536,19 +536,43 @@ HB.mixin Record isFiltered U T := {
   nbhs : T -> set_system U
 }.
 
-#[short(type="filteredType")]
-HB.structure Definition Filtered (U : Type) := {T of Pointed T & isFiltered U T}.
+HB.structure Definition JustFiltered U := { T of isFiltered U T }.
+
 Arguments nbhs {_ _} _ _ : simpl never.
+Module UnpointedFiltered.
+#[export] HB.structure Definition Filtered (U:Type) := {T of Choice T & isFiltered U T}.
+Module Exports. HB.reexport. End Exports.
+End UnpointedFiltered.
+Export UnpointedFiltered.Exports.
+
+Module PointedFiltered.
+#[export] HB.structure Definition Filtered (U:Type) := {T of Pointed T & isFiltered U T}.
+Module Exports. HB.reexport. End Exports.
+End PointedFiltered.
+Export PointedFiltered.Exports.
+
 
-Notation "[ 'filteredType' U 'of' T ]" := (Filtered.clone U T _)
-  (at level 0, format "[ 'filteredType'  U  'of'  T ]") : form_scope.
+Notation "'pfilteredType'" := (PointedFiltered.Filtered.type) (at level 0).
+Notation "[ 'pfilteredType' U 'of' T ]" := (PointedFiltered.Filtered.clone U T _)
+  (at level 0, format "[ 'pfilteredType'  U  'of'  T ]").
+
+Declare Scope pointed_filter_scope.
+Notation "'filteredType'" := (PointedFiltered.Filtered.type)
+  (at level 0, format "'filteredType'") : pointed_filter_scope.
+Notation "[ 'filteredType' U 'of' T ]" := (PointedFiltered.Filtered.clone U T _)
+  (at level 0, format "[ 'filteredType'  U  'of'  T ]") : pointed_filter_scope.
+
+Declare Scope unpointed_filter_scope.
+Notation "'filteredType'" := (UnpointedFiltered.Filtered.type)
+  (at level 0, format "'filteredType'") : unpointed_filter_scope.
+Notation "[ 'filteredType' U 'of' T ]" := (UnpointedFiltered.Filtered.clone U T _)
+  (at level 0, format "[ 'filteredType'  U  'of'  T ]") : unpointed_filter_scope.
 
 HB.instance Definition _ T := Equality.on (set_system T).
 HB.instance Definition _ T := Choice.on (set_system T).
 HB.instance Definition _ T := Pointed.on (set_system T).
 HB.instance Definition _ T := isFiltered.Build T (set_system T) id.
 
-Arguments nbhs {_ _} _ _ : simpl never.
 
 HB.mixin Record selfFiltered T := {}.
 
@@ -558,8 +582,39 @@ HB.builders Context T of hasNbhs T.
   HB.instance Definition _ := selfFiltered.Build T.
 HB.end.
 
-#[short(type="nbhsType")]
-HB.structure Definition Nbhs := {T of Pointed T & hasNbhs T}.
+Module UnpointedNbhs.
+#[export] HB.structure Definition Nbhs := {T of Choice T & hasNbhs T}.
+Module Exports. HB.reexport. End Exports.
+End UnpointedNbhs.
+Export UnpointedNbhs.Exports.
+
+Module PointedNbhs.
+#[export] HB.structure Definition Nbhs := {T of Pointed T & hasNbhs T}.
+Module Exports. HB.reexport. End Exports.
+End PointedNbhs.
+Export PointedNbhs.Exports.
+
+
+Notation "'pnbhsType'" := (PointedNbhs.Nbhs.type) (at level 0).
+Notation "[ 'pnbhsType' 'of' T ]" := (PointedNbhs.Nbhs.clone T _)
+  (at level 0, format "[ 'pnbhsType'  'of'  T ]").
+
+Notation "'nbhsType'" := (PointedNbhs.Nbhs.type)
+  (at level 0, format "'nbhsType'") : pointed_filter_scope.
+Notation "[ 'nbhsType' 'of' T ]" := (PointedNbhs.Nbhs.clone T _)
+  (at level 0, format "[ 'nbhsType'  'of'  T ]") : pointed_filter_scope.
+Notation "'Nbhs' T" := (PointedNbhs.Nbhs T)
+  (at level 0, format "'Nbhs'  T") : pointed_filter_scope.
+
+Notation "'nbhsType'" := (UnpointedNbhs.Nbhs.type)
+  (at level 0, format "'nbhsType'") : unpointed_filter_scope.
+Notation "[ 'nbhsType' 'of' T ]" := (UnpointedNbhs.Nbhs.clone T _)
+  (at level 0, format "[ 'nbhsType'  'of'  T ]") : unpointed_filter_scope.
+Notation "'Nbhs' T" := (UnpointedNbhs.Nbhs T)
+  (at level 0, format "'Nbhs'  T") : unpointed_filter_scope.
+
+
+Local Open Scope unpointed_filter_scope.
 
 Definition filter_from {I T : Type} (D : set I) (B : I -> set T) :
   set_system T := [set P | exists2 i, D i & B i `<=` P].
@@ -642,10 +697,10 @@ Proof. by move=> FG GH P /GH /FG. Qed.
 Notation "F --> G" := (cvg_to (nbhs F) (nbhs G)) : classical_set_scope.
 Definition type_of_filter {T} (F : set_system T) := T.
 
-Definition lim_in {U : Type} (T : filteredType U) :=
+Definition lim_in {U : Type} (T : pfilteredType U) :=
   fun F : set_system U => get (fun l : T => F --> l).
 Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T (nbhs F)) : classical_set_scope.
-Definition lim {T : nbhsType} (F : set_system T) := [lim F in T].
+Definition lim {T : pnbhsType} (F : set_system T) := [lim F in T].
 Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope.
 Notation cvg F := (F --> lim F).
 
@@ -669,41 +724,41 @@ move=> xl yk X [[X1 X2] /= [HX1 HX2] H]; exists (X1, X2) => //=.
 split; [exact: xl | exact: yk].
 Qed.
 
-Lemma cvg_in_ex {U : Type} (T : filteredType U) (F : set_system U) :
+Lemma cvg_in_ex {U : Type} (T : pfilteredType U) (F : set_system U) :
   [cvg F in T] <-> (exists l : T, F --> l).
 Proof. by split=> [cvg|/getPex//]; exists [lim F in T]. Qed.
 
-Lemma cvg_ex (T : nbhsType) (F : set_system T) :
+Lemma cvg_ex (T : pnbhsType) (F : set_system T) :
   cvg F <-> (exists l : T, F --> l).
 Proof. exact: cvg_in_ex. Qed.
 
-Lemma cvg_inP {U : Type} (T : filteredType U) (F : set_system U) (l : T) :
+Lemma cvg_inP {U : Type} (T : pfilteredType U) (F : set_system U) (l : T) :
    F --> l -> [cvg F in T].
 Proof. by move=> Fl; apply/cvg_in_ex; exists l. Qed.
 
-Lemma cvgP (T : nbhsType) (F : set_system T) (l : T) : F --> l -> cvg F.
+Lemma cvgP (T : pnbhsType) (F : set_system T) (l : T) : F --> l -> cvg F.
 Proof. exact: cvg_inP. Qed.
 
-Lemma cvg_in_toP {U : Type} (T : filteredType U) (F : set_system U) (l : T) :
+Lemma cvg_in_toP {U : Type} (T : pfilteredType U) (F : set_system U) (l : T) :
    [cvg F in T] -> [lim F in T] = l -> F --> l.
 Proof. by move=> /[swap]->. Qed.
 
-Lemma cvg_toP (T : nbhsType) (F : set_system T) (l : T) :
+Lemma cvg_toP (T : pnbhsType) (F : set_system T) (l : T) :
   cvg F -> lim F = l -> F --> l.
 Proof. exact: cvg_in_toP. Qed.
 
-Lemma dvg_inP {U : Type} (T : filteredType U) (F : set_system U) :
+Lemma dvg_inP {U : Type} (T : pfilteredType U) (F : set_system U) :
   ~ [cvg F in T] -> [lim F in T] = point.
 Proof. by rewrite /lim_in /=; case xgetP. Qed.
 
-Lemma dvgP (T : nbhsType) (F : set_system T) : ~ cvg F -> lim F = point.
+Lemma dvgP (T : pnbhsType) (F : set_system T) : ~ cvg F -> lim F = point.
 Proof. exact: dvg_inP. Qed.
 
-Lemma cvg_inNpoint {U} (T : filteredType U) (F : set_system U) :
+Lemma cvg_inNpoint {U} (T : pfilteredType U) (F : set_system U) :
   [lim F in T] != point -> [cvg F in T].
 Proof. by apply: contra_neqP; apply: dvg_inP. Qed.
 
-Lemma cvgNpoint (T : nbhsType) (F : set_system T) : lim F != point -> cvg F.
+Lemma cvgNpoint (T : pnbhsType) (F : set_system T) : lim F != point -> cvg F.
 Proof. exact: cvg_inNpoint. Qed.
 
 End FilteredTheory.
@@ -1226,11 +1281,11 @@ Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T'
   f =1 g -> (f @ F --> x) = (g @ F --> x).
 Proof. by move=> /funext->. Qed.
 
-Lemma eq_is_cvg_in (T T' : Type) (fT : filteredType T') (F : set_system T) (f g : T -> T') :
+Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') :
   f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
 Proof. by move=> /funext->. Qed.
 
-Lemma eq_is_cvg (T : Type) (T' : nbhsType) (F : set_system T) (f g : T -> T') :
+Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') :
   f =1 g -> cvg (f @ F) = cvg (g @ F).
 Proof. by move=> /funext->. Qed.
 
@@ -1637,7 +1692,7 @@ HB.instance Definition _ := hasNbhs.Build bool principal_filter.
 End PrincipalFilters.
 
 (** Topological spaces *)
-HB.mixin Record Nbhs_isTopological (T : Type) of Nbhs T := {
+HB.mixin Record Nbhs_isTopological (T : Type) of isFiltered T T := {
   open : set_system T;
   nbhs_pfilter_subproof : forall p : T, ProperFilter (nbhs p) ;
   nbhsE_subproof : forall p : T, nbhs p =
@@ -1645,9 +1700,43 @@ HB.mixin Record Nbhs_isTopological (T : Type) of Nbhs T := {
   openE_subproof : open = [set A : set T | A `<=` nbhs^~ A ]
 }.
 
-#[short(type="topologicalType")]
-HB.structure Definition Topological :=
-  {T of Nbhs T & Nbhs_isTopological T}.
+HB.structure Definition JustTopological := {T of Nbhs_isTopological T }.
+
+Module UnpointedTopological.
+#[export] HB.structure Definition Topological := 
+  {T of Choice T & Nbhs_isTopological T & selfFiltered T}.
+Module Exports. HB.reexport. End Exports.
+End UnpointedTopological.
+Export UnpointedTopological.Exports.
+
+Module PointedTopological.
+#[export] HB.structure Definition Topological := {T of Pointed T 
+  & Nbhs_isTopological T & selfFiltered T}.
+Module Exports. HB.reexport. End Exports.
+End PointedTopological.
+Export PointedTopological.Exports.
+
+Notation "'ptopologicalType'" := (PointedTopological.Topological.type) (at level 0).
+Notation "[ 'ptopologicalType' 'of' T ]" := (PointedTopological.Topological.clone T _)
+  (at level 0, format "[ 'ptopologicalType'  'of'  T ]").
+
+Notation "'topologicalType'" := (PointedTopological.Topological.type)
+  (at level 0, format "'topologicalType'") : pointed_filter_scope.
+Notation "[ 'topologicalType' 'of' T ]" := (PointedTopological.Topological.clone T _)
+  (at level 0, format "[ 'topologicalType'  'of'  T ]") : pointed_filter_scope.
+Notation "'Topological' T" := (PointedTopological.Topological T)
+  (at level 0, format "'Topological'  T") : pointed_filter_scope.
+Notation "'Topological.Pack' T" := (PointedTopological.Topological.Pack T)
+  (at level 0, format "'Topological.Pack'  T") : pointed_filter_scope.
+
+Notation "'topologicalType'" := (UnpointedTopological.Topological.type)
+  (at level 0, format "'topologicalType'") : unpointed_filter_scope.
+Notation "[ 'topologicalType' 'of' T ]" := (UnpointedTopological.Topological.clone T _)
+  (at level 0, format "[ 'topologicalType'  'of'  T ]") : unpointed_filter_scope.
+Notation "'Topological' T" := (UnpointedTopological.Topological T)
+  (at level 0, format "'Topological'  T") : unpointed_filter_scope.
+Notation "'Topological.Pack' T" := (UnpointedTopological.Topological.Pack T)
+  (at level 0, format "'Topological.Pack'  T") : unpointed_filter_scope.
 
 Section Topological1.
 
@@ -1833,7 +1922,7 @@ move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous).
 exact: (@cvg_comp _ _ _ _ h _ _ _ fa).
 Qed.
 
-Lemma continuous_is_cvg {T : Type} {V U : topologicalType} [F : set_system T]
+Lemma continuous_is_cvg {T : Type} {V U : ptopologicalType} [F : set_system T]
   (FF : Filter F) (f : T -> V) (h : V -> U) :
   (forall l, f x @[x --> F] --> l -> {for l, continuous h}) ->
   cvg (f x @[x --> F]) -> cvg ((h \o f) x @[x --> F]).
@@ -1861,7 +1950,7 @@ by apply: filterS fFl => _ ->; apply: nbhs_singleton.
 Qed.
 Arguments cvg_near_cst {T U} l {f F FF}.
 
-Lemma is_cvg_near_cst (T : Type) (U : topologicalType)
+Lemma is_cvg_near_cst (T : Type) (U : ptopologicalType)
   (l : U) (f : T -> U) (F : set_system T) {FF : Filter F} :
   (\forall x \near F, f x = l) -> cvg (f @ F).
 Proof. by move=> /cvg_near_cst/cvgP. Qed.
@@ -1883,7 +1972,7 @@ Proof. by apply: cvg_near_cst; near=> x0. Unshelve. all: by end_near. Qed.
 Arguments cvg_cst {U} x {T F FF}.
 #[global] Hint Resolve cvg_cst : core.
 
-Lemma is_cvg_cst (U : topologicalType) (x : U) (T : Type)
+Lemma is_cvg_cst (U : ptopologicalType) (x : U) (T : Type)
   (F : set_system T) {FF : Filter F} :
   cvg ((fun _ : T => x) @ F).
 Proof. by apply: cvgP; apply: cvg_cst. Qed.
@@ -1953,7 +2042,7 @@ Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)).
 
 (** Topology defined by a filter *)
 
-HB.factory Record Nbhs_isNbhsTopological T of Nbhs T := {
+HB.factory Record Nbhs_isNbhsTopological T of isFiltered T T := {
   nbhs_filter : forall p : T, ProperFilter (nbhs p);
   nbhs_singleton : forall (p : T) (A : set T), nbhs p A -> A p;
   nbhs_nbhs : forall (p : T) (A : set T), nbhs p A -> nbhs p (nbhs^~ A);
@@ -1986,7 +2075,7 @@ HB.end.
 Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) :=
   exists B, [/\ op B, B p & B `<=` A].
 
-HB.factory Record Pointed_isOpenTopological T of Pointed T := {
+HB.factory Record isOpenTopological T of Choice T := {
   op : set T -> Prop;
   opT : op setT;
   opI : forall (A B : set T), op A -> op B -> op (A `&` B);
@@ -1994,7 +2083,7 @@ HB.factory Record Pointed_isOpenTopological T of Pointed T := {
     op (\bigcup_i f i);
 }.
 
-HB.builders Context T of Pointed_isOpenTopological T.
+HB.builders Context T of isOpenTopological T.
 
 HB.instance Definition _ := hasNbhs.Build T (nbhs_of_open op).
 
@@ -2031,7 +2120,7 @@ HB.end.
 
 (** Topology defined by a base of open sets *)
 
-HB.factory Record Pointed_isBaseTopological T of Pointed T := {
+HB.factory Record isBaseTopological T of Choice T := {
   I : pointedType;
   D : set I;
   b : I -> (set T);
@@ -2040,7 +2129,7 @@ HB.factory Record Pointed_isBaseTopological T of Pointed T := {
     exists k, [/\ D k, b k t & b k `<=` b i `&` b j];
 }.
 
-HB.builders Context T of Pointed_isBaseTopological T.
+HB.builders Context T of isBaseTopological T.
 
 Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].
 
@@ -2085,7 +2174,7 @@ have /getPex [_ ->] : exists Dj, fop j Dj by have [Dj] := H j; exists Dj.
 by move=> [i]; exists i => //; exists j.
 Qed.
 
-HB.instance Definition _ := Pointed_isOpenTopological.Build T
+HB.instance Definition _ := isOpenTopological.Build T
   open_fromT open_fromI open_from_bigU.
 
 HB.end.
@@ -2197,13 +2286,13 @@ Proof. by rewrite filterI_iter_finI filterI_iterE. Qed.
 
 End filter_supremums.
 
-HB.factory Record Pointed_isSubBaseTopological T of Pointed T := {
-  I : pointedType;
+HB.factory Record isSubBaseTopological T of Choice T := {
+  I : choiceType;
   D : set I;
   b : I -> (set T);
 }.
 
-HB.builders Context T of Pointed_isSubBaseTopological T.
+HB.builders Context T of isSubBaseTopological T.
 
 Local Notation finI_from := (finI_from D b).
 
@@ -2226,7 +2315,7 @@ by move=> [DAi|DBi];
   [have := As; rewrite -AeIbA; apply|have := Bs; rewrite -BeIbB; apply].
 Qed.
 
-HB.instance Definition _ := Pointed_isBaseTopological.Build T
+HB.instance Definition _ := isBaseTopological.Build T
   finI_from_cover finI_from_join.
 
 HB.end.
@@ -2244,7 +2333,7 @@ Let bD : forall i j t, D i -> D j -> b i t -> b j t ->
   exists k, [/\ D k, b k t & b k `<=` b i `&` b j].
 Proof. by move=> i j t _ _ -> ->; exists j. Qed.
 
-HB.instance Definition _ := Pointed_isBaseTopological.Build nat bT bD.
+HB.instance Definition _ := isBaseTopological.Build nat bT bD.
 
 End nat_topologicalType.
 
@@ -2403,7 +2492,7 @@ Qed.
 
 Section matrix_Topology.
 
-Variables (m n : nat) (T : topologicalType).
+Variables (m n : nat) (T : ptopologicalType).
 
 Implicit Types M : 'M[T]_(m, n).
 
@@ -2430,16 +2519,18 @@ Qed.
 HB.instance Definition _ := Nbhs_isNbhsTopological.Build 'M[T]_(m, n)
   mx_nbhs_filter mx_nbhs_singleton mx_nbhs_nbhs.
 
+HB.instance Definition _ := Pointed.on 'M[T]_(m, n).
+
 End matrix_Topology.
 
 (** Weak topology by a function *)
 
-Definition weak_topology {S : pointedType} {T : topologicalType}
+Definition weak_topology {S : choiceType} {T : topologicalType}
   (f : S -> T) : Type := S.
 
 Section Weak_Topology.
 
-Variable (S : pointedType) (T : topologicalType) (f : S -> T).
+Variable (S : choiceType) (T : topologicalType) (f : S -> T).
 Local Notation W := (weak_topology f).
 
 Definition wopen := [set f @^-1` A | A in open].
@@ -2466,9 +2557,9 @@ rewrite predeqE => s; split=> [[i _]|[i _]]; last by rewrite g_preim; exists i.
 by rewrite -[_ _]/((f @^-1` _) _) -g_preim; exists i.
 Qed.
 
-HB.instance Definition _ := Pointed.on W.
+HB.instance Definition _ := Choice.on W.
 HB.instance Definition _ :=
-  Pointed_isOpenTopological.Build W wopT wopI wop_bigU.
+  isOpenTopological.Build W wopT wopI wop_bigU.
 
 Lemma weak_continuous : continuous (f : W -> T).
 Proof. by apply/continuousP => A ?; exists A. Qed.
@@ -2490,22 +2581,25 @@ Qed.
 
 End Weak_Topology.
 
+HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) :=
+  Pointed.on (weak_topology f).
+
 (** Supremum of a family of topologies *)
 
-Definition sup_topology {T : pointedType} {I : Type}
+Definition sup_topology {T : choiceType} {I : Type}
   (Tc : I -> Topological T) : Type := T.
 
 Section Sup_Topology.
 
-Variable (T : pointedType) (I : Type) (Tc : I -> Topological T).
+Variable (T : choiceType) (I : Type) (Tc : I -> Topological T).
 Local Notation S := (sup_topology Tc).
 
 Let TS := fun i => Topological.Pack (Tc i).
 
 Definition sup_subbase := \bigcup_i (@open (TS i) : set_system T).
 
-HB.instance Definition _ := Pointed.on S.
-HB.instance Definition _ := Pointed_isSubBaseTopological.Build S sup_subbase id.
+HB.instance Definition _ := Choice.on S.
+HB.instance Definition _ := isSubBaseTopological.Build S sup_subbase id.
 
 Lemma cvg_sup (F : set_system T) (t : T) :
   Filter F -> F --> (t : S) <-> forall i, F --> (t : TS i).
@@ -2528,6 +2622,9 @@ Qed.
 
 End Sup_Topology.
 
+HB.instance Definition _ (I : Type) (T : pointedType) (f : I -> Topological T) :=
+  Pointed.on (sup_topology f).
+
 (** deleted neighborhood *)
 
 Definition dnbhs {T : topologicalType} (x : T) :=
@@ -2563,7 +2660,7 @@ Lemma cvg_within_filter {T U} {f : T -> U} (F : set_system T) {FF : (Filter F) }
   (G : set_system U) : forall (D : set T), (f @ F) --> G -> (f @ within D F) --> G.
 Proof. move=> ?;  exact: cvg_trans (cvg_fmap2 (cvg_within _)). Qed.
 
-Lemma cvg_app_within {T} {U : topologicalType} (f : T -> U) (F : set_system T)
+Lemma cvg_app_within {T} {U : ptopologicalType} (f : T -> U) (F : set_system T)
   (D : set T): Filter F -> cvg (f @ F) -> cvg (f @ within D F).
 Proof. by move => FF /cvg_ex [l H]; apply/cvg_ex; exists l; exact: cvg_within_filter. Qed.
 
@@ -3250,7 +3347,7 @@ move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)).
 - by move=> _ [?? <-]; apply: finIf.
 Qed.
 
-Lemma filter_finI (T : pointedType) (F : set_system T) (D : set_system T)
+Lemma filter_finI (T : choiceType) (F : set_system T) (D : set_system T)
   (f : set T -> set T) :
   ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f.
 Proof.
@@ -3297,6 +3394,11 @@ Definition closed_fam_of (A : set T) I (D : set I) (f : I -> set T) :=
   exists2 g : I -> set T, (forall i, D i -> closed (g i)) &
     forall i, D i -> f i = A `&` g i.
 
+End Covers.
+
+Section PCovers.
+
+Variable T : ptopologicalType.
 Lemma compact_In0 :
   compact = [set A | forall (I : choiceType) (D : set I) (f : I -> set T),
     closed_fam_of A D f -> finI D f -> \bigcap_(i in D) f i !=set0].
@@ -3317,7 +3419,7 @@ exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA.
 by have /AclFIp [_] := FB; move=> /(_ _ p_C).
 Qed.
 
-Lemma compact_cover : compact = cover_compact.
+Lemma compact_cover : compact = @cover_compact T.
 Proof.
 rewrite compact_In0 cover_compactE predeqE => A.
 split=> [Aco I D f [g gop feAg] fcov|Aco I D f [g gcl feAg]].
@@ -3362,7 +3464,7 @@ have /Ifp := D'k; rewrite feAg; last by have /sD := D'k; rewrite inE.
 by move=> [/sAnfcov [i D'i [_ nfip]] _]; have /Ifp := D'i.
 Qed.
 
-End Covers.
+End PCovers.
 
 Lemma finite_compact {X : topologicalType} (A : set X) :
   finite_set A -> compact A.
@@ -3372,7 +3474,7 @@ case/finite_setP=> n; elim: n A => [A|n ih A /eq_cardSP[x Ax /ih ?]].
 by rewrite -(setD1K Ax); apply: compactU => //; exact: compact_set1.
 Qed.
 
-Lemma clopen_countable {T : topologicalType}:
+Lemma clopen_countable {T : ptopologicalType}:
   compact [set: T] -> @second_countable T -> countable (@clopen T).
 Proof.
 move=> cmpT [B /fset_subset_countable cntB] [obase Bbase].
@@ -3500,16 +3602,6 @@ Lemma close_refl x : close x x.
 Proof. exact: (@cvg_close (nbhs x)). Qed.
 Hint Resolve close_refl : core.
 
-Lemma close_cvg (F1 F2 : set_system T) {FF2 : ProperFilter F2} :
-  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
-Proof.
-move=> F12 F21.
-have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
-  by apply: (@cvg_close F2) => //; apply: cvgP F2l.
-have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
-rewrite dvgP // dvgP //; exact/close_refl.
-Qed.
-
 Lemma cvgx_close x y : x --> y -> close x y.
 Proof. exact: cvg_close. Qed.
 
@@ -3576,31 +3668,10 @@ Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
 Lemma cvg_eq x y : x --> y -> x = y.
 Proof. by rewrite -closeE //; apply: cvg_close. Qed.
 
-Lemma lim_id x : lim (nbhs x) = x.
-Proof. by apply/esym/cvg_eq/cvg_ex; exists x. Qed.
-
-Lemma cvg_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) :
-  f @ F --> l -> lim (f @ F) = l.
-Proof. by move=> /[dup] /cvgP /cvg_unique; apply. Qed.
-
-Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) :
-   (\forall x \near F, f x = l) -> lim (f @ F) = l.
-Proof. by move=> /cvg_near_cst/cvg_lim. Qed.
-
-Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) :
-   lim ((fun _ : U => k) @ F) = k.
-Proof. by apply: cvg_lim; apply: cvg_cst. Qed.
-
 Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
   {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
 Proof. by move=> ffun fx fy; rewrite -closeE //; exact: cvgi_close. Qed.
 
-Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
-  F (fun x : U => is_subset1 (f x)) ->
-  f `@ F --> l -> lim (f `@ F) = l.
-Proof.
-move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
-Qed.
 
 Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular_space}.
 Proof.
@@ -3625,6 +3696,46 @@ Qed.
 
 End separated_topologicalType.
 
+Section separated_ptopologicalType.
+Variable T : ptopologicalType.
+Implicit Types x y : T.
+
+Lemma close_cvg (F1 F2 : set_system T) {FF2 : ProperFilter F2} :
+  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
+Proof.
+move=> F12 F21.
+have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1).
+  by apply: (@cvg_close _ F2) => //; apply: cvgP F2l.
+have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
+rewrite dvgP // dvgP //; exact/close_refl.
+Qed.
+
+Hypothesis sep : hausdorff_space T.
+
+Lemma lim_id x : lim (nbhs x) = x.
+Proof. by apply/esym/cvg_eq/cvg_ex => //; exists x. Qed.
+
+Lemma cvg_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) :
+  f @ F --> l -> lim (f @ F) = l.
+Proof. by move=> /[dup] /cvgP /cvg_unique; apply. Qed.
+
+Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) :
+   (\forall x \near F, f x = l) -> lim (f @ F) = l.
+Proof. by move=> /cvg_near_cst/cvg_lim. Qed.
+
+Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) :
+   lim ((fun _ : U => k) @ F) = k.
+Proof. by apply: cvg_lim; apply: cvg_cst. Qed.
+
+Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
+  F (fun x : U => is_subset1 (f x)) ->
+  f `@ F --> l -> lim (f `@ F) = l.
+Proof.
+move=> f_prop fl; apply: get_unique => // l' fl'; exact: cvgi_unique _ fl' fl.
+Qed.
+
+End separated_ptopologicalType.
+
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")]
 Notation cvg_map_lim := cvg_lim (only parsing).
 #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgi_lim`")]
@@ -3997,7 +4108,7 @@ Lemma nbhs_E {T T'} (ent : set_system (T * T')) x :
   nbhs_ ent x = filter_from ent (fun A => to_set A x).
 Proof. by []. Qed.
 
-HB.mixin Record Nbhs_isUniform_mixin M of Nbhs M := {
+HB.mixin Record Nbhs_isUniform_mixin M of isFiltered M M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
   entourage_refl_subproof : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
@@ -4007,11 +4118,46 @@ HB.mixin Record Nbhs_isUniform_mixin M of Nbhs M := {
   nbhsE_subproof : nbhs = nbhs_ entourage;
 }.
 
-#[short(type="uniformType")]
-HB.structure Definition Uniform :=
-  {T of Topological T & Nbhs_isUniform_mixin T}.
+HB.structure Definition JustUniform := {M of Nbhs_isUniform_mixin M}.
+
+Module UnpointedUniform.
+#[export] HB.structure Definition Uniform := 
+  {T of UnpointedTopological.Topological T & Nbhs_isUniform_mixin T}.
+Module Exports. HB.reexport. End Exports.
+End UnpointedUniform.
+Export UnpointedUniform.Exports.
 
-HB.factory Record Nbhs_isUniform M of Nbhs M := {
+Module PointedUniform.
+#[export] HB.structure Definition Uniform := 
+  {T of PointedTopological.Topological T & Nbhs_isUniform_mixin T}.
+Module Exports. HB.reexport. End Exports.
+End PointedUniform.
+Export PointedUniform.Exports.
+
+Notation "'puniformType'" := (PointedUniform.Uniform.type) (at level 0).
+Notation "[ 'puniformType' 'of' T ]" := (PointedUniform.Uniform.clone T _)
+  (at level 0, format "[ 'puniformType'  'of'  T ]").
+
+Notation "'uniformType'" := (PointedUniform.Uniform.type)
+  (at level 0, format "'uniformType'") : pointed_filter_scope.
+Notation "[ 'uniformType' 'of' T ]" := (PointedUniform.Uniform.clone T _)
+  (at level 0, format "[ 'uniformType'  'of'  T ]") : pointed_filter_scope.
+Notation "'Uniform' T" := (PointedUniform.Uniform T)
+  (at level 0, format "'Uniform'  T") : pointed_filter_scope.
+Notation "'Uniform.Pack' T" := (PointedUniform.Uniform.Pack T)
+  (at level 0, format "'Uniform.Pack'  T") : pointed_filter_scope.
+
+Notation "'uniformType'" := (UnpointedUniform.Uniform.type)
+  (at level 0, format "'uniformType'") : unpointed_filter_scope.
+Notation "[ 'uniformType' 'of' T ]" := (UnpointedUniform.Uniform.clone T _)
+  (at level 0, format "[ 'uniformType'  'of'  T ]") : unpointed_filter_scope.
+Notation "'Uniform' T" := (UnpointedUniform.Uniform T)
+  (at level 0, format "'Uniform'  T") : unpointed_filter_scope.
+Notation "'Uniform.Pack' T" := (UnpointedUniform.Uniform.Pack T)
+  (at level 0, format "'Uniform.Pack'  T") : unpointed_filter_scope.
+
+
+HB.factory Record Nbhs_isUniform M of isFiltered M M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
   entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
@@ -4055,7 +4201,7 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build M
 
 HB.end.
 
-HB.factory Record isUniform M of Pointed M := {
+HB.factory Record isUniform M of Choice M := {
   entourage : set_system (M * M);
   entourage_filter : Filter entourage;
   entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
@@ -4101,16 +4247,16 @@ move=> FF; split => /=.
 Qed.
 
 Section uniformType1.
-Context {M : uniformType}.
+
+Variable M : uniformType.
 
 Lemma entourage_refl (A : set (M * M)) x :
   entourage A -> A (x, x).
 Proof. by move=> entA; apply: entourage_refl_subproof entA _ _. Qed.
 
-Global Instance entourage_pfilter : ProperFilter (@entourage M).
+Global Instance entourage_filter' : Filter (@entourage M).
 Proof.
-apply Build_ProperFilter; last exact: entourage_filter.
-by move=> A entA; exists (point, point); apply: entourage_refl.
+exact: entourage_filter.
 Qed.
 
 Lemma entourageT : entourage [set: M * M].
@@ -4169,6 +4315,12 @@ Qed.
 
 End uniformType1.
 
+Global Instance entourage_pfilter {M : puniformType} : ProperFilter (@entourage M).
+Proof.
+apply Build_ProperFilter; last exact: entourage_filter.
+by move=> A entA; exists (point, point); apply: entourage_refl.
+Qed.
+
 #[global]
 Hint Extern 0 (entourage (split_ent _)) => exact: entourage_split_ent : core.
 #[global]
@@ -4211,7 +4363,7 @@ Lemma countable_uniformityP {T : uniformType} :
     (forall n, entourage (f n)).
 Proof.
 split=> [[M []]|[f fsubE entf]].
-  move=> /pfcard_geP[-> _ /(_ _ entourageT)[]//|/unsquash f eM Msub].
+  move=> /pfcard_geP[-> _ /(_ _ (@entourageT _))[]//|/unsquash f eM Msub].
   exists f; last by move=> n; apply: eM; exact: funS.
   by move=> ? /Msub [Q + ?] => /(@surj _ _ _ _ f)[n _ fQ]; exists n; rewrite fQ.
 exists (range f); split; first exact: card_image_le.
@@ -4256,7 +4408,9 @@ apply: (entourage_split x) => //.
 by have := cxy _ (entourage_inv (entourage_split_ent entA)).
 Qed.
 
-Lemma cvg_closeP (F : set_system U) (l : U) : ProperFilter F ->
+End uniform_closeness.
+
+Lemma cvg_closeP { U : puniformType} (F : set_system U) (l : U) : ProperFilter F ->
   F --> l <-> ([cvg F in U] /\ close (lim F) l).
 Proof.
 move=> FF; split=> [Fl|[cvF]Cl].
@@ -4264,7 +4418,6 @@ move=> FF; split=> [Fl|[cvF]Cl].
 by apply: cvg_trans (close_cvgxx Cl).
 Qed.
 
-End uniform_closeness.
 
 Definition unif_continuous (U V : uniformType) (f : U -> V) :=
   (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.
@@ -4291,7 +4444,7 @@ Qed.
 
 Lemma prod_ent_filter : Filter prod_ent.
 Proof.
-have prodF := filter_prod_filter (@entourage_pfilter U) (@entourage_pfilter V).
+have prodF := filter_prod_filter (@entourage_filter U) (@entourage_filter V).
 split; rewrite /prod_ent; last 1 first.
 - by move=> A B sAB /=; apply: filterS => ? [xy /sAB ??]; exists xy.
 - by rewrite -setMTT; apply: prod_entP filterT filterT.
@@ -4356,7 +4509,7 @@ End prod_Uniform.
 
 Section matrix_Uniform.
 
-Variables (m n : nat) (T : uniformType).
+Variables (m n : nat) (T : puniformType).
 
 Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)).
 
@@ -4422,7 +4575,7 @@ HB.instance Definition _ := Nbhs_isUniform.Build 'M[T]_(m, n)
 
 End matrix_Uniform.
 
-Lemma cvg_mx_entourageP (T : uniformType) m n (F : set_system 'M[T]_(m,n))
+Lemma cvg_mx_entourageP (T : puniformType) m n (F : set_system 'M[T]_(m,n))
   (FF : Filter F) (M : 'M[T]_(m,n)) :
   F --> M <->
   forall A, entourage A -> \forall N \near F,
@@ -4446,7 +4599,7 @@ Definition map_pair {S U} (f : S -> U) (x : (S * S)) : (U * U) :=
 
 Section weak_uniform.
 
-Variable (pS : pointedType) (U : uniformType) (f : pS -> U).
+Variable (pS : choiceType) (U : uniformType) (f : pS -> U).
 
 Let S := weak_topology f.
 
@@ -4496,6 +4649,10 @@ HB.instance Definition _ := @Nbhs_isUniform.Build (weak_topology f) (*S nbhs*)
 
 End weak_uniform.
 
+HB.instance Definition _ (pS : pointedType) (U : uniformType) (f : pS -> U) :=
+  Pointed.on (weak_topology f).
+
+
 Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) :=
   exists2 B, entourage B & forall PQ, A PQ -> forall p q,
     PQ.1 p -> PQ.2 q -> B (p,q).
@@ -4504,7 +4661,7 @@ Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) :=
 
 Section sup_uniform.
 
-Variable (T : pointedType) (Ii : Type) (Tc : Ii -> Uniform T).
+Variable (T : choiceType) (Ii : Type) (Tc : Ii -> Uniform T).
 
 Let I : choiceType := {classic Ii}.
 Let TS := fun i => Uniform.Pack (Tc i).
@@ -4523,8 +4680,19 @@ Ltac IEntP := move=> [[ /= + + /[dup] /asboolP]].
 
 Definition sup_ent_filter : Filter sup_ent.
 Proof.
-apply: finI_filter; move=> J JsubEnt /=; exists (point, point).
-by IEntP => i b /= /entourage_refl ? ? _.
+case: (pselect (exists t:T, True)).
+  case => p _; apply: finI_filter; move=> J JsubEnt /=; exists (p, p).
+  by IEntP => i b /= /entourage_refl ? ? _.
+move=> empT. 
+have TT0 (E : set (T*T)) : E = set0.
+  rewrite eqEsubset; split => //=; case=> t ? _; move: empT. 
+  by apply: absurd; exists t.
+have ent0 : sup_ent set0.
+  rewrite -(TT0 setT); exists set0 => //=; exists fset0 => //=.
+split.
+- rewrite (TT0 setT); exact: ent0.
+- by move => P Q ? ?; rewrite (TT0 (P `&` Q)).
+- by move=> P Q _ _; rewrite (TT0 Q).
 Qed.
 
 Lemma sup_ent_refl A : sup_ent A -> [set fg | fg.1 = fg.2] `<=` A.
@@ -4656,7 +4824,8 @@ Lemma entourage_E {R : numDomainType} {T T'} (ball : T -> R -> set T') :
   @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]).
 Proof. by []. Qed.
 
-HB.mixin Record Uniform_isPseudoMetric (R : numDomainType) M of Uniform M := {
+HB.mixin Record Uniform_isPseudoMetric (R : numDomainType) M of 
+    Nbhs_isUniform_mixin M & isFiltered M M := {
   ball : M -> R -> M -> Prop ;
   ball_center_subproof : forall x (e : R), 0 < e -> ball x e x ;
   ball_sym_subproof : forall x y (e : R), ball x e y -> ball y e x ;
@@ -4665,9 +4834,43 @@ HB.mixin Record Uniform_isPseudoMetric (R : numDomainType) M of Uniform M := {
   entourageE_subproof : entourage = entourage_ ball
 }.
 
-#[short(type="pseudoMetricType")]
-HB.structure Definition PseudoMetric (R : numDomainType) :=
-  {T of Uniform T & Uniform_isPseudoMetric R T}.
+HB.structure Definition JustPseudoMetric R := {M of Uniform_isPseudoMetric R M}.
+
+Module UnpointedPseudoMetric.
+#[export] HB.structure Definition PseudoMetric (R : numDomainType) := 
+  {T of UnpointedUniform.Uniform T & Uniform_isPseudoMetric R T}.
+Module Exports. HB.reexport. End Exports.
+End UnpointedPseudoMetric.
+Export UnpointedPseudoMetric.Exports.
+
+Module PointedPseudoMetric.
+#[export] HB.structure Definition PseudoMetric (R : numDomainType) := 
+  {T of PointedUniform.Uniform T & Uniform_isPseudoMetric R T}.
+Module Exports. HB.reexport. End Exports.
+End PointedPseudoMetric.
+Export PointedPseudoMetric.Exports.
+
+Notation "'ppseudoMetricType'" := (PointedPseudoMetric.PseudoMetric.type) (at level 0).
+Notation "[ 'ppseudoMetricType' R 'of' T ]" := (PointedPseudoMetric.PseudoMetric.clone R T _)
+  (at level 0, format "[ 'ppseudoMetricType'  R  'of'  T ]").
+
+Notation "'pseudoMetricType'" := (PointedPseudoMetric.PseudoMetric.type)
+  (at level 0, format "'pseudoMetricType'") : pointed_filter_scope.
+Notation "[ 'pseudoMetricType' R 'of' T ]" := (PointedPseudoMetric.PseudoMetric.clone R T _)
+  (at level 0, format "[ 'pseudoMetricType'  R  'of'  T ]") : pointed_filter_scope.
+Notation "'PseudoMetric' T" := (PointedPseudoMetric.PseudoMetric T)
+  (at level 0, format "'PseudoMetric'  T") : pointed_filter_scope.
+Notation "'PseudoMetric.Pack' T" := (PointedPseudoMetric.PseudoMetric.Pack T)
+  (at level 0, format "'PseudoMetric.Pack'  T") : pointed_filter_scope.
+
+Notation "'pseudoMetricType'" := (UnpointedPseudoMetric.PseudoMetric.type)
+  (at level 0, format "'pseudoMetricType'") : unpointed_filter_scope.
+Notation "[ 'pseudoMetricType' R 'of' T ]" := (UnpointedPseudoMetric.PseudoMetric.clone R T _)
+  (at level 0, format "[ 'pseudoMetricType'  R  'of'  T ]") : unpointed_filter_scope.
+Notation "'PseudoMetric' T" := (UnpointedPseudoMetric.PseudoMetric T)
+  (at level 0, format "'PseudoMetric'  T") : unpointed_filter_scope.
+Notation "'PseudoMetric.Pack' T" := (UnpointedPseudoMetric.PseudoMetric.Pack T)
+  (at level 0, format "'PseudoMetric.Pack'  T") : unpointed_filter_scope.
 
 Definition discrete_topology T (dsc : discrete_space T) : Type := T.
 
@@ -4692,13 +4895,14 @@ by rewrite set_compose_diag => x [i _ <-]; apply: dA; exists i.
 Qed.
 
 HB.instance Definition _ := Choice.on (discrete_topology dsc).
-HB.instance Definition _ := Pointed.on (discrete_topology dsc).
 HB.instance Definition _ := discrete_uniform_mixin.
 
 End discrete_uniform.
 
+HB.instance Definition _ {T : pnbhsType} {dsc: discrete_space T} := Pointed.on (discrete_topology dsc).
+
 (* was uniformityOfBallMixin *)
-HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := {
+HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of isFiltered M M := {
   ent : set_system (M * M);
   nbhsE : nbhs = nbhs_ ent;
   ball : M -> R -> M -> Prop ;
@@ -4765,8 +4969,8 @@ Proof. by rewrite entourageE_subproof. Qed.
 Lemma entourage_from_ballE {R : numDomainType} {M : pseudoMetricType R} :
   @filter_from R _ [set x : R | 0 < x]
     (fun e => [set xy | @ball R M xy.1 e xy.2]) = entourage.
-Proof. by rewrite -entourage_ballE. Qed.
 
+Proof. by rewrite -entourage_ballE. Qed.
 Lemma entourage_ball {R : numDomainType} (M : pseudoMetricType R)
   (e : {posnum R}) : entourage [set xy : M * M | ball xy.1 e%:num xy.2].
 Proof. by rewrite -entourage_ballE; exists e%:num => /=. Qed.
@@ -4778,10 +4982,12 @@ Definition nbhs_ball_ {R : numDomainType} {T T'} (ball : T -> R -> set T')
 Definition nbhs_ball {R : numDomainType} {M : pseudoMetricType R} :=
   nbhs_ball_ (@ball R M).
 
-Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : (@nbhs_ball R M) = nbhs.
+Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : 
+  (@nbhs_ball R M) = nbhs.
 Proof.
 rewrite predeq2E => x P; rewrite -nbhs_entourageE; split.
-  by move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2].
+  move=> [_/posnumP[e] sbxeP]; exists [set xy | ball xy.1 e%:num xy.2].
+  simple apply (entourage_ball).
 rewrite -entourage_ballE; move=> [A [e egt0 sbeA] sAP].
 by exists e => // ??; apply/sAP/sbeA.
 Qed.
@@ -4834,12 +5040,6 @@ move=> le12 y. case: comparableP le12 => [lte12 _|//|//|->//].
 by rewrite -[e2](subrK e1); apply/ball_triangle/ballxx; rewrite subr_gt0.
 Qed.
 
-Global Instance entourage_proper_filter : ProperFilter (@entourage M).
-Proof.
-apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA].
-by exists (point, point); apply: sbeA; apply: ballxx.
-Qed.
-
 Lemma near_ball (y : M) (eps : R) : 0 < eps -> \forall y' \near y, ball y eps y'.
 Proof. exact: nbhsx_ballx. Qed.
 
@@ -4894,6 +5094,14 @@ Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y :
 Proof. by move/cvgi_ballP. Qed.
 
 End pseudoMetricType_numDomainType.
+
+Global Instance entourage_proper_filter {R : numDomainType} {M : ppseudoMetricType R} :
+  ProperFilter (@entourage M).
+Proof.
+apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA].
+by exists (point, point); apply: sbeA; apply: ballxx.
+Qed.
+
 #[global] Hint Resolve nbhsx_ballx : core.
 #[global] Hint Resolve close_refl : core.
 Arguments close_cvg {T} F1 F2 {FF2} _.
@@ -4984,7 +5192,7 @@ Qed.
 
 (** matrices *)
 Section matrix_PseudoMetric.
-Variables (m n : nat) (R : numDomainType) (T : pseudoMetricType R).
+Variables (m n : nat) (R : numDomainType) (T : pseudoPMetricType R).
 Implicit Types x y : 'M[T]_(m, n).
 Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j).
 Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x.
@@ -5001,7 +5209,8 @@ Lemma mx_entourage : entourage = entourage_ mx_ball.
 Proof.
 rewrite predeqE=> A; split; last first.
   move=> [_/posnumP[e] sbeA].
-  by exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]).
+  exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]) => //= _ _.
+  by rewrite -entourage_ballE; exists e%:num => //=.
 move=> [P]; rewrite -entourage_ballE => entP sPA.
 set diag := fun (e : {posnum R}) => [set xy : T * T | ball xy.1 e%:num xy.2].
 exists (\big[Num.min/1%:pos]_i \big[Num.min/1%:pos]_j xget 1%:pos
@@ -5022,7 +5231,6 @@ End matrix_PseudoMetric.
 Section prod_PseudoMetric.
 Context {R : numDomainType} {U V : pseudoMetricType R}.
 Implicit Types (x y : U * V).
-Definition prod_point : U * V := (point, point).
 Definition prod_ball x (eps : R) y :=
   ball (fst x) eps (fst y) /\ ball (snd x) eps (snd y).
 Lemma prod_ball_center x (eps : R) : 0 < eps -> prod_ball x eps x.
@@ -5081,6 +5289,7 @@ Definition quotient_topology (T : topologicalType) (Q : quotType T) : Type := Q.
 
 Section quotients.
 Local Open Scope quotient_scope.
+Section unpointed.
 Context {T : topologicalType} {Q0 : quotType T}.
 
 Local Notation Q := (quotient_topology Q0).
@@ -5088,12 +5297,11 @@ Local Notation Q := (quotient_topology Q0).
 HB.instance Definition _ := Quotient.copy Q Q0.
 HB.instance Definition _ := [Sub Q of T by %/].
 HB.instance Definition _ := [Choice of Q by <:].
-HB.instance Definition _ := isPointed.Build Q (\pi_Q point : Q).
 
 Definition quotient_open U := open (\pi_Q @^-1` U).
 
 Program Definition quotient_topologicalType_mixin :=
-  @Pointed_isOpenTopological.Build Q quotient_open _ _ _.
+  @isOpenTopological.Build Q quotient_open _ _ _.
 Next Obligation. by rewrite /quotient_open preimage_setT; exact: openT. Qed.
 Next Obligation. by move=> ? ? ? ?; exact: openI. Qed.
 Next Obligation. by move=> I f ofi; apply: bigcup_open => i _; exact: ofi. Qed.
@@ -5119,8 +5327,16 @@ have greprE x : g (repr (\pi_Q x)) = g x by apply/eqP; rewrite rgE// reprK.
 by rewrite eqEsubset; split => x /=; rewrite greprE.
 Qed.
 
+End unpointed.
+
+Section pointed.
+Context {T : ptopologicalType} {Q0 : quotType T}.
+Local Notation Q := (quotient_topology Q0).
+HB.instance Definition _ := isPointed.Build Q (\pi_Q point : Q).
+End pointed.
 End quotients.
 
+
 Section discrete_pseudoMetric.
 Context {R : numDomainType} {T : nbhsType} {dsc : discrete_space T}.
 
@@ -5153,7 +5369,7 @@ Definition pseudoMetric_bool {R : realType} :=
 
 Definition cauchy {T : uniformType} (F : set_system T) := (F, F) --> entourage.
 
-Lemma cvg_cauchy {T : uniformType} (F : set_system T) : Filter F ->
+Lemma cvg_cauchy {T : puniformType} (F : set_system T) : Filter F ->
   [cvg F in T] -> cauchy F.
 Proof.
 move=> FF cvF A entA; have /entourage_split_ex [B entB sB2A] := entA.
@@ -5163,7 +5379,7 @@ exists (to_set ((B^-1)%classic) (lim F), to_set B (lim F)).
 by move=> ab [/= Balima Blimb]; apply: sB2A; exists (lim F).
 Qed.
 
-HB.mixin Record Uniform_isComplete T of Uniform T := {
+HB.mixin Record Uniform_isComplete T of PointedUniform T := {
   cauchy_cvg :
     forall (F : set_system T), ProperFilter F -> cauchy F -> cvg F
 }.
@@ -5251,7 +5467,7 @@ Arguments cauchyP {R T} F {PF}.
 
 #[short(type="completePseudoMetricType")]
 HB.structure Definition CompletePseudoMetric R :=
-  {T of Complete T & PseudoMetric R T}.
+  {T of Complete T & PseudoPointedMetric R T}.
 
 HB.instance Definition _ (R : numFieldType) (T : completePseudoMetricType R)
   (m n : nat) := Uniform_isComplete.Build 'M[T]_(m, n) cauchy_cvg.
@@ -5259,7 +5475,7 @@ HB.instance Definition _ (R : numFieldType) (T : completePseudoMetricType R)
 
 HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.
 
-Lemma compact_cauchy_cvg {T : uniformType} (U : set T) (F : set_system T) :
+Lemma compact_cauchy_cvg {T : puniformType} (U : set T) (F : set_system T) :
   ProperFilter F -> cauchy F -> F U -> compact U -> cvg F.
 Proof.
 move=> PF cf FU /(_ F PF FU) [x [_ clFx]]; apply: (cvgP x).
@@ -5341,22 +5557,22 @@ HB.instance Definition _ (R : numFieldType) :=
 Module numFieldTopology.
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : realType) := PseudoMetric.copy R R^o.
+HB.instance Definition _ (R : realType) := PseudoPointedMetric.copy R R^o.
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : rcfType) := PseudoMetric.copy R R^o.
+HB.instance Definition _ (R : rcfType) := PseudoPointedMetric.copy R R^o.
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : archiFieldType) := PseudoMetric.copy R R^o.
+HB.instance Definition _ (R : archiFieldType) := PseudoPointedMetric.copy R R^o.
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : realFieldType) := PseudoMetric.copy R R^o.
+HB.instance Definition _ (R : realFieldType) := PseudoPointedMetric.copy R R^o.
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : numClosedFieldType) := PseudoMetric.copy R R^o.
+HB.instance Definition _ (R : numClosedFieldType) := PseudoPointedMetric.copy R R^o.
 
 #[export, non_forgetful_inheritance]
-HB.instance Definition _ (R : numFieldType) := PseudoMetric.copy R R^o.
+HB.instance Definition _ (R : numFieldType) := PseudoPointedMetric.copy R R^o.
 
 Module Exports. HB.reexport. End Exports.
 
@@ -5454,7 +5670,7 @@ by exists (nat_of_rat \o f) => i j Di Dj /inj_nat_of_rat/inj_f; exact.
 Qed.
 
 Section weak_pseudoMetric.
-Context {R : realType} (pS : pointedType) (U : pseudoMetricType R) .
+Context {R : realType} (pS : choiceType) (U : pseudoMetricType R) .
 Variable (f : pS -> U).
 
 Notation S := (weak_topology f).
@@ -5498,7 +5714,7 @@ Proof. by []. Qed.
 
 End weak_pseudoMetric.
 
-Lemma compact_second_countable {R : realType} {T : pseudoMetricType R} :
+Lemma compact_second_countable {R : realType} {T : pseudoPMetricType R} :
   compact [set: T] -> @second_countable T.
 Proof.
 have npos n : (0:R) < n.+1%:R^-1 by [].
@@ -5524,7 +5740,7 @@ pose B := \bigcup_n (f n) @` [set` h'' n]; exists B;[|split].
   by apply: (le_ball (ltW deleps)); apply: interior_subset.
 Qed.
 
-Lemma clopen_surj {R : realType} {T : pseudoMetricType R} :
+Lemma clopen_surj {R : realType} {T : pseudoPMetricType R} :
   compact [set: T] -> $|{surjfun [set: nat] >-> @clopen T}|.
 Proof.
 move=> cmptT.
@@ -5843,6 +6059,7 @@ Definition type : Type := let _ := countableBase in let _ := entF in T.
 #[export] HB.instance Definition _ := Uniform.on type.
 #[export] HB.instance Definition _ := Uniform_isPseudoMetric.Build R type
   step_ball_center step_ball_sym step_ball_triangle step_ball_entourage.
+#[export] HB.instance Definition _ {q : Pointed T} := Pointed.copy type (Pointed.Pack q).
 
 Lemma countable_uniform_bounded (x y : T) :
   let U := [the pseudoMetricType R of type]
@@ -5855,17 +6072,19 @@ by apply/andP; split => //; rewrite invf_lt1 //= ltrDl.
 Qed.
 
 End countable_uniform.
+
+
 Module Exports. HB.reexport. End Exports.
 End countable_uniform.
 Export countable_uniform.Exports.
 
 Notation countable_uniform := countable_uniform.type.
 
-Definition sup_pseudometric (R : realType) (T : pointedType) (Ii : Type)
+Definition sup_pseudometric (R : realType) (T : choiceType) (Ii : Type)
   (Tc : Ii -> PseudoMetric R T) (Icnt : countable [set: Ii]) : Type := T.
 
 Section sup_pseudometric.
-Variable (R : realType) (T : pointedType) (Ii : Type).
+Variable (R : realType) (T : choiceType) (Ii : Type).
 Variable (Tc : Ii -> PseudoMetric R T).
 
 Hypothesis Icnt : countable [set: Ii].
@@ -5921,8 +6140,6 @@ Qed.
 
 HB.instance Definition _ := Choice.copy (subspace A) _.
 
-HB.instance Definition _ := isPointed.Build (subspace A) point.
-
 HB.instance Definition _ := hasNbhs.Build (subspace A) nbhs_subspace.
 
 Lemma nbhs_subspaceP (x : subspace A) :
@@ -6122,6 +6339,7 @@ by move=> ?; exists (P, Q).
 Qed.
 End SubspaceOpen.
 
+
 Lemma compact_subspaceIP (U : set T) :
   compact (U `&` A : set (subspace A)) <-> compact (U `&` A : set T).
 Proof.
@@ -6153,6 +6371,9 @@ Qed.
 
 End Subspace.
 
+HB.instance Definition _ {T : ptopologicalType} (A : set T) := isPointed.Build (subspace A) point.
+
+
 Global Instance subspace_filter {T : topologicalType}
      (A : set T) (x : subspace A) :
    Filter (nbhs_subspace x) := nbhs_subspace_filter x.
@@ -6408,7 +6629,7 @@ HB.instance Definition _ :=
 End SubspacePseudoMetric.
 
 Section SubspaceWeak.
-Context {T : topologicalType} {U : pointedType}.
+Context {T : topologicalType} {U : choiceType}.
 Variables (f : U -> T).
 
 Lemma weak_subspace_open (A : set (weak_topology f)) :
@@ -6554,7 +6775,7 @@ Qed.
 
 Let gauged : Type := T.
 
-HB.instance Definition _ := Pointed.on gauged.
+HB.instance Definition _ := Choice.on gauged.
 HB.instance Definition _ :=
   @isUniform.Build gauged gauge gauge_filter gauge_refl gauge_inv gauge_split.
 
@@ -6566,18 +6787,14 @@ by move=> D [n _ ?]; exists (iter n split_sym (E `&` E^-1)).
 Qed.
 
 Definition type := countable_uniform.type gauge_countable_uniformity.
-
-#[export] HB.instance Definition _ := Uniform.on type.
-#[export] HB.instance Definition _ {R : realType} : PseudoMetric R _ :=
-  PseudoMetric.on type.
-
 End entourage_gauge.
+
 End gauge.
 Module Exports. HB.reexport. End Exports.
 End gauge.
 Export gauge.Exports.
 
-Lemma uniform_pseudometric_sup {R : realType} {T : uniformType} :
+Lemma uniform_pseudometric_sup {R : realType} {T : puniformType} :
     @entourage T = @sup_ent T {E : set (T * T) | @entourage T E}
   (fun E => Uniform.class (@gauge.type T (projT1 E) (projT2 E))).
 Proof.