Re: Predicativity in Categories

[Sergey Goncharov <sergey.goncharov@fau.de>]

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/ ]