# 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 ⊣ [] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =# 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)] ```

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 ⊣ [] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =# 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)] ```

### 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.ThClass`

— Module``` ThClass ``` A Class is just a Set that doesn't worry about foundations.

## ThClass ``` Ob::TYPE ⊣ [] ```

`GATlab.Stdlib.StdTheories.ThLawlessCat`

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

## ThLawlessCat ``` Ob::TYPE ⊣ [] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =# compose(f, g)::Hom(a, c) ⊣ [a::Ob, b::Ob, c::Ob, f::Hom(a, b), g::Hom(b, c)] ```

`GATlab.Stdlib.StdTheories.ThAscCat`

— Module``` ThAsCat ``` The theory of a category with the associative law for composition.

## ThAscCat ``` Ob::TYPE ⊣ [] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =# 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)] ```

`GATlab.Stdlib.StdTheories.ThIdLawlessCat`

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

## ThIdLawlessCat ``` Ob::TYPE ⊣ [] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:24 =# Hom(dom, codom)::TYPE ⊣ [dom::Ob, codom::Ob] #= /juliateam/.julia/packages/GATlab/UL4sq/src/stdlib/theories/categories.jl:33 =# 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] ```

`GATlab.Stdlib.StdTheories.##1704`

— Constant`ThClass`

A Class is just a Set that doesn't worry about foundations.

`GATlab.Stdlib.StdTheories.##1705`

— Constant`ThGraph`

A graph where the edges are typed depending on dom/codom. Contains all necessary types for the theory of categories.

`GATlab.Stdlib.StdTheories.##1706`

— Constant`ThLawlessCat`

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

`GATlab.Stdlib.StdTheories.##1707`

— Constant`ThAsCat`

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

`GATlab.Stdlib.StdTheories.##1708`

— Constant`ThIdLawlessCat`

The theory of a category without identity axioms.

`GATlab.Stdlib.StdTheories.##1709`

— Constant`ThCategory`

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

`GATlab.Stdlib.StdTheories.##1710`

— 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.

`GATlab.Stdlib.StdTheories.##1712`

— ConstantThe theory of a set with no operations

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

`GATlab.Stdlib.StdTheories.##1713`

— ConstantThe 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

`GATlab.Stdlib.StdTheories.##1714`

— ConstantThis theory contains an associative binary operation called multiplication.

Examples:

- The integers under multiplication
- Nonempty lists under concatenation

`GATlab.Stdlib.StdTheories.##1715`

— ConstantThe theory of a semigroup with identity.

Examples:

- The integers under multiplication
- Lists (nonempty and empty) under concatenation

`GATlab.Stdlib.StdTheories.##1716`

— ConstantThe 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

`GATlab.Stdlib.StdTheories.##1717`

— ConstantThe theory of a monoid where multiplication enjoys commutativity.

Examples:

- The set of classical 1-knots under "knot sum"

`GATlab.Stdlib.StdTheories.##1718`

— ConstantThe 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"

`GATlab.Stdlib.StdTheories.##1719`

— ConstantThe theory of monoidal categories

`mcompose`

is usually denoted with ⊗ and the munit is usually denoted by 1 or I.

`GATlab.Stdlib.StdTheories.##1720`

— ConstantThe theory of monoidal categories with strict associativity

`GATlab.Stdlib.StdTheories.##1721`

— ConstantThe theory of natural numbers

`GATlab.Stdlib.StdTheories.##1722`

— ConstantThe theory of natural numbers with addition as repeated succession

`GATlab.Stdlib.StdTheories.##1723`

— ConstantThe theory of nat-plus with multiplication