category theory is a branch of mathematics that formalizes the notion of a special function via arrows or morphisms. a category is an algebraic object that (abstractly) consists of a class of "objects", and for every pair of objects, a set of "morphisms". a partial (equiv. dependently typed) binary operation called composition is provided on morphisms, every object has one special morphism from it to itself called the identity on that object, and composition and identities are required to obey certain relations.