[The IFF Metashell Type Namespace]

Overview

The core component of the type namespace of the IFF metashell (IFF-TYPE) is a medium-sized namespace (~ 450 terms, with ~ 230 terms in the kernel) located directly below the IFF-IFF namespace and directly above the core component of the IFF-META namespace. It enables declarations of all core component (and some structural component) meta things. Below we list the complete terminology for the core component of the IFF-TYPE namespace (emphasized terms were previously introduced in the IFF-IFF namspace). Look into the linked PDF files for more detailed comments and the axiomatization. The core component of the IFF-TYPE namespace consists of three nested namespaces: kernel, finite diagrams and finite limits namespaces.

kernel
The kernel nested namespace continues the axiomatization for the basic collections of sets and functions, and initiates the axiomatization for the other core concepts. By introducing basic terminology, it defines at the type level a finitely-complete category Set of Cantorian featureless sets and functions enriched with factorization and subobjects. In a standard fashion, the finitely-complete category Set defines the bicategory Span = spn(Set) of sets and spans, the ordered category Rel = rel(Set) of sets and (binary) relations, and their categorical connections. The category Set embeds into the other two (Figure 1), and there is an adjunctive structure Φ ⊣ Λ linking the embedding Λ and flattening Φ passages between Span and Rel: any relation is a span and any span flattens to a relation.
[Span-Relation Connection]
Figure 1: Span-Relation Connection
As Table 1 indicates, the type kernel implicitly specifies the various categorical, functorial and adjunctive structures illustrated in Figure 1.
IFF Term      Concept


Set, the category of sets and functions
type.set:set
obj(Set) = set, the object set of Set
type.ftn:function
mor(Set) = ftn, the morphism set of Set


Spn, the bicategory of sets and spans
type.set:set
obj(Spn) = set, the object set of Spn
type.spn:span
mor(Spn) = spn, the morphism set of Spn


Rel, the ordered category of sets and relations
type.set:set
obj(Rel) = set, the object set of Rel
type.rel:relation
mor(Rel) = rel, the morphism set of Rel



∝ : Spnop → Spn, the involution
implicit identity on type.set:set
obj(∝), the object function of ∝
type.spn:opposite
mor(∝), the morphism function of ∝


∝ : Relop → Rel, the involution
implicit identity on type.set:set
obj(∝), the object function of ∝
type.rel:opposite
mor(∝), the morphism function of ∝


Φ : Spn → Rel, the flattening functor
implicit identity on type.set:set
obj(Φ), the object function of Φ
type.spn:relation
mor(Φ), the morphism function of Φ


Λ : Rel → Spn, the embedding functor
implicit identity on type.set:set
obj(Λ), the object function of Λ
type.rel:span
mor(Λ), the morphism function of Λ



η : 1 ⇒ Φ ∘ Λ, the unit natural transformation
type.spn:unit
cmp(η), the component function of η
Table 1: IFF Representation of Mathematical Concepts
In addition to canonical functionality for finite limits, Set has factorizations and subobjects. The kernel namespace introduces the concepts and basic terminology for subobjects, and it also introduces the categorical approach to membership and inclusion. The fundamental relations in the kernel namespace are (Figure 2) function and span belonging (⇒), predicate and relation inclusion (⊆), function-predicate and span-relation membership (∈) with associated proof operation (⊢), function-set and span-set-pair elementhood (:).
[IFF Subobject Architecture]
Figure 2: Subobject Architecture
As Table 2 indicates, the type kernel explicitly specifies the various subobject structures illustrated in Figure 2.
IFF Term      Concept


(ftn, ⇒), function belonging preorder
type.ftn:belonging
ext(⇒), extent set of ⇒
type.ftn:element0
π0 : ext(⇒) → ftn, the 0th projection function of ⇒
type.ftn:element1
π1 : ext(⇒) → ftn, the 1th projection function of ⇒


(spn, ⇒), span belonging preorder
type.spn:belonging
ext(⇒), the extent set of ⇒
type.spn:element0
π0 : ext(⇒) → spn, the 0th projection function of ⇒
type.spn:element1
π1 : ext(⇒) → spn, the 1th projection function of ⇒


