<div dir="ltr">I'm not sure what you mean by "<span style="font-family:arial,sans-serif;font-size:13px">The interesting question, is why is it provable?"</span><div><span style="font-family:arial,sans-serif;font-size:13px"><br>
</span></div><div><font face="arial, sans-serif">Univalence can't be proven within Coq because Coq is compatible with proof-irrelevance for equality, which contradicts univalence (on, e.g., the type bool = bool).</font></div>
<div><font face="arial, sans-serif"><br></font></div><div><font face="arial, sans-serif">A formulation of computational univalence in Coq is a collection of reduction rules for pattern matching on univalence, possibly together with a proof that the reduction algorithm is terminating, confluent, and strongly normalizing up to propositional equality. For example, one reduction rule is</font></div>
<div><div>∀ (X Y : Type) (e : X ≃ Y) (B : Type → Type) (f : X → B X)</div><div> match ua e in (_ = T) return (T → B T) with</div><div> | eq_refl ⇒ f</div><div> end</div><div> ≡</div><div> λ (x : Y) ⇒</div><div> match ua e in (_ = T) return B T with</div>
<div> | eq_refl ⇒ f (e⁻¹ x)</div><div> end</div></div><div><br></div><div>I'm pretty sure that most reduction rules for univalence that don't require returning an arbitrary inductive type can be proven in Coq. (For example, this can can be proven, I believe, using the fact that e⁻¹ = ua⁻¹ (eq_sym (ua e)), and then [case (ua e); reflexivity.].) And even the ones that require returning an arbitrary inductive type might be made to work with typeclasses for w-types (a project I might try to play with when I have time).</div>
<div><br></div><div>-Jason </div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 10, 2014 at 9:46 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">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.</div>
<div class="HOEnZb"><div class="h5">
<div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 10, 2014 at 9:11 PM, Jason Gross <span dir="ltr"><<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</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">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"><div><div>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>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><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><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></div></div>_______________________________________________<br>
HoTT-reading-group mailing list<br>
<a href="mailto:HoTT-reading-group@mit.edu" target="_blank">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>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><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></div></blockquote></div><br></div>