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