[HoTT-reading-group] Isomorphism's & Equality

[Gregory Malecha]

That's what I figured. The interesting question, is why is it provable? And
given this, it seems that univalence can not be proven within Coq (in
retrospect this makes sense) though now it is less clear to me what a
computational formulation of it will be.


On Mon, Feb 10, 2014 at 9:11 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> With the univalence axiom, your goal is very easy; if you have (H : A ≃ B)
> and ua is the univalence axiom, then you have (ap P (ua H) : P A = P B)
> (and (X = Y -> X -> Y) is an easy path induction).
>
> Without univalence, it's unprovable in general.  Consider A ≡ unit,
> B ≡ unit * unit, and P x ≡ (unit = x).  Then we have unit ≃ unit * unit,
> and we have P unit (by refl), but we don't have P (unit * unit) (which is
> unit = unit * unit), unless we have univalence/propositional extensionality.
>
> However, you can prove it for almost any appropriately concrete type
> family not involving equality (or anything else where the only way to
> construct it is when things are judgmentally equal).  The benefit of having
> computational univalence is that you don't have to do so manually.
>
> -Jason
>
>
> On Mon, Feb 10, 2014 at 8:17 PM, Gregory Malecha <gmalecha at cs.harvard.edu>wrote:
>
>> Hello --
>>
>> I was thinking a little bit more about the proof today, and I'm wondering
>> if the following statement is provable:
>>
>> Goal forall (A B : Type), A \equiv B -> forall (P : Type -> Prop), P A ->
>> P B.
>>
>> (here \equiv is meant to be HoTT equivalence of types)
>>
>> In particular, this gets at the idea that you can not write a proposition
>> that distinguishes two equivalent types, i.e. Type is a setoid and no
>> function in the language can distinguish equivalent values in the setoid.
>>
>> You can also make this stronger using [transport] (or whatever it is
>> called in HoTT):
>>
>> Goal forall (A B : Type) (pf : \equiv A B)
>>             (E : Type -> Type)
>>             (P : forall x, E x -> Prop),
>>        forall a : E A, P A a ->
>>                        P B (@transport A B pf E a).
>>
>> The idea here is you can get arbitrary amounts of other data associated
>> with the type (e.g. eliminators) and everything will still work. Neither of
>> these is provable in vanilla Coq, though you can prove both by giving
>> richer types for [P] that guarantee that they respect equivalence.
>>
>> --
>> gregory malecha
>> http://www.people.fas.harvard.edu/~gmalecha/
>>
>> _______________________________________________
>> HoTT-reading-group mailing list
>> HoTT-reading-group at mit.edu
>> http://mailman.mit.edu/mailman/listinfo/hott-reading-group
>>
>>
>


-- 
gregory malecha
http://www.people.fas.harvard.edu/~gmalecha/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140210/15b60314/attachment.htm