Dear Steve, thank you for your answer! Indeed, I was seeking for feedback in this style. Like you said, with the restrictions you adopt you are on a safe side, but those exclude function spaces, which are allowed in Martin-L?f TT, and the latter is commonly called predicative. I realize though that you have additional motivation for geometric logic (as a logic of observable properties, at least this is my current intuition, which I also picked up from your book) and that happens to be predicative. The reason I believe that one can potentially make sense of predicativity in categories is because I learned recently from the paper "Modular correspondence between dependent type theories and categories including pretopoi and topoi" by Maria Maietti that various classes of categories are uniformly described by their internal language written is the style of extensional dependent type theory. By incrementally extending the language one obtains narrower and narrower classes of categories ending up at toposes. Hence, I thought that there might be a way to formally classify such extensions as predicative or impredicative. Best regards, Sergey On 30/11/16 12:01, Steve Vickers wrote:
Dear Sergey,
For myself, I'm not exactly sure I understand the original notion of predicativity, but I have a rule of thumb that seems to work and satisfy predicative mathematicians. I've frequently claimed that parts of my work are predicative, and no one has complained so far.
In topos theory, as you point out, the subobject classifier and powersets indicate impredicativity.
My rule of thumb is that "geometric" reasoning, preserved (up to isomorphism) by the inverse image parts of geometric morphisms, is safely within the predicative fragment. (Note that even exponentials, function sets, are not geometric, so geometric reasoning is quite restricted.)
The subobject classifier and powersets are not geometric.
On the other hand, the free semilattices, along with free algebras (for cartesian theories) in general, are geometric, and they classify Kuratowski finite subobjects. My rule of thumb predicts that Kuratowski finite powersets are predicative, and there seems to be general agreement with that.
My current work on arithmetic universes seeks a setting for pure geometric reasoning, without the non-geometric parts that exist in toposes, and independent of base topos so long as it has an nno.
Best wishes,
Steve Vickers.
On 27 Nov 2016, at 18:53, Sergey Goncharov <sergey.goncharov@fau.de> wrote:
Dear Community,
I am recently racking my brains in trying to understand what (im-)predicativity means from a categorical perspective, but failing short, hence calling for you help.
...
Looking forward to your answers.
Sergey
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]