Hi Martin, Thanks for your response. My catlist posting was using rather general formulations but there are underlying detail that can be found in our papers. Let me add just a few historical remarks. One main idea of our work is that their is a "lativity" in logic that is not respected. It's not comparable to the "lativity" in set theory where you can create classes out of sets, but you cannot throw classes back into the basket of sets, whatever that would be. The same thing happens in logic. We must start with the signature, based on which we construct terms, and terms are used inside sentences. Once we have the "bag of sentences" we may proceed "latively" to construct other things. When we eventually come to proof rules, the bag of sentences was closed a long time ago. Yet, G??del uses "provability" to create new sentences, and simply opens up that bag of sentences, and throws in these new ones. It has always been accepted, but this in fact breaches the lativity principle, which indeed is not respected in logic. The lativity principle cannot be formulated in set theory alone, and set theory is also very much untyped, we have to say. It basically also boils down to separating object languages from their metalanguages. First-order logic as developed from a fons-et-origo becomes acceptable over decades while being developed hand-in-hand, so as to say, with set theory. Type constructors in type theory are good examples that basically appear in no language whatsoever. They are simply brought in from the outside, almost like a holy spirit. But then we have category theory, and in our approach we use it as an object language where that hand-in-hand appears as a metalanguage. And then I turn category theory into a new metalanguage in order to deal with lativity of logic. There is a bit of lativity in Goguen-Burstall's and Meseguer's general models, but unfortunately types do not explicitly occur since the Sign category is considered as abstract until it is made precise for particular logics. And when it's made "precise" e.g. for first-order, it simply adopts e.g. the traditional explanation of terms, so they are not formally constructed within that categorical metalanguage. This is of course then the also reason why the Cat theory enters when dealing with semantics. It's also too general. Yes, we cannot create the set of all sets, similarly as we shouldn't even try out creating the type of all types. Nevertheless, Martin-L??f took the liberty of doing that, and was opportunistic enough to publish it. Things went wrong but it was not called a paradox. Constructions were "improved" over decades, but the HoTT community still uses universality, so that paradox just appears as the emperors new clothes. Sch??nfinkel, Curry and Church saw all these problems, and Hilbert saw it, too, of course, since all of these three were discussing these quite frequently over many years in G??ttingen. Hilbert never wrote anything about it, but probably because he couldn't solve it (or wasn't interested in medals), and he was becoming too old at that time anyway. Sch??nfinkel and Church write more explicitly that something remains to be understood, but Curry less so. Curry just went on even if the foundations were shaky. Kleene never did that, and he was in any case cleaning up other things. von Neumann probably saw what was going on, but he kept himself always out of that mess. So when that mess now has rooted itself like the Mentha Piperita, opportunists travel around, and the bank voles follow them.

I am not sure why these questions are being asked in this list:

In our work now it's indeed about understanding that lativity, and these questions turn up when we use categories as a metalanguage for logic. We thereby also say that types are not fundamental, but rather given because of an object in a category. We also see how we need to debate category theory itself. Take monoidal categories. They are not really categories, are they? They do contain a category, but they are not categories. They are not algebraic structures either, are they? Freeness issues become tricky, and it becomes doubtful if universal algebra can overcoat lativity of logic. Universal algebra kind of strangles logic to become what it is generally accepted to be. Cheers, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile +46 70 586 4414 website www8.cs.umu.se/~peklund [For admin and other information see: http://www.mta.ca/~cat-dist/ ]