if you get computation, you get the curry-howard-lambek correspondence for free. So you have an equivalence between logic as well as (cartesian closed) categories.
It also means some of those axioms are probably superfluous. It also means your bound by some of the same laws (? maybe the wrong term here?) that computation is (halting problem) etc.
It also means some of those axioms are probably superfluous. It also means your bound by some of the same laws (? maybe the wrong term here?) that computation is (halting problem) etc.