Category Theory Definitions

#![allow(unused)]
fn main() {
/// Endofunctor is a function from `Type -> Type` and a mapping operation for morphisms.
set Endofunctor { F : { A : Type } -> Type } -> {
	/// map is a mapping operation for outgoing morphisms on `A : Type`.
	map : { [ B : Type, morphism : A -> B ], a : F(A) } -> F(B)
}
}

#![allow(unused)]
fn main() {
/// Magma is a type with a "unit" element and a binary operation
set Magma [ M : Type ] -> {
	unit: M,
	mult: [a : M, b : M] -> M
}

/// Associativity is a property of a type and a binary operation
set Associativity [ M : Type, bin_op: [M, M] -> M ] -> { {a, b, c} : M^3 } Equivalence(bin_op(bin_op(a, b), c), bin_op(a, bin_op(b, c)))

/// Identity is a property of a type, element `elem` of the type, and a binary operation `bin_op` over the type proving that there is some element of the type such that `bin_op(m, elem) = m` and `bin_op(elem, m) = m`
set Identity [ M : Type, { elem: M, bin_op: [M, M] -> M } ] -> { m : M } {
	Equivalence(bin_op(m, elem), m),
	Equivalence(bin_op(elem, m), m)
}

/// Inverse is a property of a type, element `elem` of the type, and a binary operation over the type proving that for all elements `a` of the type there is a corresponding element `inverse_a` such that `bin_op(a, inverse_a) = elem` and `bin_op(inverse_a, a) = elem`
set Inverse [ M : Type, elem: M, bin_op: [M, M] -> M ] -> { m : M } [
	inverse_a : M,
	{
		Equivalence(bin_op(a, inverse_a), elem),
		Equivalence(bin_op(inverse_a, a), elem)
	}
]

/// A Semigroup is a magma with associativity
set Semigroup [ M : Type ] -> [
	magma: Magma[M],
	Associativity[M, magma.mult]
]

/// A Monoid is a magma with associativity and identity
set Monoid [ M : Type ] -> [
	magma: Magma[M],
	{
		Associativity[M, magma.mult],
		Identity[M, magma],
	}
]

/// A group is a magma with associativity, identity, and inversability
set Group [ M : Type ] -> [
	magma: Magma[M],
	{
		Associativity[M, magma.mult],
		Identity[M, magma],
		Inversability[M, magma]
	}
]
}

#![allow(unused)]
fn main() {
/// Full definition of a monoid
set Monoid [ M : Type ] -> [
	{
		unit : M,
		multiplication : [a : M, b : M] -> M
	},
	{
		associativity : { a : M, b : M, c : M } -> Equivalence(multiplication[multiplication[a, b], c], multiplication[a, multiplication[b, c]])
		identity : { a : M } -> Equivalence(multiplication(a, unit), multiplication(unit, a))
	}
]
}

#![allow(unused)]
fn main() {
/// A Monad is just an Endofunctor and a Monoid
set Monad [ M : Type -> Type ] -> {
	Endofunctor(M)
	Monoid(M)
}
}

Dither Ideas