From ba65ab19b42008b8781339bbeafd1c750fb15e1d Mon Sep 17 00:00:00 2001
From: Florian Rabe <florian.rabe@gmail.com>
Date: Fri, 28 Mar 2025 14:53:33 +0100
Subject: [PATCH] no message

---
 source/fundamentals/universes.mmt                    | 2 ++
 source/set_theory/axioms.mmt                         | 2 +-
 source/type_theory/endofunctors/collection_types.mmt | 2 +-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/source/fundamentals/universes.mmt b/source/fundamentals/universes.mmt
index cb75c180..cc997b4c 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 f2c35d2b..4c631b97 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 8ffd308f..1b357498 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} 
-- 
GitLab