namespace http://mathhub.info/MitM/core/algebra ❚

import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
import sets http://mathhub.info/MitM/core/typedsets ❚

theory NaturalMonoid : base:?Logic =
	include ?Monoid ❙
	include ☞base:?NaturalDeduction ❙
	include ☞arith:?NaturalArithmetics ❙
	
	naturalMonoid : monoid ❘ = ['
		universe := ℕ,
		op := ☞arith:?NaturalArithmetics?addition ,
		axiom_associative := forallI [x : ℕ] (forallI [y : ℕ] (forallI [z : ℕ] (associative_plus_nat x y z))) ,
		unit := 0 ,
		axiom_leftUnital := forallI leftunital_plus_nat ,
		axiom_rightUnital := forallI rightunital_plus_nat
	'] ❙
❚

theory IntegerRing : base:?Logic =                         
	include ?Ring ❙
	include ☞base:?NaturalDeduction ❙
	include ☞arith:?IntegerArithmetics ❙
	
	axiom_intOneNeqZero : ⊦ neq ℤ 1 0 ❙ 
	
	integerRing : ring ❘ = ['
		universe := ℤ,
		rplus := ☞arith:?IntegerArithmetics?addition ,
		addition/axiom_associative := forallI [x : ℤ] (forallI [y : ℤ] (forallI [z : ℤ] (associative_plus_int x y z))) ,
		rzero := 0 ,
		addition/axiom_leftUnital := forallI ☞arith:?IntegerArithmetics?axiom_leftUnitalPlus ,
		addition/axiom_rightUnital := forallI ☞arith:?IntegerArithmetics?axiom_rightUnitalPlus ,
		rtimes := ☞arith:?IntegerArithmetics?multiplication ,
		multiplication/axiom_associative := forallI [x : ℤ] (forallI [y : ℤ] (forallI [z : ℤ] (associative_times_int x y z))) ,
		rminus := ☞arith:?IntegerArithmetics?uminus ,
		addition/axiom_inverse := forallI (axiom_plusUminus) ,
		addition/axiom_commutative := forallI [x : ℤ] (forallI [y : ℤ] (☞arith:?IntegerArithmetics?axiom_additionCommutative x y)) ,
		axiom_distributive := forallI [x : ℤ] (forallI [y : ℤ] (forallI [z : ℤ] (☞arith:?IntegerArithmetics?axiom_distributive x y z))) ,
		rone := 1 ,
		axiom_oneNeqZero := axiom_intOneNeqZero,
		axiom_leftUnital := forallI ☞arith:?IntegerArithmetics?axiom_leftUnitalTimes ,
		axiom_rightUnital := forallI ☞arith:?IntegerArithmetics?axiom_rightUnitalTimes
	'] ❙
	
	integerGroup = additiveGroup integerRing ❙
❚

theory RationalField : base:?Logic =
	include ?Field ❙
	include ☞arith:?RationalArithmetics ❙
	include ☞base:?NaturalDeduction ❙
	
	axiom_ratOneNeqZero : ⊦ neq ℚ 1 0 ❙ 

	rationalField : field ❘ = ['
		universe := ℚ,
		rplus := ☞arith:?RationalArithmetics?addition ,
		addition/axiom_associative := forallI [x : ℚ] (forallI [y : ℚ] (forallI [z : ℚ] (associative_plus_rat x y z))) ,
		rzero := 0 ,
		addition/axiom_leftUnital := forallI ☞arith:?RationalArithmetics?axiom_leftUnitalPlus ,
		addition/axiom_rightUnital := forallI ☞arith:?RationalArithmetics?axiom_rightUnitalPlus ,
		rtimes := ☞arith:?RationalArithmetics?multiplication ,
		multiplication/axiom_associative := forallI [x : ℚ] (forallI [y : ℚ] (forallI [z : ℚ] (associative_times_rat x y z))) ,
		rminus := ☞arith:?RationalArithmetics?uminus ,
		addition/axiom_inverse := forallI ☞arith:?RationalArithmetics?axiom_plusUminus ,
		addition/axiom_commutative := forallI [x : ℚ] (forallI [y : ℚ] (☞arith:?RationalArithmetics?axiom_commutativePlus x y)) ,
		☞arith:?IntegerArithmetics?axiom_distributive := forallI [x : ℚ] (forallI [y : ℚ] (forallI [z : ℚ] (☞arith:?RationalArithmetics?axiom_distributive x y z))) ,
		rone := 1 ,
		axiom_oneNeqZero := axiom_ratOneNeqZero,
		axiom_leftUnital := forallI ☞arith:?RationalArithmetics?axiom_leftUnitalTimes ,
		axiom_rightUnital := forallI ☞arith:?RationalArithmetics?axiom_rightUnitalTimes ,
		inverse := inverseTyped ,
		axiom_inverse := forallI axiom_inv2 ,
		axiom_commutative := forallI [x : ℚ] (forallI [y : ℚ] ☞arith:?RationalArithmetics?axiom_commutativeTimes x y)
	'] ❙ // TODO ugly hack!! ❙
	
	rationalField2 : field ❘ # IntegerRing❙
	
❚

theory RealField : base:?Logic =
	include ?Field ❙
	include ☞arith:?RealArithmetics ❙
	include ☞base:?NaturalDeduction ❙
	
	axiom_realOneNeqZero : ⊦ neq ℝ 1 0 ❙ 

	realField : field ❘ = ['
		universe := ℝ,
		rplus := ☞arith:?RealArithmetics?addition ,
		addition/axiom_associative := forallI [x : ℝ] (forallI [y : ℝ] (forallI [z : ℝ] (associative_plus_real x y z))) ,
		rzero := 0 ,
		addition/axiom_leftUnital := forallI ☞arith:?RealArithmetics?axiom_leftUnitalPlus ,
		addition/axiom_rightUnital := forallI ☞arith:?RealArithmetics?axiom_rightUnitalPlus ,
		rtimes := ☞arith:?RealArithmetics?multiplication ,
		multiplication/axiom_associative := forallI [x : ℝ] (forallI [y : ℝ] (forallI [z : ℝ] (associative_times_real x y z))) ,
		rminus := ☞arith:?RealArithmetics?uminus ,
		addition/axiom_inverse := forallI ☞arith:?RealArithmetics?axiom_plusUminus ,
		addition/axiom_commutative := forallI [x : ℝ] (forallI [y : ℝ] (☞arith:?RealArithmetics?axiom_commutativePlus x y)) ,
		☞arith:?IntegerArithmetics?axiom_distributive := forallI [x : ℝ] (forallI [y : ℝ] (forallI [z : ℝ] (☞arith:?RealArithmetics?axiom_distributive x y z))) ,
		rone := 1 ,
		axiom_oneNeqZero := axiom_realOneNeqZero,
		axiom_leftUnital := forallI ☞arith:?RealArithmetics?axiom_leftUnitalTimes ,
		axiom_rightUnital := forallI ☞arith:?RealArithmetics?axiom_rightUnitalTimes ,
		☞arith:?IntegerArithmetics?inverse := ☞arith:?RealArithmetics?inverseTyped ,
		axiom_inverse := forallI ☞arith:?RealArithmetics?axiom_inv2 ,
		axiom_commutative := forallI [x : ℝ] (forallI [y : ℝ] ☞arith:?RealArithmetics?axiom_commutativeTimes x y)
	'] ❙ // TODO ugly hack!! ❙
	
❚

theory RealVectorspace : base:?Logic =
	include ?Vectorspace ❙
	include ?RealField ❙
	include ?Productspace ❙
	
	realVec : kind ❘ = vectorspace realField ❙
	realVec1 : realVec ❘ = asVectorspace realField ❘ # ℝ1 ❙
	realVec2 : realVec ❘ // = productspace realField ℝ1 ℝ1 ❘ # ℝ2 ❙
	realVec3 : realVec ❘ // = productspace realField ℝ1 ℝ2 ❘ # ℝ3 ❙ // takes forever ❙
	// finite_real_vectorspace : pos_lit ⟶ RealVec ❙
❚