As a simplification in coding the axiomatization of the generic core, initially we will not specify the metastack links between the natural part and the metashell. Whether this simplification is permanent can be decided in the future (see the discussion about
an Ur simplification). This does not affect the metastack links within the natural part. An example from generic functions will serve to explain this simplification.
Each generic function f : X → Y has a unique generic source set X (and a unique generic target set Y). Here is the unsimplified code for the source function.
((#n+1).ftn:function source)
(= ((#n+1).ftn:source source) function)
(= ((#n+1).ftn:target source) #n.set:set)
((#n+2).ftn:restriction source (#n+1).ftn:source)
(type.ftn:restriction source meta.set:source)
This contains a metastack link internal to the natural part and a metastack link between the natural part and the metashell. By eliminating the latter, the code is simplified.
((#n+1).ftn:function source)
(= ((#n+1).ftn:source source) function)
(= ((#n+1).ftn:target source) #n.set:set)
((#n+2).ftn:restriction source (#n+1).ftn:source)