Re: [HoTT] A puzzle about "univalent equality"

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

On 08/09/16 07:45, Michael Shulman wrote:
> Type theory does have set-theoretic models, of course.  But that
> doesn't provide a notion of equality that makes sense *inside* MLTT,
> compelling or otherwise.


Exactly: elementwise equality can't even be formulated internally.

However, there is one situation in which elementwise equality can both
be formulated and is the equality we get.

For a type X define its powerset to be

  PX := X->Prop.

For A:PX write x \in A (like in topos type theory) to mean A(x).

Then (A=B) = (forall x:X, x \in A <-> x \in B).

In topos type theory we get this because both function extensionality
and propositional extensionality hold.

In HoTT we get this because these two extensionality properties are a
particular case of univalence.

In MLTT with equality reflection, you don't get this, because although
you get function extensionality, you don't get propositional
extensionality. So equality reflection is not doing the job of capturing
elementwise equality in the powerset. But univalence is.

Martin

> 
> On Wed, Sep 7, 2016 at 11:34 PM, Matt Oliveri <atm...@gmail.com> wrote:
>> True, the language does not provide this structure. But that doesn't mean it
>> isn't in the model. Is there a problem interpreting ITT as all Zermelo-style
>> sets, with identity as a subsingletons for equality?
>>
>> On Thursday, September 8, 2016 at 12:15:13 AM UTC-4, Michael Shulman wrote:
>>>
>>> Does "Zermelo-style set-theoretic equality" even make sense in MLTT?
>>> Types don't have the global membership structure that Zermelo-sets do.
>>>
>>> On Wed, Sep 7, 2016 at 4:18 PM, Matt Oliveri <atm...@gmail.com> wrote:
>>>> On Tuesday, September 6, 2016 at 6:14:24 PM UTC-4, Martin Hotzel Escardo
>>>> wrote:
>>>>>
>>>>> Some people like the K-axiom for U because ... (let them fill the
>>>>> answer).
>>>>
>>>>
>>>> It allows you to interpret (within type theory) the types of ITT + K as
>>>> types of U, and their elements as the corresponding elements.
>>>> (Conjecture?)
>>>> Whereas without K, we don't know how to interpret ITT types as types of
>>>> U.
>>>> In other words, K is a simple way to give ITT reflection.
>>>>
>>>>> Can we stare at the type (Id U X Y) objectively, mathematically, say
>>>>> within intensional MLTT, where it was introduced, and, internally in
>>>>> MLTT, ponder what it can be, and identify the only "compelling" thing
>>>>> it
>>>>> can be as the type of equivalences X~Y, where "compelling" is a notion
>>>>> remote from univalence?
>>>>
>>>>
>>>> How does Zermelo-style set-theoretic equality get ruled out as a
>>>> potential
>>>> "compelling" meaning for identity? Of course, there's a potential
>>>> argument
>>>> about what "compelling" ought to be getting at. You seem to not consider
>>>> set-theoretic equality compelling, which I can play along with.
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>