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

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.

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

`GATlab.Stdlib.StdTheories.ThLawlessCat`

— Module`ThLawlessCat`

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

`GATlab.Stdlib.StdTheories.ThAscCat`

— Module`ThAsCat`

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

`GATlab.Stdlib.StdTheories.ThIdLawlessCat`

— Module`ThIdLawlessCat`

The theory of a category without identity axioms.