Overview

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 IFF-META namespace. It enables declarations of all meta things. The IFF-TYPE namespace is the freest formalism with respect to first order expression, not just in the metashell, but in the entire IFF: since the central goal of the IFF-IFF namespace above is to establish the fundamental types of sets and functions, it does not actually use the full capabilities of first order logical expression; and in the IFF-META namespace below, a large part of the kernel is the specialization (using subset, delimitation, (optimal-)restriction and abridgment) of the IFF-TYPE namespace kernel, the nested IFF-META diagram namespace uses to a great extent the type terminology, and the nested IFF-META limit namespace uses atomic expression of adjunctive style axiomatization. For these reasons, it would seem that the IFF-TYPE namespace is the location in the IFF where set theory reigns supreme and category theory is non-existent. While this may be true when looking only at the narrowest scope of the code, since it is full first order expression, it is misleading when we expand our horizons. First, the core component of the IFF-TYPE namespace has an implicit category-theoretic structure, since composition and identity are introduced here, implicitly giving us the categories Set, Rel and Span. Second, since the largest number of its terms are used at the lower levels for defining special finite diagrams and limits, the IFF-TYPE namespace has an explicit category-theoretic purpose.

Author: Robert E. Kent