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

GATlab.Stdlib.StdTheories.##1713 — 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

GATlab.Stdlib.StdTheories.##1714 — Constant

This theory contains an associative binary operation called multiplication.

Examples:

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

The theory of a semigroup with identity.

Examples:

  • The integers under multiplication
  • Lists (nonempty and empty) under concatenation
GATlab.Stdlib.StdTheories.##1716 — 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
GATlab.Stdlib.StdTheories.##1717 — Constant

The theory of a monoid where multiplication enjoys commutativity.

Examples:

  • The set of classical 1-knots under "knot sum"
GATlab.Stdlib.StdTheories.##1718 — 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"