(pred, ⊆), predicate inclusion (subset) order
type.pred:inclusion-relation
ext(⊆), the extent set of ⊆
type.pred:part0
π0 : ext(⊆) → pred, the 0th projection function of ⊆
type.pred:part1
π1 : ext(⊆) → pred, the 1th projection function of ⊆


(rel, ⊆), relation inclusion (subset) order
type.rel:inclusion-relation
ext(⊆), the extent set of ⊆
type.rel:part0
π0 : ext(⊆) → rel, the 0th projection function of ⊆
type.rel:part1
π1 : ext(⊆) → rel, the 1th projection function of ⊆


∈ : ftn ⇁ pred, function-predicate membership relation
type.pred:membership
ext(∈), the extent set of ∈
type.pred:element
π0 : ext(∈) → ftn, the 0th projection function of ∈
type.pred:part
π1 : ext(∈) → pred, the 1th projection function of ∈
type.pred:proof
⊢ : ext(∈) → ftn, the proof function of ∈


∈ : spn ⇁ rel, span-relation membership relation
type.rel:membership
ext(∈), the extent set of ∈
type.rel:element
π0 : ext(∈) → spn, the 0th projection function of ∈
type.rel:part
π1 : ext(∈) → rel, the 1th projection function of ∈
type.rel:proof
⊢ : ext(∈) → ftn, the proof function of ∈
Table 2: IFF Representation of Mathematical Concepts
As illustrated in Figure 3, the type kernel namespace consists of five nested namespaces: set, function, span, predicate and relation.
Figure 3: Namespaces

(type)

set
(unary)ftnpred
(binary)spnrel

(element)(part)
  • The set (sketch) namespace terminology is listed in Table 3. This consists of 42 terms and 36 concepts (6 synonyms) representing the set basic collection and its components, and subobject structure.

IFF SetIFF Function
.set
basicsset isomorphic-relation
[in]finite-set
binary-(union | intersection) difference
instanceszero = initial = empty
one = terminal two three		constant-zero constant-one
counique unique
subobjectsubset-relationsmaller larger inclusion predicate
power power-pair
leq bottom top binary-(join | meet)
minus complement implication
singleton union = join intersection = meet


exists = power inverse-image forall

Technical Prefix: type.krnl
Recommended Prefix: type

Table 3: The Type Set Namespace
  • The function namespace terminology is listed in Table 4. This consists of 57 terms and concepts representing the concepts of function, function (optimal-)restriction order, composition functionality, element, application functionality, factorization, conversion to other kinds, function morphism and belonging order.

IFF SetIFF Function
.ftn
basicsfunction
[optimal-]restriction-relation		source target
[optimal-](smaller | larger)

element
constant-function		set
constant-element construction
category theorycomposable-pairfactor0 factor1 composition identity

appliable-pairelement-factor function-factor
application
factorization
injection
surjection
bijection		range kernel coimage
injective-factor coapplication
surjective-factor coequalizer
inverse
conversion
predicate span relation fiber unit
instances
initial terminal counique unique


.ftn.mor
basics2-cell
belonging
equivalence isomorphism		source target function
element0 element1
category theorycomposable-pairfactor0 factor1 composition identity

Technical Prefix: type.krnl
Recommended Prefix: type

Table 4: The Type Function Namespace
  • The spannamespace terminology is listed in Table 5. This consists of 72 terms representing 69 concepts (3 synonyms) of span, span abridgment order, composition functionality, factorization, conversion to other kinds, span morphism and belonging order.

IFF SetIFF Function
.spn
basicsspan

abridgment-relation		set = vertex set0 set1 set-pair
function0 function1 function-pair
smaller larger
category theorycomposable-pairfactor0 factor1 opspan composition identity

combinable-paircomponent0 component1 combination
factorization
injection
surjection
bijection		extent = range kernel coimage
injective-factor coapplication
surjective-factor coequalizer
conversion
opposite function relation unit
instances
initial terminal counique unique
basicsendospanset
order theoryreflexive-span
transitive-span
symmetric-span

proto-category
equivalence-span


