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.##1003 — 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.##1005 — 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.##1025 — 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
GATlab.Stdlib.StdTheories.##972 — 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.##975 — 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.##977 — 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.##982 — Constant

This theory contains an associative binary operation called multiplication.

Examples:

  • The integers under multiplication
  • Nonempty lists under concatenation
source
GATlab.Stdlib.StdTheories.##992 — 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