gistfile1.txt

def (a: type) prop := 
	(a1 a2: a) => a1 = a2

def (a: type) set :=
	(a1 a2: a) => (a1 = a2) prop

under (s: type) {

	def binary_relation :=
		(a b: s) => s
	and under (*) {
		def associative := 
			(a b c: s) => (a * b) * c = a * (b * c)

		def commutative :=
			(a b: s) => a * b = b * c

		def transitive :=
			(a b c: s)  => (a * b) => (b * c) => (a * c)

		def reflective :=
			(a: s) => (a * a)
	}
}

def semigroup := (a: #set type, *: #associative a binary_relation)
and under (s) {
	def (e: s) is_identity =>
		(b: s) => alleq(e s.* b, b s.* e, b)
}


def monoid := (a: semigroup, identity: #(is_identity of a) a)
and under (a) {

	under (i: a) {
		def (b: a) is_inverse := alleq(i * b, b * i, identity)

		theorem (#is_inverse b: a, #is_inverse c: a) inverse_is_unique: b = c
			b = b * (i * c) = c
	}
}

def group := (a: monoid, inverse: (i: a) => (#(is_inverse of i) a))