namespace http://mathhub.info/MitM/core/algebra ❚
import top http://mathhub.info/MitM/interfaces❚
import base http://mathhub.info/MitM/Foundation ❚
import num http://mathhub.info/MitM/core/arithmetics ❚
import sets http://mathhub.info/MitM/core/typedsets ❚

theory OperationProps : base:?Logic = 
  prop_idempotent : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[a] op a a ≐ a ❘ # prop_idempotent 2❙
  prop_associative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[x : U]∀[y : U]∀[z : U] op x (op y z) ≐ op (op x y) z ❘ # prop_associative 2❙
  prop_commutative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[x : U]∀[y] op x y ≐ op y x ❘ # prop_commutative 2❙
  prop_leftUnital : {U : type} (U ⟶ U ⟶ U) ⟶ U ⟶ prop ❘ = [U,op,e] ∀[x] op e x ≐ x ❘ # prop_leftUnital 2 3 ❙
  prop_rightUnital : {U : type} (U ⟶ U ⟶ U) ⟶ U ⟶ prop ❘ = [U,op,e] ∀[x] op x e ≐ x ❘ # prop_rightUnital 2 3 ❙
  prop_leftCancellative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[a] ∀[b] ∀[c] op a c ≐ op b c ⇒ a ≐ b ❘ # prop_leftCancellative 2❙
  prop_rightCancellative : {U : type} (U ⟶ U ⟶ U) ⟶ prop ❘ = [U,op] ∀[a] ∀[b] ∀[c] op c a ≐ op c b ⇒ a ≐ b ❘ # prop_rightCancellative 2❙
  prop_inverse : {U : type} (U ⟶ U ⟶ U) ⟶ (U ⟶ U) ⟶ U ⟶ bool ❘ = [U,op,inv,e] ∀[x] op x (inv x) ≐ e ❘ # prop_inverse 2 3 4 ❙
  prop_absorption : {U : type} (U ⟶ U ⟶ U) ⟶ (U ⟶ U ⟶ U) ⟶ bool ❘ = [U][m,j] ∀[a] ∀[b] m a (j a b) ≐ a ❘ # prop_absorption 2 3 ❙
  prop_distributive : {U : type} (U ⟶ U ⟶ U) ⟶ (U ⟶ U ⟶ U) ⟶ bool ❘
		= [U][plus,times] ∀ [x] ∀ [y] ∀ [z] (times x (plus y z)) ≐ (plus (times x y) (times x z)) ❘ # prop_distributive 2 3 ❙
❚

theory Magma : base:?Logic =
	include ?OperationProps ❙
	include ☞sets:?SetStructures ❙
	theory magma_theory : base:?Logic =
		include ☞sets:?SetStructures/setstruct_theory ❙
		op : U ⟶ U ⟶ U ❘ # 1 ∘ 2 prec 19 ❙
	❚     
	magma = Mod ☞?Magma/magma_theory ❘ role abbreviation ❙
	baseset 	: magma ⟶ type ❘ = [m] (m.universe) ❘ # dom 1 ❙
	operation : {G: magma} (G.universe ⟶ G.universe ⟶ G.universe) ❘ # 2 ∘ 3 prec 20 ❘ = [G] [a,b] (G.op) a b ❙
	finite: magma ⟶ prop ❙
❚
	
theory SemiGroup : base:?Logic =
	include ?Magma ❙

	theory semigroup_theory : base:?Logic =
		include ?Magma/magma_theory ❙
		axiom_associative : ⊦ prop_associative op ❙
	❚
	semigroup = Mod ☞?SemiGroup/semigroup_theory ❙
❚
	
theory Unital : base:?Logic =
	include ?Magma ❙

	theory unital_theory : base:?Logic =
		include ?Magma/magma_theory ❙
		unit : U ❘ # e prec -1 ❙	
		axiom_leftUnital : ⊦ prop_leftUnital op e ❙
		axiom_rightUnital : ⊦ prop_rightUnital op e ❙
	❚
	unital = Mod ☞?Unital/unital_theory  ❙
	
	unitOf 	: {G: unital} dom G ❘ # %I1 e prec 5 ❘ = [G] (G.unit) ❙
❚

theory QuasiGroup : base:?Logic =
	include ☞base:?DescriptionOperator ❙
	include ☞base:?NaturalDeduction ❙
	include ?Magma ❙
	
	theory quasigroup_theory : base:?Logic =
		include ?Magma/magma_theory ❙
		qg1 : ⊦ ∀[a]∀[b]∃![x] a ∘ x ≐ b ❙
		qg2 : ⊦ ∀[a]∀[b]∃![y] y ∘ a ≐ b ❙
	  leftDivision : U ⟶ U ⟶ U ❘ = [a,b] that U ([x] a ∘ x ≐ b) (forallE (forallE qg1 a) b) ❙
	  rightDivision : U ⟶ U ⟶ U ❘ = [a,b] that U ([x] x ∘ a ≐ b) (forallE (forallE qg2 a) b) ❙
