>compare TM and LC You can, but Turing already did such in 1937 and showed equivalence of expressiveness. :p >The types themselves are not (programmatic) obje

>compare TM and LC You can, but Turing already did such in 1937 and showed equivalence of expressiveness. :p >The types themselves are not (programmatic) objects at all—they're merely the "objects" of the category. Do you mean 'programmatic' in the computational sense or categorical sense? Because, I was referring to the fact that every program (morphism) also has an equivalent function type (internal hom). Function types are objects within the Category as well. :) >If you use set comprehension to deal with the components of your category then you might end up with a Russel's paradox. It seems that this paper is using a set-theoretic comprehension for the concepts. Although, you could consider 'more powerful' constructions like Universes. I know a lot has been put into the study of LCs and I have nothing against studying them. I just have a personal preference to use other 'methods' to study computational theory. :p