Category theory

From Esolang
Jump to navigation Jump to search

Category theory is the area of mathematics concerned with "Categories". Categories can be thought of as the algebraic structure of the universe of sets along with the class of all functions/mappings on sets, in a similar way to groups as the algebraic structure of the rotation and reflection symmetries of a regular polygon.

Introduction

A category can also be thought of as—but is not equivalent to—a labeled digraph: a set of nodes containing values with directed edges mapping nodes to other nodes. In the more general way of thought, a category is a class of "objects"—which can be any type of arbitrary thing—with "arrows" (also called "morphisms") between them mapping one to another. An arrow represents some sort of transformation between a "domain" (the object from which the arrow originates) and the "codomain" (the destination object).

Categories also have some sort of operation for composing arrows, written f ∘ g. This leads to the property that, if there is are two arrows f : A → B and g : B → C, then there is another arrow f ∘ g : A → C. This should be reminiscent of function composition in other areas of mathematics, but represents a more general concept. Note that it is required that is associative—that is, (f ∘ g) ∘ h ≡ f ∘ (g ∘ h).

The final requirement for a category is that every object A has an "identity morphism" idA. For every morphism f : A → B, The identity object has the property that f ∘ idA ≡ f, and for every morphism g : B → A, idA ∘ g ≡ g

Higher Categories

In certain contexts, such as topology, it is natural to define 2-morphisms, things similar to morphisms whose domains and codomains are themselves morphisms. These can be composed in more varied ways, and lead to a generalization of associativity known as a coherence law. There is a hierarchy of k-morphisms parameterized by natural numbers, which may or may not be directed. The study of categories with such higher k-morphisms is known as Higher Category Theory, and is discussed in detail on The nLab.

Automatic Language Generation

Given a category, we can follow a recipe to generate the semantics for a language which studies that category. If facts about the original category are computable, then the resulting language is computable too.

Native Type Theory

Conversely, given a language, we can generate a type theory and associated category. The resulting type theory is called the native type theory. Even dynamically-typed languages often have useful native type theories.