feat: add DeepThunk

[Equilibris]

DeepThunk corresponds to the (co-)trace of a given polynomial functor, here we add the natural transformation required to generate them. These will later be used to inject into when generating syntax for codef syntax.

This commit simply adds the code without using it.

[AtticusKuhn]

It seems that this file involves some pretty dense Category Theory and many abstractions. Due to my limited knowledge of Category Theory, I don't really understand what's going on in this file, but I will cautiously approve this nonetheless.

[alexkeizer]

It seems that this file involves some pretty dense Category Theory and many abstractions. Due to my limited knowledge of Category Theory, I don't really understand what's going on in this file, but I will cautiously approve this nonetheless.

Reviewing code you don't understand can be a bit intimidating, but nonetheless having you look over it is very valuable!
Even if you don't understand the categorical nonsense, you can still look for "obvious" mistakes in style and such. It's completely fine to approve a file for style with the caveat that you didn't consider the bigger picture of it all.
So thanks for having a look anyway!

[alexkeizer]

Nice construction! I don't quite follow what the docstrings are saying, which probably means they could use some more love.

I like that you wrote a detailed intro, it's a complicated construction so having the context at the start is really nice!

[Equilibris]

Fixed the comments, feel free to take a look when you have time @alexkeizer

[alexkeizer]

LGTM

[alexkeizer]

I'm not sure if adding a link to ncatlab make the code more approachable (it's good to have references!) or less (people tend to be intimidated by ncat 🤣). Thanks for adding it, though, I guess ncat is the canonical source for categorical nonsense