<div dir="ltr">If anyone else cares one way or the other about seeing this discussion, feel free to email either the list or us personally, and we'll make sure to take it offline/continue on the list according to preference. Otherwise, I'll default to including the list for now, in case people are interested.<div>
<br></div><div><div>I think all of the program equivalence rules that I cook up for univalence and HITs can be directionalized in a way that permits a homotopy-canonical form (i.e., a normal form up to propositional equality), which is why I call them reduction rules; you should always be able to push instances of univalence inwards (in the sense that if you have a lambda transported across ua, you should be able to turn it into an untransported lambda, where the body/argument are transported; or if you have an application of a constructor transported across ua, you should be able to make it an untransported constructor applied to transported arguments; etc). I unfortunately don't know how to make this precise in a way that allows proving termination of the extended reduction algorithm, nor do I have a complete set of rules (yet).<br>
</div></div><div><br></div><div><br></div><div>I have only a very fuzzy notion of compilation (because I tend to think in Coq, rather than in assembly), but my intuition is that your [match foobar ...] would be compiled down to a program that compiled [f], and then transformed it using the compiled version of [foobar]. Similarly, if you want to compile</div>
<div><br></div><div>match b as b' return T b with</div><div> | true ⇒ x</div><div> | false ⇒ y</div><div>end </div><div><br></div><div>then you would compile x and y, and then decide which to run/return based on the compiled value of [b]. The main difference in the univalence case is that [foobar] might never compile down to a constructor, and the reduction is more complicated than simply picking a branch. So I'd imagine that the general feature here would be that you're allowed to introduce axioms with (appropriately consistent) computation rules, so the compilation of univalence would come with all of the reduction/program transformation rules that are needed to run it. </div>
<div><br></div><div>-Jason</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 11, 2014 at 10:56 AM, 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">Hi, Jason --<div><br></div><div>I'm not sure if this conversation has become too specialized for the list in general, so it might be worthwhile taking it offline. It may only be of interest to the more computer-sciency people.</div>
<div><br></div><div>What you say seems strange to me from a computational perspective. From a logical perspective, this works nicely, but when I think about computation, I usually think about running a program and it isn't clear what this reduction rule would translate to in assembly language. For me, and perhaps I am wrong, the key notion of computation is a compositional semantics. I..e. I should be able to look at various pieces of the programming language and compile them independently. This is essential to support lambda abstraction, i.e. if I have a program:</div>
<div><br></div><div><div><font face="courier new, monospace">match foobar in (_ = T) return (T → B T) with</font></div><div><font face="courier new, monospace"> | eq_refl ⇒ f</font></div><div><font face="courier new, monospace">end</font></div>
</div><div><br></div><div>(the same as your program except [ua e] is replaced with [foobar]) then I would need to know how to compile it without knowing what foobar is. [foobar] may come from an external library, be a parameter to my function, etc.</div>
<div><br></div><div>The rule that you give above is a program equivalence, and is likely provable, but I don't think of something like it as a reduction rule.</div><div><br></div><div>Perhaps that is me showing my narrow-minded computer science perspective.</div>
</div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Feb 10, 2014 at 11:04 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">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>
<span><font color="#888888">
<div><br></div><div>-Jason </div></font></span></div><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><div>
<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>
</div></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>