And if I got it right,

∂List = List × List -> two lists

I should also say that C needs to be a decidable container, meaning that the domain/codomain of ∂ is likely muddled even further?

But surely there is a (largest) subcategory of Cont for which the derivative is well-defined. Is it known what that subcategory is?

This is because its action on morphisms cannot be defined for an arbitrary lens (to see this, take the unique lens I -> 1, where I is the unit of the tensor product of containers, and 1 is the terminal container. Then the set of lenses ∂I -> ∂1 is empty.)

I do get a burst of inspiration every now and then. But these are few and far in-between.

Quite hoping it gets back - those have been good days, and I often think about how I wouldn't have become the mathematician and computer scientist I am today if it were not for those days

Is there a container interpretation in the case of an arbitrary category S?

This looks like it's a useful resource for thinking about this, though on the first glance it doesn't include anything about tree-shaped arrays, which I'd be very interested in

I'd been wondering myself about the foundations of the question of 'coordinate transformation' of the logical representation of multi-dimensional arrays or of general inductive types into a physical, 1d linear representation.

TLDR; insertion sort is dual to selection sort

"...duality among sorting algorithms: insertion sorts are dual to selection sorts."

First time I hear about this!

And this is the part where I conjecture that it has to be a certain kind of a fixpoint. But when it comes to deducing whether we're looking at
\mu(Ext(C)) or \nu(Ext(C)) I am actually not sure...

The natural way to formalise such an infinite product is by trying to compute the final coalgebra of the (- o C) functor, and see whether that gets us anything interesting.

I *think* this ought to hold also when \mu on the RHS is replaced with \nu

Actually, I don't think anymore we have the kleene star at hand.

I think now I have a working hypothesis which is the following:

\nu(- o C) \cong Const (\mu(Ext(C)))

With ordinary containers that gets muddled, so I'm looking to add an extra level of refinement. And singly indexed containers seem like the right thing to write some examples of