Seems like this is an extension of the Curry-Howard-Lambek isomorphism [1] relating type theory, logic and category theory together. I find that to be one of the most beautiful results in computer science and have been working on a practical language built on the same principles for a while (A mix of Haskell, Prolog and APL in a python-like language)
[1] https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence