<div dir="ltr">Hi,<div>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.</div>
<div><br></div><div>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. ;-)</div>
<div><br></div><div>-Jason</div><div><br></div><div>Here is the code we wrote, which depends on <a href="https://github.com/HoTT/HoTT/pull/337">https://github.com/HoTT/HoTT/pull/337</a>.</div><div><br></div><div>Require Import HoTT hit.Circle hit.Suspension hit.TwoSphere.</div>
<div><br></div><div>Set Implicit Arguments.</div><div><br></div><div>Local Open Scope equiv_scope.</div><div><br></div><div>Definition f : Susp S1 -> S2.</div><div>Proof.</div><div> refine (Susp_rect_nd</div><div> base</div>
<div> base</div><div> _).</div><div> intro x.</div><div> refine (S1_rectnd</div><div> _</div><div> idpath</div><div> surf</div><div> x).</div><div>Defined.</div>
<div><br></div><div>Notation refl x := (idpath x).</div><div><br></div><div>Definition g : S2 -> Susp S1.</div><div>Proof.</div><div> refine (S2_rectnd</div><div> _</div><div> North</div><div> _).</div>
<div> exact ((concat_pV _)^</div><div> @ concat2 (ap merid loop) (idpath (merid Circle.base)^)</div><div> @ concat_pV _).</div><div>Defined.</div><div><br></div><div>Lemma Book_6_2 : Susp S1 <~> S2.</div>
<div>Proof.</div><div> refine (equiv_adjointify</div><div> f g</div><div> _ _);</div><div> hnf;</div><div> unfold f, g; simpl.</div><div> refine (S2_rect</div><div> (fun x => f (g x) = x)</div>
<div> idpath</div><div> _);</div><div> unfold f, g; simpl.</div><div> Focus 2.</div><div> refine (Susp_rect</div><div> (fun x => g (f x) = x)</div><div> idpath</div><div>
(merid Circle.base)</div><div> _);</div><div> unfold f, g; simpl.</div><div> intro. </div></div>