From the lens of the Curry-Howard isomorphism where logic, category theory and type theory are just different perspectives on the same sort of mental human acti

From the lens of the Curry-Howard isomorphism where logic, category theory and type theory are just different perspectives on the same sort of mental human activity... Implication (logic) is the same thing as internal hom (Category theory); or Function type (type theory). It is just syntax. B |- A in logic translates to f::B -> A in Haskell. https://ncatlab.org/nlab/show/computational%20trilogy#rosetta_stone https://ncatlab.org/nlab/show/computational%20trilogy#rosett... And then the context left implicit is the transformation of B to A e.g the concrete steps for tranforming B to A. The implementation of f. There is no escaping The Hierarchy. https://en.wikipedia.org/wiki/Chomsky_hierarchy#The_hierarchy https://en.wikipedia.org/wiki/Chomsky_hierarchy#The_hierarch...