fix(Topology/Category): make TopCat.Hom constructor private

Mathlib/Condensed/Light/Sequence.lean

@@ -32,7 +32,7 @@ def LightProfinite.fibre : LightProfinite :=
     isCompact_iff_compactSpace.mp (IsClosed.preimage (by fun_prop) isClosed_singleton).isCompact
   of (f ⁻¹' {y})
 
-def LightProfinite.fibreIncl : fibre y f ⟶ X := ⟨⟨{ toFun := Subtype.val }⟩⟩
+def LightProfinite.fibreIncl : fibre y f ⟶ X := ⟨TopCat.ofHom { toFun := Subtype.val }⟩
 
 end
 
@@ -190,9 +190,9 @@ are equal. This can be checked by precomposing with an epimorphism,
 which is given by this morphism. -/
 def cover {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) :
     (of _ (T ⊕ (pullback (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)
-      (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨⟨{
+      (LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ π)))) ⟶ pullback π π := ⟨TopCat.ofHom {
   toFun := coverToFun _ _
-  continuous_toFun := by dsimp [coverToFun]; fun_prop }⟩⟩
+  continuous_toFun := by dsimp [coverToFun]; fun_prop }⟩
 
 open Limits in
 set_option backward.isDefEq.respectTransparency false in
@@ -262,7 +262,9 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] :
   -- `fibres`.
   have := S'_compactSpace π (by fun_prop)
   let S'π (n : ℕ∪{∞}) : LightProfinite.of (S' π) ⟶ LightProfinite.fibre n (π ≫ snd _ _) :=
-    ⟨⟨{ toFun x := x.val n, continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩⟩
+    ⟨TopCat.ofHom {
+      toFun x := x.val n,
+      continuous_toFun := by refine (continuous_apply _).comp ?_; fun_prop }⟩
   let y' : LightProfinite.of (S' π) ⟶ S := ConcreteCategory.ofHom ⟨y π, y_continuous π⟩
   let π' := pullback.snd π (y' ▷ ℕ∪{∞})
   let σ' : ℕ∪{∞} → LightProfinite.of (S' π) → pullback π (y' ▷ ℕ∪{∞}) := fun n ↦
@@ -276,8 +278,8 @@ lemma aux {S T : LightProfinite} (π : T ⟶ S ⊗ ℕ∪{∞}) [Epi π] :
   have : CompactSpace (fibres π' σ') := isCompact_iff_compactSpace.mp
     (fibres_closed π' (by fun_prop) σ' (by fun_prop) hσ').isCompact
   refine ⟨LightProfinite.of (S' π), LightProfinite.of (fibres π' σ'), y',
-    ⟨⟨Subtype.val, by fun_prop⟩⟩ ≫ π',
-    ⟨⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩
+    ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ π',
+    ⟨TopCat.ofHom ⟨Subtype.val, by fun_prop⟩⟩ ≫ pullback.fst _ _, ?_, ?_, ?_, ?_, ?_⟩
   · rw [LightProfinite.epi_iff_surjective]
     refine fibres_surjective _ ?_ _ hσ hσ'
     rw [← LightProfinite.epi_iff_surjective]

Mathlib/Topology/Category/TopCat/Basic.lean

@@ -67,15 +67,19 @@ variable {X} in
 /-- The type of morphisms in `TopCat`. -/
 @[ext]
 structure Hom (X Y : TopCat.{u}) where
-  --private mk ::
+  private mk ::
   /-- The underlying `ContinuousMap`. -/
   hom' : C(X, Y)
 
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
 instance : Category TopCat where
   Hom X Y := Hom X Y
   id X := ⟨ContinuousMap.id X⟩
   comp f g := ⟨g.hom'.comp f.hom'⟩
 
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
 instance : ConcreteCategory.{u} TopCat (fun X Y => C(X, Y)) where
   hom := Hom.hom'
   ofHom f := ⟨f⟩

Mathlib/Topology/Category/TopPair.lean

@@ -52,7 +52,7 @@ abbrev of {A X : TopCat.{u}} (f : A ⟶ X) (h : Topology.IsEmbedding f) : TopPai
 
 /-- Constructor for a topological pair (X, A) where A ⊆ X. -/
 abbrev ofSubset {X : TopCat.{u}} (A : Set X) : TopPair.{u} := TopPair.of (A := (TopCat.of A))
-  (X := X) ⟨{ toFun := Subtype.val }⟩ Topology.IsEmbedding.subtypeVal
+  (X := X) (TopCat.ofHom { toFun := Subtype.val }) Topology.IsEmbedding.subtypeVal
 
 /-- Constructs the topological pair `(X, ∅)` from `X : TopCat`. -/
 abbrev ofTopCat (X : TopCat.{u}) : TopPair.{u} :=

Mathlib/Topology/Sheaves/LocalPredicate.lean

@@ -361,8 +361,8 @@ the presheaf of continuous functions.
 def subpresheafContinuousPrelocalIsoPresheafToTop {X : TopCat.{u}} (T : TopCat.{u}) :
     subpresheafToTypes (continuousPrelocal X T) ≅ presheafToTop X T :=
   NatIso.ofComponents fun X ↦
-    { hom := ↾(by rintro ⟨f, c⟩; exact ofHom ⟨f, c⟩)
-      inv := ↾(by rintro ⟨f, c⟩; exact ⟨f, c⟩) }
+    { hom := ↾fun f ↦ ofHom ⟨f.1, f.2⟩
+      inv := ↾fun f ↦ ⟨f.1, f.1.2⟩ }
 
 /-- The sheaf of continuous functions on `X` with values in a space `T`.
 -/