no message

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❚

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❘

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}