<div dir="ltr">Hello --<div><br></div><div>I was thinking a little bit more about the proof today, and I'm wondering if the following statement is provable:</div><div><br></div><div><font face="courier new, monospace">Goal forall (A B : Type), A \equiv B -> forall (P : Type -> Prop), P A -> P B.</font><br clear="all">
<div><br></div><div>(here \equiv is meant to be HoTT equivalence of types)</div><div><br></div><div>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.<br>
</div><div><br></div><div>You can also make this stronger using [transport] (or whatever it is called in HoTT):</div><div><br></div><div><div><font face="courier new, monospace">Goal forall (A B : Type) (pf : \equiv A B)</font></div>
<div><font face="courier new, monospace"> (E : Type -> Type)</font></div><div><font face="courier new, monospace"> (P : forall x, E x -> Prop),</font></div><div><font face="courier new, monospace"> forall a : E A, P A a -></font></div>
<div><font face="courier new, monospace"> P B (@transport A B pf E a).</font></div></div><div><br></div><div>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.</div>
<div><br></div><div>-- <br></div><div dir="ltr">gregory malecha<br><div><a href="http://www.people.fas.harvard.edu/~gmalecha/" target="_blank">http://www.people.fas.harvard.edu/~gmalecha/</a></div></div>
</div></div>