|
|
|||
| |
The IFF Kind Namespace |
||
| |
|||
| |
The kind namespace of the IFF metashell (IFF-KIND) is a small-sized namespace consisting of 289 terms and 265 concepts (24 synonyms). It is located directly below the iff namespace and directly above the type namespace, and provides declarations for all type things. The kind namespace consists of three nested namespaces. |
 |
|
|
The kernel nested namespace
continues the axiomatization for sets, predicates
(unary relations), (unary)
functions and
(binary) relations. It also continues the axiomatization for the
subset,
predicate delimitation, function (optimal-) restriction and relation
abridgment partial orders. It introduces basic terminology for the
category Set
of sets and functions, the category SetP
of sets and multivalued functions and the category Rel (=̃ SetP)
of sets and
relations. It introduces basic terminology for subobjects, and it also
introduces basic terminology for order theory. |
|||
|
The finite diagram nested namespace essentially defines three categories of diagrams: the category Set2 of set pairs and function pairs (diagrams for binary products), the category Set3 of set triples and function triples (diagrams for ternary products), and the (comma) category Ospn = (1, Δ) of opspans and opspan morphisms (diagrams for pullbacks). |
|||
|
The finite limit nested
namespace essentially defines three adjunctions between the
constant functor and ``the'' limit functor*: binary products on pairs
of sets and functions, ternary products on triples of sets and
functions, and pullbacks on opspans and opspan morphisms. It uses the
first order expression of adjunctive style axiomatization. |
|||
| *The
definite article is in quotes, since the limit functor is unique only
up to isomorphism. Theoretically, this is well understood and
immediately dismissed. But practically, this issue is important, since
it affects the axiomatization. The use of a strict category-theoretic
axiomatization, such as the adjunctive-style axiomatization for limits
and exponents that is favored in the IFF specification, does not give a
concrete limit, and hence can be regarded as an under-specified
axiomatization. An additional axiom is needed for a full concrete
specification. In the IFF, this additional axiom is added, not at the
point where the limit is initially axiomatized, such as in this
namespace, but at a lower metalevel, where the limit is used. |
|||
| unions and
universes |
In the
current version of the IFF, although we have bounded unions at every
metalevel, we have no use for either local (unbounded) unions or
universes. However, here we show how they could be defined within the
IFF. |
||
|
The kind 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 namespace above is to establish the fundamental types, it does not actually use the full capabilities of first order logical expression; and in the type namespace below, a large part of the kernel is the specialization (using subset, delimitation, (optimal-)restriction and abridgment) of the kind namespace kernel, the nested diagram namespace uses to a great extent the kind terminology, and the nested limit namespace uses atomic expression of adjunctive style axiomatization. For these reasons, it would seem that the kind 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 kind namespace has an implicit category-theoretic structure, since composition and identity are introduced here, implicitly giving us the categories Set and Rel. Second, since the largest number of its terms are used at the lower levels for defining special finite diagrams and limits, the kind namespace has an explicit category-theoretic purpose. |
|||