<div dir="ltr">Today, we talked a bit about how to compile univalence, why [nat] defined as a W-type has the wrong judgmental rules (and what it would take to give it the "right" rules), and we went over exercises 5.2 and 5.3. We also talked about the positivity condition.<div>
<br></div><div>Coq solutions for the assigned exercises in chapter 5 are <a href="http://hott.github.io/HoTT/proviola-html/HoTTBookExercises.html#Book_5_2.ez">here</a>.<br><div><br></div><div>For next week, please read chapter 6, and do Exercises 6.2, 6.5, and 6.9. If you want to play with a version of Coq with native support for pattern matching on higher inductive types, Bruno Barras has a <a href="https://github.com/barras/coq/tree/hit">partial implementation of such a Coq</a>. Here is some example code:</div>
</div><div><br></div><div><div>Inductive interval :=</div><div>| zero : interval</div><div>| one : interval</div><div>with paths :=</div><div>| seg : zero = one.</div><div><br></div><div>Definition ap A B (f : A -> B) x y (p : x = y) : f x = f y</div>
<div> := match p in (_ = y) return f x = f y with</div><div> | eq_refl => eq_refl</div><div> end.</div><div><br></div><div>Definition transport_const A B x y z p</div><div>: eq_rect x (fun _ : A => B) y z p</div>
<div> = y.</div><div>Proof.</div><div> destruct p.</div><div> reflexivity.</div><div>Defined.</div><div><br></div><div>Definition funext A (B : A -> Type) (f g : forall a, B a) (H : forall x, f x = g x)</div><div>: f = g</div>
<div> := @ap _ _</div><div> (fun (i : interval) x =></div><div> fixmatch {h} i with</div><div> | zero => f x</div><div> | one => g x</div><div> | seg => eq_trans (transport_const _ _ _ _ _ _) (H x)</div>
<div> end)</div><div> _ _</div><div> seg.</div></div><div><br></div><div><br></div><div>See you next week!</div><div><br></div><div>-Jason</div></div>