[HoTT-reading-group] Chapters 5 & 6

[Jason Gross]

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.

Coq solutions for the assigned exercises in chapter 5 are
here<http://hott.github.io/HoTT/proviola-html/HoTTBookExercises.html#Book_5_2.ez>
.

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 partial
implementation of such a Coq <https://github.com/barras/coq/tree/hit>.
 Here is some example code:

Inductive interval :=
| zero : interval
| one : interval
with paths :=
| seg : zero = one.

Definition ap A B (f : A -> B) x y (p : x = y) : f x = f y
  := match p in (_ = y) return f x = f y with
       | eq_refl => eq_refl
     end.

Definition transport_const A B x y z p
: eq_rect x (fun _ : A => B) y z p
  = y.
Proof.
  destruct p.
  reflexivity.
Defined.

Definition funext A (B : A -> Type) (f g : forall a, B a) (H : forall x, f
x = g x)
: f = g
  := @ap _ _
         (fun (i : interval) x =>
            fixmatch {h} i with
              | zero => f x
              | one => g x
              | seg => eq_trans (transport_const _ _ _ _ _ _) (H x)
            end)
         _ _
         seg.


See you next week!

-Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140303/132e4739/attachment.htm