The Type Namespace Structure Component

Overview

The structure component of the type namespace of the IFF metashell (IFF-TYPE) is a medium-sized namespace located directly below the IFF-IFF namespace and directly above the structure component of the IFF-META namespace. It enables category-theoretic declarations of meta things. The structural component of the type namespace of the IFF metashell provides a baseline formalism for category theory. In one sense, it represents “the category of categories as a foundation for mathematics” (Lawvere) (See also the Antimeta blog).

As illustrated in Diagram 1, the sets and functions at the IFF metalevel characterize the overall architecture for the structural component. Nodes in this diagram represent IFF sets and edges (arrows) represent IFF functions. The small oval on the right represents the namespace of type sets and their functions. The next larger oval represents the namespace of type graphs and their morphisms. These two namespaces are contained in the core component. Also indicated are namespaces for categories, functors, natural transformations and adjunctions that are represented in the structural component. Not illustrated are the namespaces for monads and colimits. The structural component currently contains ~310 concepts (~335 terms with ~25 synonyms), partitioned into ~90 terms for graphs and their morphisms (gph.obj, gph.mor, free.obj, free.mor), ~45 terms for categories (cat), ~35 terms for functors (func), ~20 terms for natural transformations (nat), ~20 terms for adjunctions (adj, adj.mor), ~40 for monads (mnd, mnd.em, mnd.kli), and ~80 terms for colimits ( col, col.init, col.coprd2, col.coeq, col.psh).

Diagram 1: Type Level Structural Component Sets and Functions

Below we list the complete terminology for the structure component of the IFF-TYPE namespace. Look into the linked PDF files for more detailed comments and the axiomatization. The structure component of the IFF-TYPE namespace consists of several nested namespaces: graphs, categories, functors, natural transformations, adjunctions and monads namespaces.

graphs

This nested namespace axiomatizes (directed) graphs and their morphisms. A graph has a set of objects (nodes), and a set of morphisms (edges or arrows) that are directed from source node to target node. Graphs are connected by graph morphisms. A graph morphism from a source graph to a target graph has an object (morphism) function between object (morphism) sets of source graph and target graph. Graphs and graph morphisms form the (implicit) category Gph_type.

	IFF Set	IFF Function
.gph.obj
basics	graph isomorphic-relation subgraph-relation small-graph	object = node morphism = edge source target inclusion opposite
instances	empty two arrow three parallel-pair opspan span
horizontal	multipliable-pair	graph0 graph1 opspan multiplication unit tau
	multipliable-triple	multipliable-pair0 multipliable-pair1
.gph.mor
basics	graph-morphism	object = node morphism = edge source target opposite
	monomorphism epimorphism isomorphism	inverse
vertical	composable-pair	factor0 factor1 composition identity
horizontal	multipliable-pair	graph-morphism0 graph-morphism1 unit cone multiplication
coherence		associativity left right
.free.obj
free functor	free-functor	graph functor
diagram	diagram	graph-morphism category
		embedding-functor embedding free = path free-embedding = path-embedding
		path-opspan edge-morphism edge morphism path-triple path-set
		composition-diagram composition free-composition = path-composition
		restriction extension
.free.mor
		free-diagram free
	Technical and Recommended Prefix: type
	Table 3: The Type Graph Namespace

categories

This nested namespace axiomatizes categories. Categories represent (mathematical) contexts with structure. A category is a graph with an associative composition function and a unital identity function.

functors

This nested namespace axiomatizes functors. Categories are connected by functers. Functors are structure-preserving passages between categories. A functor is a graph morphism that preserves composition and identity. Categories and functors form the (implicit) category Cat_type.

natural transformations

This nested namespace axiomatizes natural transformations. Natural transformations enrich categories and functors, making Cat_type into a 2-category (a Cat-valued category).

adjunctions

This nested namespace axiomatizes adjunctions. Adjunctions are generalized inverse passages.

monads

This nested namespace axiomatizes monads. Monads generalize universal algebra. Each equational presentation defines a monad. Any adjunction defines a monad.