.spn.mor
basics2-cell
belonging
equivalence isomorphism		source target function = vertex set0 set1
element0 element1
conversion
function-2-cell
.spn.mor.vrt


composable-pairfactor0 factor1 composition identity
.spn.mor.hrz


composable-pairfactor0 factor1 composition identity
opspan-morphism

Technical Prefix: type.krnl
Recommended Prefix: type

Table 5: The Type Span Namespace
  • The predicatenamespace terminology is listed in Table 6. This consists of 18 terms and 17 concepts (1 synonym) representing the predicate basic collection and its components, predicate delimitation order, conversion maps, subobject order, and the membership relation (with proof operator) between generalized elements (functions) and parts (predicates).

IFF SetIFF Function
.pred
basicspredicate
strict-predicate canon
delimitation-relation		genus differentia

smaller larger
conversion
function subordinate injection
subobjectinclusion-relation
equivalence = isomorphism		part0 part1

membershipelement part proof

Technical Prefix: type.krnl
Recommended Prefix: type

Table 6: The Type Predicate Namespace
  • The relation namespace terminology is listed in Table 7. This consists of 43 terms and 42 concepts (1 synonym) representing the relation basic collection and its components, relation abridgment order, category theory, conversion maps, subobject order, the membership relation (with proof operator) between generalized element pairs (spans) and binary parts (relations), and endorelation subtypes.

IFF SetIFF Function
.rel
basicsrelation
strict-relation canon
abridgment-relation		extent set0 set1 set-pair
projection0 projection1
smaller larger
category theorycomposable-pairfactor0 factor1 composition identity
conversion
function predicate span injection
opposite fiber01 fiber10
subobjectinclusion-relation
equivalence = isomorphism		part0 part1

membershipelement part proof
basicsendorelationset
order theoryreflexive-relation
transitive-relation
antisymmetric-relation
symmetric-relation

preorder partial-order
equivalence-relation
respects-relation
quotient canon

Technical Prefix: type.krnl
Recommended Prefix: type

Table 7: The Type Relation Namespace
finite diagrams
The finite diagram nested namespace essentially defines four categories of diagrams (Figure 4): 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), the (comma) category Ppr = (Δ, Δ) of parallel pairs and parallel pair morphisms (diagrams for equalizers), and the (comma) category Ospn = (1, Δ) of opspans and opspan morphisms (diagrams for pullbacks).
[Categories of Diagrams]
Figure 4: Categories of Diagrams
As Table 9 indicates, the type kernel implicitly specifies the various diagram and limit structures illustrated in Figures 3.
IFF Term      Concept
type.dgm



Set2, the category of set pairs and function pairs
.pr.obj:set-pair
obj(Set2) = set2, the object set of Set2
.pr.mor:function-pair
mor(Set2) = ftn2, the morphism set of Set2


Set3, the category of set triples and function triples
.trp.obj:set-triple
obj(Set3) = set3, the object set of Set3
.trp.mor:function-triple
mor(Set3) = ftn3, the morphism set of Set3


Ppr, the category of parallel pairs and their morphisms
.ppr.obj:parallel-pair
obj(Ppr) = ppr, the object set of Ppr
.ppr.mor:parallel-pair-morphism
mor(Ppr), the morphism set of Ppr


Ospn, the category of opspans and their morphisms
.ospn.obj:opspan
obj(Ospn) = Ospn, the object set of Ospn
.ospn.mor:opspan-morphism
mor(Ospn), the morphism set of Ospn



C = Set2, Set3, Ppr or Ospn
  pre = pr, trp, ppr, ospn
Δ : Set → C, the constant functor
.pre.obj:constant
obj(Δ), the object function of Δ
.pre.mor:constant
mor(Δ), the morphism function of Δ
 gph = • •,  • • •,  • ⇉ •  or  • → • ← •
C = Set2, Set3, Ppr or  Ospn
  pre = pr, trp, ppr, ospn
πk : C → Set, the kth projection functor, k ∈ node(gph)
.pre.obj:set(0 | 1)
obj(πk), the object function of πk
.pre.mor:function(0 | 1)
mor(πk), the morphism function of πk


