An IFF Simplification

There is a significant simplification in the IFF architecture and code. The assertion that the categories, functors and natural transformations (at the metalevel of the metashell) form a 2-category needs suitable terminology axiomatized in the structural component of the type namespace (IFF-TYPE) of the metashell (level type = ∞+2). Similarly, the assertion that categories, functors and natural-transformations (at level n) form a 2-category needs suitable terminology axiomatized in the structural component of level n+1. However, level n and level n+1 are represented by the same axiomatization. This is the meaning when we say that the pure aspect of the natural part is generic. These observations suggest that making structural assertions (such as category-ness, 2-category-ness, double-category-ness, bicategory-ness, …) at finite metalevels allows significant simplification, since then such structural axiomatizations would need to be created just once (generically). Currently, the basic structural axiomatization for category-ness (containing the basic concepts for categories, graphs, functors, natrual transformations, adjunctions, monads, …) is nearly compliant with categorical design, and it is assumed that the other structural axiomatizations mentioned above would also be so compliant. Hence, the question presents itself: Do we really need the Ur meta-level?

Point 1: In the kernel namespace at level n, the collection set_n is specified to be a subset of both the level n+1 collection of sets set_n ⊆ set_n+1 and the Ur level collection of sets set_n ⊆ set_∞. The first constraint is required, since it is a basic constraint for the metastack. However, the second constraint is more problematic – its purpose is part of the specification that the Ur level is the cumulative generic level for the natural part.
Point 2: Similarly, in the kernel namespace at level n, the two metastack constraints set_n ⊆ set_∞ and set_∞ ⊆ set_meta are equivalent to the metastack constraint set_n ⊆ set_meta.
Point 3: In one sense, the Ur level axiomatization is somewhat redundant, since it is just the specialization of the meta level axiomatization, using the metastack constraints of subset, predicate delimitation, function (optimal-)restriction and relation abridgment.

Eliminating the Ur level axiomatization would clearly make the axiomatization much simpler. But, elimination of the Ur level axiomatization requires that we also eliminate the metastack constraints such as set_n ⊆ set_∞. Following this, there is one further design decision. Should we add the metastack constraints of the form set_n ⊆ set_meta or not? If metastack constraints of the form set_n ⊆ set_∞ (and similar constraints for predicates, functions and relations) are elminated without adding metastack constraints of the form set_n ⊆ set_meta, the natural part of the IFF would become disconnected from the metashell. In this case, following the principle of conceptual warrant, the metashell would lose its raison d'être. This would argue for elimination of the entire metashell. By eliminating the metashell, the natural part would become the full IFF axiomatization. But note that the pointwise set-theoretical foundation of the IFF exists only in the metashell. Hence, assuming complete compliance of the natural part with the principle of categorical design, the natural part, and hence the full IFF axiomatization, would have only a pointless set-theoretic axiomatization (in the generic core) and a category-theoretic foundation (in the generic structure), and these would be expressed atomically by means of some declarations, some relational expressions, but mainly commutative diagrams.