Re: [HoTT] Conjecture

[Martin Escardo <escardo...@googlemail.com>]

On 07/04/17 18:11, Michael Shulman wrote:
> On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type
> Theory <HomotopyT...@googlegroups.com> wrote:
>> (1) Indeed, I do like to think of the fragment of univalent type
>> theory consisting of function extensionality + proposition
>> extensionality + propositional truncation as essentially the same
>> thing as topos logic, provided we have propositional resizing. (But,
>> as discussed, much can be done without propositional resizing (but not
>> all), and one way of looking at HIT's is as a mechanism to avoid
>> resizing.)
> 
> I would say that to really be talking about (elementary) topos logic,
> one should also do without universes other than hProp.  Of course,
> elementary 1-toposes also validate UIP.

Agreed. (But you can consider elementary toposes with a universe object,
and a number of people have worked on that independently of any
connection with dependent type theory.)

> If we also omit hProp and propositional resizing, but include
> nonrecursive HITs as well as ordinary inductive types, then it ought
> to be basically Pi-W-pretopos logic; right?

I'd let the experts on these details to answer this.

I noticed the following mistake immediately after I send my message this
morning, and this is a good opportunity to rectify it:

>> In topos logic, you define (for the dominance of all propositions)
>>
>>   Lift(X) = { A:X->Omega | (exists(x:X), A x) &
>>                            forall(x,y:X), A x -> A y -> x = y }
>>

  Lift(X) = { A:X->Omega | forall(x,y:X), A x -> A y -> x = y }

If anybody noticed, they probably knew I meant that, and, if they didn't
notice, they probably understood that. There are other possibilities, of
course. :-)

Martin