[giomasce]

I'd put that in a different way: the point of maths is not really being context-independent, but to make it very clear what is the context. So, let us consider a statement A which is true provided that a certain set of hypotheses B is true. You might either consider that "A is true in the context of B" (what is commonly written as "B |- A"), so you have a context (but it is very clearly stated what it is). Or you can (often) write it as an implication: "B -> A". The whole sentence "B -> A" is an absolute, it has no context any more, because the context has been absorbed in the antecedent.

(yes, I know I am oversimplifying something, take this at the "philosophical" level)

[ukj]

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#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_hierarch...