update

narration/primitives.omdoc

+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://www.gap-system.org/primitives.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://www.gap-system.org/primitives.mmt#0.0.0:3045.89.0"/></metadata><mref name="[http://www.gap-system.org/mitm?prim]" target="http://www.gap-system.org/mitm?prim"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://www.gap-system.org/primitives.mmt#44.2.0:54.2.10"/></metadata></mref></omdoc>
\ No newline at end of file

relational/http..www.gap-system.org/mitm/prim.rel

+untypedconstant http://www.gap-system.org/mitm?prim?ListConstr
+theory http://www.gap-system.org/mitm?prim
+HasMeta http://www.gap-system.org/mitm?prim http://www.gap-system.org?Types
+Declares http://www.gap-system.org/mitm?prim http://www.gap-system.org/mitm?prim?ListConstr
+constant http://www.gap-system.org/mitm?prim?ListConstr

relational/primitives.rel

+document http://www.gap-system.org/primitives.omdoc
+Declares http://www.gap-system.org/primitives.omdoc http://www.gap-system.org/mitm?prim

source/alignment.mmt

-namespace http://www.gap-system.org ❚
+namespace http://www.gap-system.org ❚
\ No newline at end of file
+
+theory Alignments : mitm?lib =
+	DihedralGroup = [d] `lib?DihedralGroup  `lib?IsPermGroup d ❙
+❚
\ No newline at end of file

source/primitives.mmt

+namespace http://www.gap-system.org/mitm ❚
+
+theory prim : ../?Types =
+	ListConstr ❙
+❚
+
+// theory Types : ur:?PLF =
+	object : type ❙
+	category : type ❙
+	
+	booleans : type ❙
+	integers : type ❙
+	floats : type ❙
+	
+	filter = object ⟶ type ❙
+	
+	hastp : object ⟶ filter ⟶ type ❘ //  = [o][f] f o ❘ # 1 $ 2 ❙
+	
+	filter_and : filter ⟶ filter ⟶ filter ❘ # 1 and 2 ❙
+	filter_and_hasFilter1 : {x : object,f : filter,g : filter} x $ f ⟶ x $ g ⟶ x $ (f and g) ❙
+	filter_and_hasFilter2 : {x : object,f : filter,g : filter} x $ (f and g) ⟶ x $ f ❙
+	filter_and_hasFilter3 : {x : object,f : filter,g : filter} x $ (f and g) ⟶ x $ g ❙
+	
+	ded : object ⟶ type ❙
+	
+	rule rules?Booleans ❙
+	rule rules?Integers ❙
+	rule rules?Floats ❙
+	
+	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) ❙
+	
+	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 ❙
+
+	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_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_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 ❙
+	
+	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 ❙
+	
+	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