diff --git a/src/topology/category/CompHaus.lean b/src/topology/category/CompHaus.lean
index 3fb69a62ca1a6..9aadbd6a3c113 100644
--- a/src/topology/category/CompHaus.lean
+++ b/src/topology/category/CompHaus.lean
@@ -7,6 +7,7 @@ Authors: Adam Topaz, Bhavik Mehta
 import category_theory.adjunction.reflective
 import topology.category.Top
 import topology.stone_cech
+import category_theory.monad.limits
 
 /-!
 
@@ -26,6 +27,8 @@ introduced.
 
 -/
 
+universe u
+
 open category_theory
 
 /-- The type of Compact Hausdorff topological spaces. -/
@@ -64,7 +67,7 @@ end CompHaus
 
 /-- The fully faithful embedding of `CompHaus` in `Top`. -/
 @[simps {rhs_md := semireducible}, derive [full, faithful]]
-def CompHaus_to_Top : CompHaus ⥤ Top := induced_functor _
+def CompHaus_to_Top : CompHaus.{u} ⥤ Top.{u} := induced_functor _
 
 /--
 (Implementation) The object part of the compactification functor from topological spaces to
@@ -105,8 +108,8 @@ noncomputable def stone_cech_equivalence (X : Top) (Y : CompHaus) :
 The Stone-Cech compactification functor from topological spaces to compact Hausdorff spaces,
 left adjoint to the inclusion functor.
 -/
-noncomputable def Top_to_CompHaus : Top ⥤ CompHaus :=
-adjunction.left_adjoint_of_equiv stone_cech_equivalence (λ _ _ _ _ _, rfl)
+noncomputable def Top_to_CompHaus : Top.{u} ⥤ CompHaus.{u} :=
+adjunction.left_adjoint_of_equiv stone_cech_equivalence.{u u} (λ _ _ _ _ _, rfl)
 
 lemma Top_to_CompHaus_obj (X : Top) : ↥(Top_to_CompHaus.obj X) = stone_cech X :=
 rfl
@@ -116,3 +119,6 @@ The category of compact Hausdorff spaces is reflective in the category of topolo
 -/
 noncomputable instance CompHaus_to_Top.reflective : reflective CompHaus_to_Top :=
 { to_is_right_adjoint := ⟨Top_to_CompHaus, adjunction.adjunction_of_equiv_left _ _⟩ }
+
+noncomputable instance CompHaus_to_Top.creates_limits : creates_limits CompHaus_to_Top :=
+monadic_creates_limits _
diff --git a/src/topology/category/Profinite.lean b/src/topology/category/Profinite.lean
index cd49770c90131..9cc707babb391 100644
--- a/src/topology/category/Profinite.lean
+++ b/src/topology/category/Profinite.lean
@@ -8,6 +8,7 @@ import topology.category.CompHaus
 import topology.connected
 import topology.subset_properties
 import category_theory.adjunction.reflective
+import category_theory.monad.limits
 
 /-!
 # The category of Profinite Types
@@ -28,9 +29,8 @@ compact, Hausdorff and totally disconnected.
 ## TODO
 
 0. Link to category of projective limits of finite discrete sets.
-1. existence of products, limits(?), finite coproducts
-2. `Profinite_to_Top` creates limits?
-3. Clausen/Scholze topology on the category `Profinite`.
+1. finite coproducts
+2. Clausen/Scholze topology on the category `Profinite`.
 
 ## Tags
 
@@ -133,4 +133,19 @@ lemma CompHaus.to_Profinite_obj' (X : CompHaus) :
 instance Profinite.to_CompHaus.reflective : reflective Profinite.to_CompHaus :=
 { to_is_right_adjoint := ⟨CompHaus.to_Profinite, Profinite.to_Profinite_adj_to_CompHaus⟩ }
 
+noncomputable
+instance Profinite.to_CompHaus.creates_limits : creates_limits Profinite.to_CompHaus :=
+monadic_creates_limits _
+
+noncomputable
+instance Profinite.to_Top.reflective : reflective (Profinite_to_Top : Profinite ⥤ Top) :=
+reflective.comp Profinite.to_CompHaus CompHaus_to_Top
+
+noncomputable
+instance Profinite.to_Top.creates_limits : creates_limits Profinite_to_Top :=
+monadic_creates_limits _
+
+instance Profinite.has_limits : limits.has_limits Profinite :=
+has_limits_of_has_limits_creates_limits Profinite_to_Top
+
 end Profinite