[mlochbaum]

I doubt it? Universal constructions give a nice definition for a few operations but I doubt they have the power to pull out all primitives, that is, select out of all the well-defined things you could do the ones that are natural or useful. Can Indices[0] be constructed as a universal morphism? Is defining it in this way simpler than an algorithmic definition, which can be quite short? One of the properties of primitives I list is that they tend to have short definitions, so constructive definition is already a sort of filter that prefers primitives. Universal morphisms might be another, even a more useful, filter, but probably not a perfect filter.

Although, if you're here... there's a more focused question that's been bothering me because I feel it should appear in category theory but can't locate it. There's an operation I call Under that I partially introduce at [1] and define at [2]. The idea is that given functions F and G, where G manipulates things in some overall framework like arrays, F⌾G is a function so that F⌾G x is as similar as possible to x while satisfying (G F⌾G x) = G x. Maybe it's a sort of pullback along a functor G. Does that look familiar?

[0] https://mlochbaum.github.io/BQN/doc/replicate.html

[1] https://mlochbaum.github.io/BQN/tutorial/variable.html#modif...

[2] https://mlochbaum.github.io/BQN/spec/inferred.html#under

[drdeca]

While I haven’t (yet?) taken the time to understand the notation you are using to define this “under” operation, it sounds a little like an adjoint of a functor?

But I could very well be totally off.

[mlochbaum]

The structure is pretty similar. If you could encode array structures into categories (part of my problem is I don't know how to do this effectively: are the structures objects, or categories?), then my take is that a structural function that extracts some part of an array should give a functor G. Then a right adjoint ⌾G puts the omitted structure back. But I don't think this can work, because the definition of an adjoint says morphisms in the target of G exactly correspond to morphisms in its source, when ⌾G is used to find the codomain. This doesn't match up: if G extracts structure, then it should collapse some functions together, when they only differ in what they do to the parts of the array that get left out.

Most of my problem seems to be that the definition of Under really depends on applying functions to particular arguments. So it's hard to see how to set up categories to capture the necessary properties. But I don't know if it's actually hard to do or just confusing.