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.
> 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.
Version 2.1.8p2