E : Ospn → Ppr, the op-pairing functor
.opsn.obj:parallel-pair
obj(E), the object function of E
.opsn.mor:parallel-pair-morphism
mor(E), the morphism function of E
Table 3: IFF Representation of Mathematical Concepts
The diagram namespace terminology is listed in Table 8. This consists of 91 terms and 85 concepts (6 synonyms) representing the four basic types of things (Set2, Set3, Ppr, Ospn) and their components, category theory, and conversion maps.

IFF SetIFF Function
.pr.obj
basicsset-pairset0 set1
conversion
opspan opposite constant
.pr.mor

basicsfunction-pairsource target function0 function1
conversion
opspan-morphism opposite constant
category theorycomposable-pairfactor0 factor1 composition identity


.trp.obj
basicsset-tripleset0 set1 set2 = set set-pair
conversion
constant
.trp.mor

basicsfunction-triplesource target
function0 function1 function2 = function function-pair
conversion
constant
category theorycomposable-pairfactor0 factor1 composition identity


.ppr.obj
basicsparallel-pairfunction0 function1 function-pair set0 set1 set-pair
conversion
constant
.ppr.mor

basicsparallel-pair-morphismsource target function0 function1 function-pair
conversion
constant
category theorycomposable-pairfactor0 factor1 composition identity


.ospn.obj
basicsopspanfunction0 = opzeroth function1 = opfirst function-pair
set0 set1 set = opvertex set-pair
conversion
parallel-pair relation opposite constant
.ospn.mor

basicsopspan-morphismsource target
function0 function1 function = opvertex function-pair
conversion
parallel-pair-morphism opposite constant
category theorycomposable-pairfactor0 factor1 composition identity

Technical and Recommended Prefix: type.dgm

Table 8: The Type Finite Diagram Namespace
finite limits
The nested namespace for finite limits essentially defines four adjunctions (Figure 5) between the constant functor and “the” limit functor*: binary products on pairs of sets and their functions, ternary products on triples of sets and their functions, equalizers on parallel pairs (of functions) and their morphisms, and pullbacks on opspans and their morphisms. It uses the first order expression of adjunctive style axiomatization. The terminology of this namespace, which is listed in Table 9, consists of 131 terms and 131 concepts (with no synonyms). There are six types of limit according to diagram shape: binary and ternary products and their power variants, equalizers and pullbacks.
[Constant-Limit Adjunctions]
Figure 5: Constant-Limit Adjunctions
As Table 9 indicates, the type kernel implicitly specifies the various diagram and limit structures illustrated in Figure 4.
*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.

IFF SetIFF Function


.prd2.objconeset function-pair function0 function1 cone-set-pair opposite

mediatormediator-set function set-pair


delta-cone delta delta-function


projection-mediator projection product projection-function-pair
projection0 projection1
tau-cone


packing pairing unpacking components
tau
.prd2.mor
product


.pwr2.objconeset function-pair function0 function1 cone-set


power projection-function-pair
projection0 projection1 pairing
.pwr2.mor
power




.prd3.objconeset function-triple function0 function1 function2 cone-set-triple

mediatormediator-set function set-triple


delta-cone delta delta-function


projection-mediator projection product projection-function-triple
projection0 projection1 projection2


packing tripling unpacking components
.prd3.mor
product


.pwr3.objconeset function-triple function0 function1 function2 cone-set


power projection-function-triple
projection0 projection1 projection2 tripling
.pwr3.mor
power




.equ.objconeset parallel-pair-morphism function0 cone-parallel-pair

mediatormediator-set function parallel-pair


delta-cone delta delta-function


projection-mediator projection equalizer projection-parallel-pair-morphism
projection-function-pair projection0


packing parting unpacking
.equ.mor
equalizer




.pbk.objconeset opspan-morphism function0 function1 cone-opspan opposite

mediatormediator-set function opspan


delta-cone delta delta-function


projection-mediator projection pullback projection-opspan-morphism
projection-function-pair projection0 projection1
tau-cone injection-cone injection


packing pairing unpacking components
tau
.pbk.mor
pullback

Technical and Recommended Prefix: type.lim

Table 9: The Type Finite Limit Namespace