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

[Gregory Malecha]

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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140210/e35f3d05/attachment.htm