❚
	
	quasigroup = Mod ☞?QuasiGroup/quasigroup_theory ❙
❚

theory CancellativeMagma : base:?Logic = 
	include ?Magma ❙
/T MiKo: use this to make a view into quasisgroup Theory: they are cancellative ❙
  theory cancellativemagma_theory : base:?Logic =
		include ?Magma/magma_theory ❙
		axiom_leftCancellative : ⊦ prop_leftCancellative op  ❙
		axiom_rightCancellative : ⊦ prop_rightCancellative op ❙
  ❚

  cancellativemagma = Mod ☞?CancellativeMagma/cancellativemagma_theory ❙
  
  /T MiKo: how to express the definitions? ❙
  leftCancellative : magma ⟶ bool ❙
  rightCancellative : magma ⟶ bool ❙
❚

/T Refactor: a Loop is just a unital Quasigroup ❚
theory Loop : base:?Logic =
	include ?Unital ❙
	include ☞base:?DescriptionOperator ❙
	include ☞base:?NaturalDeduction ❙

	theory loop_theory : base:?Logic =
		include ?Unital/unital_theory ❙
		inverse : U ⟶ U ❘ # 1 ⁻¹  prec 24 ❙
		axiom_inverse : ⊦ prop_inverse op (inverse) e ❙
	❚
	loop = Mod ☞?Loop/loop_theory ❙

	inverseElement : {U : unital} dom U ⟶ dom U ⟶ prop ❘ = [U][n,m] n ∘ m ≐ unitOf U ❙ 
	inverseExists : loop ⟶ prop ❘ = [G] ∀ [x : dom G] ∃ [y : dom G] inverseElement G x y ❙
	
	inverseOf	: {G: loop} dom G ⟶ dom G ❘ # 2 ⁻¹  prec 25 ❘ = [G] [a] (G.inverse) a ❙
❚
	
theory Monoid : base:?Logic =
	include ?SemiGroup ❙
	include ?Unital ❙
	
	theory monoid_theory : base:?Logic =
		include ?SemiGroup/semigroup_theory ❙
		include ?Unital/unital_theory ❙
	❚
	monoid = Mod ☞?Monoid/monoid_theory ❙
	
❚

theory Group : base:?Logic = 
	include ?Monoid ❙
	include ?Loop ❙
	
	theory group_theory : base:?Logic =
		include ?Monoid/monoid_theory ❙ 
		include ?Loop/loop_theory ❙
	❚
	group = Mod ☞?Group/group_theory ❙
		
	                                                                           
	inverseOf	: {G: group} dom G ⟶ dom G ❘ # 2 ⁻¹  prec 25 ❘ = [G] [a] (G.inverse) a ❙
	
	include ☞base:?NatLiterals ❙
	include ☞base:?IntLiterals ❙
	include ☞base:?InformalProofs ❙
	include ☞sets:?FiniteCardinality ❙
	
	automorphisms : group ⟶ ℕ ❙
	cyclic : group ⟶ prop ❙
	order : group ⟶ ℕ ❘ = [g] | fullset (baseset g) |❙
	parity : group ⟶ ℤ ❙
	solvable : group ⟶ prop ❙
	degree : group ⟶ ℤ ❙
	psolvable : group ⟶ ℕ+ ⟶ prop ❙
	sylow : group ⟶ ℕ+ ⟶ group ❙
❚

theory AbelianGroup : base:?Logic =
	include ?Group ❙

	theory abeliangroup_theory : base:?Logic =
		include ?Group/group_theory ❙		
		axiom_commutative : ⊦ prop_commutative op ❙
	❚
	abeliangroup = Mod ☞?AbelianGroup/abeliangroup_theory ❘ role abbreviation ❙
	
❚
	
theory GroupHomomorphism : base:?Logic =
  include ?Group❙
  
  theory groupHomomorphism_theory : base:?Logic =
    from : group ❘# A❙
    to : group ❘# B❙
    morph : dom A ⟶ dom B❙
    axiom_morphism : ⊦ ∀[x: dom A] ∀[y: dom A] (B.op) (morph x) (morph y) ≐ morph (x ∘ y)❙
  ❚
  groupHomomorphism = Mod ☞?GroupHomomorphism/groupHomomorphism_theory❙
  
❚