Consider a category $ mathcal {C} $ contains a natural number object mathbb {N} as well as objects and arrows $ X overset {p} { leftarrow} Y overset {f} { rightarrow} mathbb {N} $, We are often interested in one $ mathbb {N} $-Value up $ X $ by "folding" over the fibers of $ Y $, Write $ Y_x: = p ^ {- 1} (x) $Some examples include

Map($ X $): $ 1 leftarrow X overset {! 1} { to} ( mathbb {N}, +) $

Total($ f: X to mathbb {N} $): $ 1 leftarrow X overset {f} { to} ( mathbb {N}, +) $

Prod ($ f: X to mathbb {N} $): $ 1 leftarrow X overset {f} { to} ( mathbb {N}, times) $

Although these values are determined canonically, they do not (generally) define global elements $ 1 to mathbb {N} $ in the $ mathcal {C} $, The easiest way to recognize this is to note that global elements must be preserved through natural transformations between presheaves, but cardinality, etc., does not.

Question 1) What type of categorical structure is required to internalize fiber aggregations like the ones mentioned above?

Guess: We have to assume that $ mathbb {N} $ is an object classifier in internal theory. Then we can map $ X to mathbb {N} $ unique ($ x mapsto Card (Y_x) $) and an ambiguous one $ Y to mathbb {K} $ The resulting square becomes a pullback. Then we can extend $ f $ to $ mathbb {K} $ (e.g. expansion by zero or one) and define the aggregations using recursive definitions.

Question 2) What explains the failure of the naturalness of these aggregates? Does it arise from the use of a universe or does it possibly indicate a hidden dependency on Heyting / dependent product structures? Is there a weakening or generalization of naturalness that still applies to these more general arrows?

References for this and related topics are very much appreciated.