diff --git a/source/draft-structure.mmt b/source/draft-structure.mmt
index 379fcb2630374ce0e6006f694fe15721f4dfb689..66cbab0de82de973c30f8d65ce9fc909d9d70668 100644
--- a/source/draft-structure.mmt
+++ b/source/draft-structure.mmt
@@ -1,7 +1,7 @@
-namespace http://mathhub.info/MitM/smglom/draft-0
+namespace http://mathhub.info/MitM/smglom/draft-0 âš
-import base http://mathhub.info/MitM/Foundation
+import base http://mathhub.info/MitM/Foundation âš
// This is an outline of how to design the MitM for group theory
//
@@ -21,29 +21,29 @@ import base http://mathhub.info/MitM/Foundation
// Subgroup
// subset of group that is closed
-// AllSubgroups : {G : Group} → Set (of subgroups of G)
+// AllSubgroups : {G : Group} ⟶ Set (of subgroups of G)
// Subgroups via embeddings:
-// subgroup : {G : Group} → (injection H → G)
+// subgroup : {G : Group} ⟶ (injection H ⟶ G)
-// Cosets {G : Group} → U : Subgroup G → Set
+// Cosets {G : Group} ⟶ U : Subgroup G ⟶ Set
// Group Action (what about pairs?)
// really these are permutation actions...
// need both left- and right-actions
-// left-action : {X : Set} → {G : Group} → X × G → X
-// right-action : {X : Set} → {G : Group} → G × X → X
+// left-action : {X : Set} ⟶ {G : Group} ⟶ X × G ⟶ X
+// right-action : {X : Set} ⟶ {G : Group} ⟶ G × X ⟶ X
//
-// also: action : {X : Set} → {G : Group} → G → SymmetricGroup(X)
+// also: action : {X : Set} ⟶ {G : Group} ⟶ G ⟶ SymmetricGroup(X)
// Formalise the "isomorphism" between the two?
// What about Automorphism groups of stuff? If we have a graph Γ and a group G
// then we act on Γ by graph automorphisms
// for any group action `act` we define
-// stabiliser : {act : GroupAction} → groundset act → Subgroup of G
-// orbit : {act : GroupAction} → groundset act → Subset (groundset act)
+// stabiliser : {act : GroupAction} ⟶ groundset act ⟶ Subgroup of G
+// orbit : {act : GroupAction} ⟶ groundset act ⟶ Subset (groundset act)
//
// Centraliser
diff --git a/source/types.mmt b/source/types.mmt
index fb27a3d15179d08de5dfe0dfab1c361eb808c4c2..0ffc79a1e4f800355368b2407a1fce9e1b9629c4 100644
--- a/source/types.mmt
+++ b/source/types.mmt
@@ -1,86 +1,86 @@
-namespace http://www.gap-system.org/
-import rules scala://GAP.odk.mmt.kwarc.info
+namespace http://www.gap-system.org/ âš
+import rules scala://GAP.odk.mmt.kwarc.infoâš
theory Types : ur:?PLF =
- object : type
- category : type
+ object : type â™
+ category : type â™
- filter = object → type
+ filter = object ⟶ type â™
- constant # : object → filter → type // = [o][f] f o # 1 # 2
+ constant # : object ⟶ filter ⟶ type ☠// = [o][f] f o ☠# 1 # 2 â™
- filter_and : filter → filter → filter # 1 and 2
- filter_and_hasFilter1 : {x,f : filter,g : filter} x # f → x # g → x # (f and g)
- filter_and_hasFilter2 : {x,f : filter,g : filter} x # (f and g) → x # f
- filter_and_hasFilter3 : {x,f : filter,g : filter} x # (f and g) → x # g
+ filter_and : filter ⟶ filter ⟶ filter ☠# 1 and 2 â™
+ filter_and_hasFilter1 : {x,f : filter,g : filter} x # f ⟶ x # g ⟶ x # (f and g) â™
+ filter_and_hasFilter2 : {x,f : filter,g : filter} x # (f and g) ⟶ x # f â™
+ filter_and_hasFilter3 : {x,f : filter,g : filter} x # (f and g) ⟶ x # g â™
- ded : object → type
+ ded : object ⟶ type â™
- rule rules?Booleans
- rule rules?Integers
- rule rules?Floats
+ rule rules?Booleans â™
+ rule rules?Integers â™
+ rule rules?Floats â™
- booleans : type
- integers : type
- floats : type
- gapbool : booleans → object
- gapint : integers → object
- gapfloat : floats → object
+ booleans : type â™
+ integers : type â™
+ floats : type â™
+ gapbool : booleans ⟶ object â™
+ gapint : integers ⟶ object â™
+ gapfloat : floats ⟶ object â™
- trueI : ded (gapbool true)
- catFilter : category → filter
- propertyFilter : (object → object) → filter = [p] [o] ded (p o)
+ trueI : ded (gapbool true) â™
+ catFilter : category ⟶ filter â™
+ propertyFilter : (object ⟶ object) ⟶ filter ☠= [p] [o] ded (p o) â™
- Has : (object → object) → filter
- CategoryCollection : filter → category
- Set : filter → (object → object)
- IsBool : category
- IsObject : category
- // HasIsProperty : {o,x} x # (propertyFilter o) → ((Has o) x) # catFilter IsBool
+ Has : (object ⟶ object) ⟶ filter â™
+ CategoryCollection : filter ⟶ category â™
+ Set : filter ⟶ (object ⟶ object) â™
+ IsBool : category â™
+ IsObject : category â™
+ // HasIsProperty : {o,x} x # (propertyFilter o) ⟶ ((Has o) x) # catFilter IsBool â™
-
+âš
// theory Types : odk:?Math =
- Object : tp
+ Object : tp â™
- Family : tp
- Family_Of_Families : tm Family
- Families_are_Objects : Family < Object
- Family_Of_Object : tm Object → tm Family # FamilyOfObj 1
- Family_Of_Family_is_Family_of_Families : {F:tm Family} ⊦ eq Family (FamilyOfObj (tpCast Families_are_Objects F)) Family_Of_Families
+ Family : tp â™
+ Family_Of_Families : tm Family â™
+ Families_are_Objects : Family < Object â™
+ Family_Of_Object : tm Object ⟶ tm Family ☠# FamilyOfObj 1 â™
+ Family_Of_Family_is_Family_of_Families : {F:tm Family} ⊦ eq Family (FamilyOfObj (tpCast Families_are_Objects F)) Family_Of_Families â™
- Filter : tp
- Elementary_Filter : tp
- Elementary_Filter_Is_Filter : Elementary_Filter < Filter
+ Filter : tp â™
+ Elementary_Filter : tp â™
+ Elementary_Filter_Is_Filter : Elementary_Filter < Filter â™
- Filter_applies : tm Filter → tm Object → prop # 1 _ 2
+ Filter_applies : tm Filter ⟶ tm Object ⟶ prop ☠# 1 _ 2 â™
- filter_conj : tm Filter → tm Filter → tm Filter # 1 + 2 prec 5
- filter_conj_is_Conjunction : {F1,F2,O} ⊦ ((F1 + F2) _ O) ≠((F1 _ O) ∧ (F2 _ O)) role Simplify
- filter_conj_is_associative : {F1,F2,F3} ⊦ F1 + (F2 + F3) ≠(F1 + F2) + F3
- filter_conj_is_commutative : {F1,F2} ⊦ F1 + F2 ≠F2 + F1
+ filter_conj : tm Filter ⟶ tm Filter ⟶ tm Filter ☠# 1 + 2 prec 5â™
+ filter_conj_is_Conjunction : {F1,F2,O} ⊦ ((F1 + F2) _ O) ≠((F1 _ O) ∧ (F2 _ O)) ☠role Simplify â™
+ filter_conj_is_associative : {F1,F2,F3} ⊦ F1 + (F2 + F3) ≠(F1 + F2) + F3 â™
+ filter_conj_is_commutative : {F1,F2} ⊦ F1 + F2 ≠F2 + F1 â™
- filter_def : (tm Object → prop) → tm Filter # MakeFilter 1
- filter_def_application : {F,O} ⊦ ((MakeFilter F) _ O) ≠F O
+ filter_def : (tm Object ⟶ prop) ⟶ tm Filter ☠# MakeFilter 1 â™
+ filter_def_application : {F,O} ⊦ ((MakeFilter F) _ O) ≠F O â™
- GAPtype : tp
- Family_of_GAPtype : tm GAPtype → tm Family # FamilyOfTp 1
- Filter_of_GAPtype : tm GAPtype → tm list Elementary_Filter # FilterOf 1
- GAPtype_Constructor : tm Family → tm list Elementary_Filter → tm GAPtype # GAPtp 1 2
- // Filter_applies_to_type_object : {O} ⊦ (FilterOf O) _ O
+ GAPtype : tp â™
+ Family_of_GAPtype : tm GAPtype ⟶ tm Family ☠# FamilyOfTp 1 â™
+ Filter_of_GAPtype : tm GAPtype ⟶ tm list Elementary_Filter ☠# FilterOf 1 â™
+ GAPtype_Constructor : tm Family ⟶ tm list Elementary_Filter ⟶ tm GAPtype ☠# GAPtp 1 2 â™
+ // Filter_applies_to_type_object : {O} ⊦ (FilterOf O) _ O â™
- Operation : tp
- Name_of_Operation : tm Operation → tm string
- Arglength_of_Operation : tm Operation → tm ℕ
- Filter_of_Operation : {op: tm Operation} tm vector Filter (Arglength_of_Operation op)
- Operation_Constructor : {name: tm string, args: tm ℕ} tm vector Filter args → tm Operation
+ Operation : tp â™
+ Name_of_Operation : tm Operation ⟶ tm string â™
+ Arglength_of_Operation : tm Operation ⟶ tm â„• â™
+ Filter_of_Operation : {op: tm Operation} tm vector Filter (Arglength_of_Operation op) â™
+ Operation_Constructor : {name: tm string, args: tm â„•} tm vector Filter args ⟶ tm Operation â™
- Category : tp
- Category_is_elementary_Filter : Category < Elementary_Filter
+ Category : tp â™
+ Category_is_elementary_Filter : Category < Elementary_Filter â™
- Property : tp
- Property_is_elementary_Filter : Property < Elementary_Filter
- Has : tm Property → tm Elementary_Filter
- OperationFromProperty : tm Property → tm Operation
- OperationSet : tm Property → tm Operation # Set 1
-
\ No newline at end of file
+ Property : tp â™
+ Property_is_elementary_Filter : Property < Elementary_Filter â™
+ Has : tm Property ⟶ tm Elementary_Filter â™
+ OperationFromProperty : tm Property ⟶ tm Operation â™
+ OperationSet : tm Property ⟶ tm Operation ☠# Set 1 â™
+âš
\ No newline at end of file