diff --git a/source/fundamentals/universes.mmt b/source/fundamentals/universes.mmt
index cb75c180cc37193107b122ac43ef7b5d9a6747c4..cc997b4c49717154503389074724c32f26f6f5ea 100644
--- a/source/fundamentals/universes.mmt
+++ b/source/fundamentals/universes.mmt
@@ -54,3 +54,5 @@ theory UniverseDepFunExample =
   function_types: Pi_legal utp utp❙
   dependent_types: Pi_legal utp ukd❙
 ❚
+
+// TODO these universes should be realized by corresponding theories of set-theoretical universe❚
diff --git a/source/set_theory/axioms.mmt b/source/set_theory/axioms.mmt
index f2c35d2bbeb9941f60c35a99037bf65cc010da19..4c631b972372549792ef66070796bc9b01da08c7 100644
--- a/source/set_theory/axioms.mmt
+++ b/source/set_theory/axioms.mmt
@@ -77,7 +77,7 @@ theory ReplacementAx =
   include ?RelationDefinitions❙
   
   // The resulting set is a replacement for A regarding function f❙
-  isreplacement = [f,A,Z] ∀ͧ[y] y∈Z ⇔ (∃ͧ[x] x∈A ∧ f x y)❙  
+  isreplacement = [f,A,Z] ∀ͧ[y] y∈Z ⇔ (∃ͧ[x] x∈A ∧ f x y)❙
 
   replacement_axiom : {f} ⊦ ∀ͧ[A] isfunction f A ⇒ ∃ͧ[Z] isreplacement f A Z❙
   replacement_unique : {f,A} ⊦ isfunction f A ⟶ ⊦ ∃ꜝͧ[Z] isreplacement f A Z❘
diff --git a/source/type_theory/endofunctors/collection_types.mmt b/source/type_theory/endofunctors/collection_types.mmt
index 8ffd308fc3ecb21f67d7445c90435062b827cc15..1b3574987063d4708685607baff2b2214fe32650 100644
--- a/source/type_theory/endofunctors/collection_types.mmt
+++ b/source/type_theory/endofunctors/collection_types.mmt
@@ -116,7 +116,7 @@ theory MultisetSpec =
   include ?ListSpec❙
   include ?EndoCommutative❙
 
-  	intersect: {a} tm &a ⟶ tm &a ⟶ tm &a❘# %n 2 3 prec 30❙ 
+  intersect: {a} tm &a ⟶ tm &a ⟶ tm &a❘# %n 2 3 prec 30❙ 
 	intersect_neutral1 : {a, xs: tm &a} ⊦ intersect neutral xs =ͭ neutral❙
 	intersect_neutral2 : {a, xs: tm &a} ⊦ intersect xs neutral =ͭ neutral❙
 	intersect_cons1: {a,x: tm a, xs,ys: tm &a}