GitHub

Standard Library

Categories

Our friend ThCategory is the main theory in this module.

GATlab.Stdlib.StdTheories.ThCategory — Module

``` ThCategory ``` The theory of a category with composition operations and associativity and identity axioms.

## ThCategory ``` Ob::TYPE ⊣ [] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:26 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:37 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] (assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)] id(a)::Hom(a, a) ⊣ [a::Ob] (idl := compose(id(a), f) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)] (idr := compose(f, id(b)) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)] ```

source

You can specialize a theory by adding more axioms. In this case we can specialize the theory of categories to that of thin category by adding the axiom that two morphisms are equal if they have the same domain and codomain.

thineq := f == g :: Hom(A,B) ⊣ [A::Ob, B::Ob, f::Hom(A,B), g::Hom(A,B)]
GATlab.Stdlib.StdTheories.ThThinCategory — Module

``` ThThinCategory ``` The theory of a thin category meaning that if two morphisms have the same domain and codomain they are equal as morphisms. These are equivalent to preorders.

## ThThinCategory ``` Ob::TYPE ⊣ [] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:26 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:37 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] (assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)] id(a)::Hom(a, a) ⊣ [a::Ob] (idl := compose(id(a), f) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)] (idr := compose(f, id(b)) == f) ⊣ [a::Ob, b::Ob, f::Hom(a, b)] (thineq := f == g) ⊣ [a::Ob, b::Ob, f::Hom(a, b), g::Hom(a, b)] ```

source

Category Building Blocks

The remaining theories in this module are not necessarily useful, but go to show demonstrate the theory hierarchy can be built up in small increments.

GATlab.Stdlib.StdTheories.ThLawlessCat — Module

``` ThLawlessCat ``` The data of a category without any axioms of associativity or identities.

## ThLawlessCat ``` Ob::TYPE ⊣ [] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:26 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:37 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] ```

source
GATlab.Stdlib.StdTheories.ThAscCat — Module

``` ThAscCat ``` The theory of a category with the associative law for composition.

## ThAscCat ``` Ob::TYPE ⊣ [] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:26 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:37 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] (assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)] ```

source
GATlab.Stdlib.StdTheories.ThIdLawlessCat — Module

``` ThIdLawlessCat ``` The theory of a category without identity axioms.

## ThIdLawlessCat ``` Ob::TYPE ⊣ [] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:26 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /home/runner/work/GATlab.jl/GATlab.jl/src/stdlib/theories/categories.jl:37 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] (assoc := compose(compose(f, g), h) == compose(f, compose(g, h))) ⊣ [a::Ob, b::Ob, c::Ob, d::Ob, f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)] id(a)::Hom(a, a) ⊣ [a::Ob] ```

source
GATlab.Stdlib.StdTheories.##916 — Constant
ThThinCategory

The theory of a thin category meaning that if two morphisms have the same domain and codomain they are equal as morphisms. These are equivalent to preorders.

source
GATlab.Stdlib.StdTheories.##919 — Constant

The theory of a set with no operations

A base theory for all algebraic theories so that multiple inheritance doesn't create multiple types.

source
GATlab.Stdlib.StdTheories.##921 — Constant

The theory of a set with a binary operation which does not guarantee associativity

Examples:

  • The integers with minus operation is not associative.

    (a ⋅ b) ⋅ c = a - b - c

    a ⋅ (b ⋅ c) = a - b + c

source
GATlab.Stdlib.StdTheories.##926 — Constant

This theory contains an associative binary operation called multiplication.

Examples:

  • The integers under multiplication
  • Nonempty lists under concatenation
source
GATlab.Stdlib.StdTheories.##936 — Constant

The theory of a monoid with multiplicative inverse.

Examples:

  • The rationals (excluding zero) under multiplication
  • E(n), the group of rigid transformations (translation and rotation)
  • Bₙ, the braid group of n strands
source
GATlab.Stdlib.StdTheories.##947 — Constant

The theory of a semiring

A set where addition is a commutative monoid, multiplication is monoidal, and they interact through distributivity.

Examples:

source
GATlab.Stdlib.StdTheories.##949 — Constant

The theory of a ring

A set where addition is a group, multiplication is monoidal, and they interact through distributivity.

Examples:

A ring can also be obtaned by imposing additive inverses on a semiring.

source
GATlab.Stdlib.StdTheories.##969 — Constant

The theory of sets which have a preorder.

This is equivalent to the theory of thin categories (ThThinCategory) where ≤ is the composition operation.

Examples:

  • The set of natural numbers ordered by b-a ≥ 0
  • The set of natural numbers ordered by "a divides b"
source