The pure aspect of the natural part of the IFF architecture is partitioned into a core component and a structural component. The core component represents set theory. The structural component represents category theory. The set-theoretic and category-theoretic axiomatizations constrain each other (Figure 1): any category is defined as a set of objects and a set of morphisms with connecting functions; whereas the collections of sets and functions (at any metalevel) form a category (actually, a topos at finite and meta levels and a fintely-complete category at the type level). The core and structural components correspond to the distinction between the foundations and organization of mathematics as discussed in the presentation Kreisel and Lawvere by J.P. Marquis. This component architecture of the IFF, which is forced by the principles of conceptual warrant and categorical design, agrees with Marquis’s claim that “We can have both worlds!”.

Setmeta∈obj(Cattype)    Cattype=cat(Settype)
  ⋯  
Setn∈obj(Catn+1)    Catn+1=cat(Setn+1)
Setn−1∈obj(Catn)    Catn=cat(Setn)
  ⋯  
Set2∈obj(Cat3)    Cat3=cat(Set3)
Set1∈obj(Cat2)    Cat2=cat(Set2)
    Cat1=cat(Set1)
Figure 1: Topos Chain

Core Component

Core refers to things that are basic, central, essential or foundational. The core component of the IFF architecture at level n contains a single generic meta-ontology IFF-SET, which incorporates the specialization (a technical concept of IFF development) of the level n+1 version of itself and/or the IFF-META namespace from the metashell. The IFF-SET meta-ontology specifies set theory as a chain of toposes

Set  =  ‹Set1 ⊂ Set2 ⊂ Set3 ⊂ … ⊂ Setn ⊂ …›

of Cantorian featureless abstract sets called the IFF metastack. Here Set1 contains “small” sets and functions between “small” sets, Set2 contains “large” sets and functions between “large” sets, et cetera. Since the kernel of the IFF-SET meta-ontology (which axiomatizes this topos hierarchy), together with the kernel of the metashell, is already called the IFF metastack, this is a (quite useful) abuse of terminology. This chain is motivated by and compatible with the Cantorian expansion of sets. The set-theoretic concepts in the core component of the IFF (the core concepts) are structurally described (Figure 1) in terms of the category-theoretic concepts in the structural component

« Setn ∈ obj(Catn+1), for all 1 ≤ n »

— the structural component provides the category-theoretic support for the core component. To satisfy categorical design, the assertion of the topos structure of Set at any metalevel n needs suitable terminology axiomatized at the next higher metalevel n+1 in the structural component (of the pure aspect). The assertion that Set1 is a topos needs suitable terminology axiomatized in the structural component at level 2. More generally, any large category (such as the category Top of topological spaces and continuous maps) is axiomatized at level 1, possibly in the applied aspect; but the axiomatization for the terminology of large categories occurs in the IFF-CAT meta-ontology at level 2. For any level n, the assertion that Setn is a topos needs suitable terminology axiomatized in the structural component at level n+1. The core component of the IFF architecture provides an adequate set-theoretic foundation for representing and maintaining object-level ontologies and for defining other metalevel ontologies, since the metastack (the kernel subnamespaces of the IFF-SET meta-ontology and the IFF-META/TYPE namespaces) contains atomic namespaces for core concepts (basic collections, metastack partial orders, and fundamental relations).

Structure Component

Structure refers to arrangement, aggregate or pattern of organization. The structural component of the IFF architecture contains various generic meta-ontologies for category theory, (IFF-CAT, IFF-2CAT, IFF-DCAT, …). By axiomatizing the basic concepts of category theory, such as categories, functors, natural transformations, adjunctions and monads, the IFF-CAT meta-ontology specifies category theory as a chain of internal categories

Cat  =  ‹Cat1 ⊂ Cat2 ⊂ Cat3 ⊂ … ⊂ Catn ⊂ …›

in the toposes Set. The structural component of the IFF provides adequate category-theoretic organizational terminology for representing and maintaining object-level ontologies and for defining other metalevel ontologies. The structural component at the nth metalevel has a basic category namespace in the IFF-CAT meta-ontology, which axiomatizes objects, morphisms and their composition. To satisfy categorical design, this axiomatization foundationally requires the core concepts and finite limits in the IFF-SET meta-ontology of the core component at the next higher metalevel n+1 (and in the IFF-META namespace of the metashell). In the metashell, the category subnamespace in the structural component of the IFF-META namespace requires the core concepts and finite limits in the IFF-TYPE namespace in the core component of the metashell. In particular, the adjunctive style for the IFF axiomatization is initiated in the subnamespace for finite limits of type sets and type functions. The IFF-CAT meta-ontology follows Mac Lane’s beginning axiomatization for category theory (Mac Lane, 1971), in that it introduces terminology and provides an axiomatization for this terminology, but it does not give a formal interpretation using set theory: it only gives an informal, intuitive interpretation. The IFF-SET meta-ontology completes such a formal interpretation. The category-theoretic concepts in the structural component of the IFF are described (Figure 1) in terms of the set-theoretic concepts in the core component (the core concepts)

« Catn = cat(Setn), for all 1 ≤ n »

— the core component provides the set-theoretic support for the structural component. The generic level axiomatizations for the selected topos-representing terms in Table 2 justify the assertion: for each n, the category Setn of level n sets and functions is a topos.

IFF Term      Concept
#n:Set      Setn
#n.set:set      obj(Setn)
#n.set:power      obj(PSetn)
#n.set:{zero, one, two}      0Setn, 1Setn, 2Setn = ΩSetn
#n.ftn:function      mor(Setn)
#n.ftn:power      mor(PSetn)
#n.ftn:composition      ∘Setn
#n.ftn:identity      1Setn
#n.pred:fiber      SubSetn
#n.pred:binary-meet      ∧Setn
#n.rel:fiber01      φ01Setn
#n.lim.prod2.obj:product      ×Setn
#n.lim.prod2.obj:projection {0, 1}      πiSetn,   i = 0, 1
#n.exp.obj:exponent      BA
#n.exp.obj:evaluation      BA × A → B
#n.exp.obj:hom      Setn[‒,‒]
#n.exp.obj:curry      Setn[C × A, B] → Setn[C, BA]
Table 2: Setn as a Topos