[HoTT-reading-group] Week of 3/17, Week of 3/31

[Jason Gross]

Hi,
This past Monday, we talked about higher inductive types.  We spent most of
the time working on exercise 6.2, and trying to construct the map S² → ΣS¹.
 I've included the Coq code we came up with at the bottom of this email.

There will be no meeting this Monday; I'm away for spring break.  For next
Monday, 3/31, please read chapter 7, about homotopy n-types.  Please
attempt exercises 7.1, 7.2, and 7.12.  7.8 is also interesting, and if you
solve 7.8 (ii), please be prepared to share your solution with us. ;-)

-Jason

Here is the code we wrote, which depends on
https://github.com/HoTT/HoTT/pull/337.

Require Import HoTT hit.Circle hit.Suspension hit.TwoSphere.

Set Implicit Arguments.

Local Open Scope equiv_scope.

Definition f : Susp S1 -> S2.
Proof.
  refine (Susp_rect_nd
            base
            base
            _).
  intro x.
  refine (S1_rectnd
            _
            idpath
            surf
            x).
Defined.

Notation refl x := (idpath x).

Definition g : S2 -> Susp S1.
Proof.
  refine (S2_rectnd
            _
            North
            _).
  exact ((concat_pV _)^
         @ concat2 (ap merid loop) (idpath (merid Circle.base)^)
           @ concat_pV _).
Defined.

Lemma Book_6_2 : Susp S1 <~> S2.
Proof.
  refine (equiv_adjointify
            f g
            _ _);
  hnf;
  unfold f, g; simpl.
  refine (S2_rect
            (fun x => f (g x) = x)
            idpath
            _);
    unfold f, g; simpl.
  Focus 2.
  refine (Susp_rect
            (fun x => g (f x) = x)
            idpath
            (merid Circle.base)
            _);
    unfold f, g; simpl.
  intro.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140322/32653da2/attachment.htm