Add outline

Add an outline of the needed structures for GAP and the example
we intent to implement.

source/alignment.mmt

+namespace http://www.gap-system.org j
\ No newline at end of file

source/draft-structure.mmt

+namespace http://mathhub.info/MitM/smglom/draft-0 
+
+
+import base http://mathhub.info/MitM/Foundation 
+
+// This is an outline of how to design the MitM for group theory 
+//
+// it is divided into 
+//  - abstract theory
+//
+//    - permutation groups
+//    - matrix groups
+//    - finitely presented groups
+
+// Group (abstract)
+
+// Group Homomorphism
+// (needs injective, surjective, bijective at some point
+//  should be inherited from underlying map?)
+
+// Subgroup
+// subset of group that is closed
+
+// AllSubgroups : {G : Group} → Set (of subgroups of G)
+
+// Subgroups via embeddings:
+// subgroup : {G : Group} → (injection H → G)
+
+// 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
+//
+// 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)
+// 
+
+// Centraliser
+// Normaliser
+
+// Computational-ish aspects
+
+// GroupByGenerators
\ No newline at end of file