# Standard Library

## Categories

Our friend ThCategory is the main theory in this module.

GATlab.Stdlib.StdTheories.ThCategoryModule

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

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

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

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

 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.##1710Constant
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.##1713Constant

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

GATlab.Stdlib.StdTheories.##1716Constant

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
GATlab.Stdlib.StdTheories.##1718Constant

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"