<div dir="ltr">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).<div>
<br></div><div>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.</div>
<div><br></div><div>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.</div>
<div><br></div><div>-Jason</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 10, 2014 at 8:17 PM, Gregory Malecha <span dir="ltr"><<a href="mailto:gmalecha@cs.harvard.edu" target="_blank">gmalecha@cs.harvard.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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>
<span class="HOEnZb"><font color="#888888">
<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>
</font></span></div></div>
<br>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu">HoTT-reading-group@mit.edu</a><br>
<a href="http://mailman.mit.edu/mailman/listinfo/hott-reading-group" target="_blank">http://mailman.mit.edu/mailman/listinfo/hott-reading-group</a><br>
<br></blockquote></div><br></div>