Jonathan Castello wrote:

> This is the kind of statement that fascinates me to no end, yet I have no idea how to start understanding where these kinds of constructions come from. Can you recommend any resources for acquiring the necessary background?

There's a very rich set of connections between category theory, logic, and computation. Since I don't know what you know, it's a bit tricky to suggest what to read next. For category theory and computation try this:

* Bartosz Milewski, _[Category Theory for Programmers](https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/)._

This might be helpful as well:

* Samson Abramsky and Nikos Tzevelekos, _[Introduction to Categories and Categorical Logic](https://arxiv.org/abs/1102.1313)._

Both discuss the Curry-Howard correspondence, which is one of the main links worth understanding.

I also suggest that you ask hundreds of small, specific questions on this forum.