feat(hott): start lemma about smashing with bool

hott/homotopy/cofiber.hlean

@@ -38,6 +38,13 @@ namespace cofiber
     intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
   end
 
+  protected definition rec_on {A : Type} {B : Type} {f : A → B} {P : cofiber f → Type}
+    (y : cofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
+    (Pglue : Π (x : A), pathover P Pinl (glue x) (Pinr (f x))) : P y :=
+   begin
+     induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
+   end
+
   end
 end cofiber
 
@@ -47,13 +54,25 @@ definition Cofiber {A B : Type*} (f : A →* B) : Type* := Pushout (pconst A Uni
 
 namespace cofiber
 
-  protected definition prec {A : Type*} {B : Type*}
-    {f : A →* B} {P : Cofiber f → Type}
+  protected definition prec {A B : Type*} {f : A →* B} {P : Cofiber f → Type}
     (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
     (Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) :
     (Π (y : Cofiber f), P y) :=
   begin
-    intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x,
+    intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
+  end
+
+  protected definition prec_on {A B : Type*} {f : A →* B} {P : Cofiber f → Type}
+    (y : Cofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x))
+    (Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) : P y :=
+  begin
+    induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x
+  end
+
+  protected definition pelim_on {A B C : Type*} {f : A →* B} (y : Cofiber f) 
+    (c : C) (g : B → C) (p : Π x, c = g (f x)) : C :=
+  begin
+    fapply pushout.elim_on y, exact (λ x, c), exact g, exact p
   end
 
   --TODO more pointed recursors

hott/homotopy/smash.hlean

@@ -10,7 +10,7 @@ import hit.pushout .wedge .cofiber .susp .sphere
 
 open eq pushout prod pointed Pointed
 
-definition product_of_wedge (A B : Type*) : Wedge A B →* A ×* B :=
+definition product_of_wedge [constructor] (A B : Type*) : Wedge A B →* A ×* B :=
 begin
   fconstructor,
   intro x, induction x with [a, b], exact (a, point B), exact (point A, b), 
@@ -19,11 +19,43 @@ end
 
 definition Smash (A B : Type*) := Cofiber (product_of_wedge A B)
 
-open sphere susp
+open sphere susp unit
 
 namespace smash
 
+  definition smash_bool (X : Type*) : Smash X Bool ≃* X :=
+  begin
+    fconstructor,
+    { fconstructor,
+      { intro x, fapply cofiber.pelim_on x, clear x, exact point X, intro p,
+        cases p with [x', b], cases b with [x, x'], exact point X, exact x',
+        clear x, intro w, induction w with [y, b], reflexivity, 
+        cases b, reflexivity, reflexivity, esimp,
+        apply eq_pathover, refine !ap_constant ⬝ph _, cases x, esimp, apply hdeg_square,
+        apply inverse, apply concat, apply ap_compose (λ a, prod.cases_on a _),
+        apply concat, apply ap _ !elim_glue, reflexivity },
+      reflexivity },
+    { fapply is_equiv.adjointify,
+      { intro x, apply inr, exact pair x bool.tt },
+      { intro x, reflexivity },
+      { intro s, esimp, induction s, } }
+  end
+
+  check ap_compose
+
+
+  check bool.rec
+
+exit
+fconstructor, intro x, induction x, exact point X,
+      induction a, exact point X, esimp, induction x, do 2 reflexivity, 
+      apply eq_pathover, apply hdeg_square, induction x, -/
+
+
   definition susp_equiv_circle_smash (X : Type*) : Susp X ≃* Smash (Sphere 1) X :=
-  sorry  
+  begin
+    fconstructor,
+    { fconstructor, intro x, induction x, },
+  end
 
 end smash