Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment