What is undecidability within the computational trilogy

232 Views Asked by At

The computational trilogy page on nLab gives a nice "Rosetta stone" that translates concepts between the theories of logic, category theory, and type theory. However, one concept it does not list is undecidability, so I am just wondering if undecidability has any special meaning from the category theory perspective or -- especially -- from the type theory perspective. Or, in general, do Gödel's Incompleteness Theorems have any special meanings from these perspectives?