Relation Between Type Theory, Category Theory and Logicncatlab.org177 points·by rndn·il y a 11 ans·70 comments
rndn·il y a 11 ans·discussDoesn't the halting problem pose an obstacle in deciding whether two types act in an equivalent way (similar to how the equivalence between two programs is undecidable)?