feat(hott/homotopy): cleanup cofiber and wedge, redefine smash

hott/homotopy/cofiber.hlean

@@ -5,9 +5,9 @@ Authors: Jakob von Raumer
 
 The Cofiber Type
 -/
-import hit.pointed_pushout function .susp types.unit
+import hit.pushout function .susp types.unit
 
-open eq pushout unit pointed is_trunc is_equiv susp unit
+open eq pushout unit pointed is_trunc is_equiv susp unit equiv
 
 definition cofiber {A B : Type} (f : A → B) := pushout (λ (a : A), ⋆) f
 
@@ -57,6 +57,11 @@ namespace cofiber
     (Pglue : Π (x : A), Pbase = Pcod (f x)) : P :=
   cofiber.elim Pbase Pcod Pglue y
 
+  protected theorem elim_glue {P : Type} (y : cofiber f) (Pbase : P) (Pcod : B → P)
+    (Pglue : Π (x : A), Pbase = Pcod (f x)) (a : A)
+    : ap (elim Pbase Pcod Pglue) (glue a) = Pglue a :=
+  !pushout.elim_glue
+
   end
 end cofiber
 
@@ -79,15 +84,15 @@ namespace cofiber
     { fconstructor, intro x, induction x, exact north, exact south, exact merid x,
       reflexivity },
     { esimp, fapply adjointify,
-      intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a,
+      { intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a },
-      intro s, induction s, do 2 reflexivity, esimp,
+      { intro s, induction s, do 2 reflexivity, esimp,
-      apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square,
+        apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square,
-      refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
+        refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
-      refine ap _ !elim_merid ⬝ _, apply elim_glue,
+        refine ap _ !elim_merid ⬝ _, apply elim_glue },
-      intro c, induction c with [n, s], induction n, reflexivity,
+      { intro c, induction c with s, reflexivity,
-      induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square,
+        induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square,
-      refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
+        refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _,
-      refine ap _ !elim_glue ⬝ _, apply elim_merid },
+        refine ap02 _ !elim_glue ⬝ _, apply elim_merid }},
   end
 
 end cofiber

hott/homotopy/smash.hlean

@@ -1,83 +1,183 @@
 /-
 Copyright (c) 2016 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jakob von Raumer
+Authors: Jakob von Raumer, Floris van Doorn
 
-The Smash Product of Types
+The Smash Product of Types.
+
+One definition is the cofiber of the map
+    wedge A B → A × B
+However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B.
 -/
 
-import hit.pushout .wedge .cofiber .susp .sphere
+import homotopy.circle homotopy.join types.pointed homotopy.cofiber homotopy.wedge
 
-open eq pushout prod pointed is_trunc
+open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge
-
-definition product_of_wedge [constructor] (A B : Type*) : pwedge A B →* A ×* B :=
-begin
-  fconstructor,
-  intro x, induction x with [a, b], exact (a, point B), exact (point A, b),
-  do 2 reflexivity
-end
-
-definition psmash (A B : Type*) := pcofiber (product_of_wedge A B)
-
-open sphere susp unit
 
 namespace smash
 
-  protected definition prec {X Y : Type*} {P : psmash X Y → Type}
+  variables {A B : Type*}
-    (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆))
+
-    (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y)))
+  section
-    (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y))
+  open pushout
-    (pg : pathover (λ x, pathover P ps (glue x) (@prod.rec X Y (λ x, P (inr x)) pxy
+
-          (pushout.elim (λ a, (a, Point Y)) (pair (Point X)) (λ x, idp) x)))
+  definition prod_of_sum [unfold 3] (u : A + B) : A × B :=
-          (px (Point X)) (glue ⋆) (py (Point Y))) : Π s, P s :=
+  by induction u with a b; exact (a, pt); exact (pt, b)
-  begin
+
-    intro s, induction s, induction x, exact ps,
+  definition bool_of_sum [unfold 3] (u : A + B) : bool :=
-    induction x with [x, y], exact pxy x y,
+  by induction u; exact ff; exact tt
-    induction x with [x, y, u], exact px x, exact py y,
+
-    induction u, exact pg,
+  definition smash' (A B : Type*) : Type := pushout (@prod_of_sum A B) (@bool_of_sum A B)
+  protected definition mk (a : A) (b : B) : smash' A B := inl (a, b)
+
+  definition pointed_smash' [instance] [constructor] (A B : Type*) : pointed (smash' A B) :=
+  pointed.mk (smash.mk pt pt)
+  definition smash [constructor] (A B : Type*) : Type* :=
+  pointed.mk' (smash' A B)
+
+  definition auxl : smash A B := inr ff
+  definition auxr : smash A B := inr tt
+  definition gluel (a : A) : smash.mk a pt = auxl :> smash A B := glue (inl a)
+  definition gluer (b : B) : smash.mk pt b = auxr :> smash A B := glue (inr b)
+
   end
 
-  protected definition prec_on {X Y : Type*} {P : psmash X Y → Type} (s : psmash X Y)
+  definition gluel' (a a' : A) : smash.mk a pt = smash.mk a' pt :> smash A B :=
-    (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆))
+  gluel a ⬝ (gluel a')⁻¹
-    (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y)))
+  definition gluer' (b b' : B) : smash.mk pt b = smash.mk pt b' :> smash A B :=
-    (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y))
+  gluer b ⬝ (gluer b')⁻¹
-    (pg : pathover (λ x, pathover P ps (glue x) (@prod.rec X Y (λ x, P (inr x)) pxy
+  definition glue (a : A) (b : B) : smash.mk a pt = smash.mk pt b :=
-          (pushout.elim (λ a, (a, Point Y)) (pair (Point X)) (λ x, idp) x)))
+  gluel' a pt ⬝ gluer' pt b
-          (px (Point X)) (glue ⋆) (py (Point Y))) : P s :=
-  smash.prec pxy ps px py pg s
 
-/-  definition smash_bool (X : Type*) : psmash X pbool ≃* X :=
+  definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b :=
-  begin
+  whisker_right !con.right_inv _ ⬝ !idp_con
-    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,
-        { cases x, apply (glue (inr bool.tt))⁻¹ },
-        { cases x with [x, b], cases b,
-          apply inverse, apply concat, apply (glue (inl x))⁻¹, apply (glue (inr bool.tt)),
-          reflexivity },
-        { esimp, apply eq_pathover, induction x,
-          esimp, apply hinverse, krewrite ap_id, apply move_bot_of_left,
-          krewrite con.right_inv,
-          refine _ ⬝hp !(ap_compose (λ a, inr (pair a _)))⁻¹,
-          apply transpose, apply square_of_eq_bot, rewrite [con_idp, con.left_inv],
-          apply inverse, apply concat, apply ap (ap _),
-           } } }
 
-  definition susp_equiv_circle_smash (X : Type*) : psusp X ≃* psmash (psphere 1) X :=
+  definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt :=
+  proof whisker_left _ !con.right_inv qed
+
+  definition ap_mk_left {a a' : A} (p : a = a') : ap (λa, smash.mk a (Point B)) p = gluel' a a' :=
+  by induction p; exact !con.right_inv⁻¹
+
+  definition ap_mk_right {b b' : B} (p : b = b') : ap (smash.mk (Point A)) p = gluer' b b' :=
+  by induction p; exact !con.right_inv⁻¹
+
+  protected definition rec {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b))
+    (Pl : P auxl) (Pr : P auxr) (Pgl : Πa, Pmk a pt =[gluel a] Pl)
+    (Pgr : Πb, Pmk pt b =[gluer b] Pr) (x : smash' A B) : P x :=
   begin
-    fconstructor,
+    induction x with x b u,
-    { fconstructor, intro x, induction x, },
+    { induction x with a b, exact Pmk a b },
-  end-/
+    { induction b, exact Pl, exact Pr },
+    { induction u: esimp,
+      { apply Pgl },
+      { apply Pgr }}
+  end
+
+  -- a rec which is easier to prove, but with worse computational properties
+  protected definition rec' {P : smash A B → Type} (Pmk : Πa b, P (smash.mk a b))
+    (Pg : Πa b, Pmk a pt =[glue a b] Pmk pt b) (x : smash' A B) : P x :=
+  begin
+    induction x using smash.rec,
+    { apply Pmk },
+    { exact gluel pt ▸ Pmk pt pt },
+    { exact gluer pt ▸ Pmk pt pt },
+    { refine change_path _ (Pg a pt ⬝o !pathover_tr),
+      refine whisker_right !glue_pt_right _ ⬝ _, esimp, refine !con.assoc ⬝ _,
+      apply whisker_left, apply con.left_inv },
+    { refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr),
+      refine whisker_right !glue_pt_left⁻² _ ⬝ _,
+      refine whisker_right !inv_con_inv_right _ ⬝ _, refine !con.assoc ⬝ _,
+      apply whisker_left, apply con.left_inv }
+  end
+
+  theorem rec_gluel {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)}
+    {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl)
+    (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) :
+    apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a :=
+  !pushout.rec_glue
+
+  theorem rec_gluer {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)}
+    {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl)
+    (Pgr : Πb, Pmk pt b =[gluer b] Pr) (b : B) :
+    apd (smash.rec Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b :=
+  !pushout.rec_glue
+
+  theorem rec_glue {P : smash A B → Type} {Pmk : Πa b, P (smash.mk a b)}
+    {Pl : P auxl} {Pr : P auxr} (Pgl : Πa, Pmk a pt =[gluel a] Pl)
+    (Pgr : Πb, Pmk pt b =[gluer b] Pr) (a : A) (b : B) :
+    apd (smash.rec Pmk Pl Pr Pgl Pgr) (glue a b) =
+      (Pgl a ⬝o (Pgl pt)⁻¹ᵒ) ⬝o (Pgr pt ⬝o (Pgr b)⁻¹ᵒ) :=
+  by rewrite [↑glue, ↑gluel', ↑gluer', +apd_con, +apd_inv, +rec_gluel, +rec_gluer]
+
+  protected definition elim {P : Type} (Pmk : Πa b, P) (Pl Pr : P)
+    (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (x : smash' A B) : P :=
+  smash.rec Pmk Pl Pr (λa, pathover_of_eq _ (Pgl a)) (λb, pathover_of_eq _ (Pgr b)) x
+
+  -- an elim which is easier to prove, but with worse computational properties
+  protected definition elim' {P : Type} (Pmk : Πa b, P) (Pg : Πa b, Pmk a pt = Pmk pt b)
+    (x : smash' A B) : P :=
+  smash.rec' Pmk (λa b, pathover_of_eq _ (Pg a b)) x
+
+  theorem elim_gluel {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
+    (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) :
+    ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a :=
+  begin
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluel A B a)),
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluel],
+  end
+
+  theorem elim_gluer {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
+    (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) :
+    ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b :=
+  begin
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluer A B b)),
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluer],
+  end
+
+  theorem elim_glue {P : Type} {Pmk : Πa b, P} {Pl Pr : P}
+    (Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) (b : B) :
+    ap (smash.elim Pmk Pl Pr Pgl Pgr) (glue a b) = (Pgl a ⬝ (Pgl pt)⁻¹) ⬝ (Pgr pt ⬝ (Pgr b)⁻¹) :=
+  by rewrite [↑glue, ↑gluel', ↑gluer', +ap_con, +ap_inv, +elim_gluel, +elim_gluer]
+
+end smash
+open smash
+attribute smash.mk auxl auxr [constructor]
+attribute smash.rec smash.elim [unfold 9] [recursor 9]
+attribute smash.rec' smash.elim' [unfold 6]
+
+namespace smash
+
+  variables {A B : Type*}
+
+  definition of_smash_pbool [unfold 2] (x : smash A pbool) : A :=
+  begin
+    induction x,
+    { induction b, exact pt, exact a },
+    { exact pt },
+    { exact pt },
+    { reflexivity },
+    { induction b: reflexivity }
+  end
+
+  definition smash_pbool_equiv [constructor] (A : Type*) : smash A pbool ≃* A :=
+  begin
+    fapply pequiv_of_equiv,
+    { fapply equiv.MK,
+      { exact of_smash_pbool },
+      { intro a, exact smash.mk a tt },
+      { intro a, reflexivity },
+      { exact abstract begin intro x, induction x using smash.rec',
+        { induction b, exact (glue a tt)⁻¹, reflexivity },
+        { apply eq_pathover_id_right, induction b: esimp,
+          { refine ap02 _ !glue_pt_right ⬝ph _,
+            refine ap_compose (λx, smash.mk x _) _ _ ⬝ph _,
+            refine ap02 _ (!ap_con ⬝ (!elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻²))) ⬝ph _,
+            apply hinverse, apply square_of_eq,
+            esimp, refine (!glue_pt_right ◾ !glue_pt_left)⁻¹ },
+          { apply square_of_eq, refine !con.left_inv ⬝ _, esimp, symmetry,
+            refine ap_compose (λx, smash.mk x _) _ _ ⬝ _,
+            exact ap02 _ !elim_glue }} end end }},
+    { reflexivity }
+  end
 
 end smash

hott/homotopy/wedge.hlean

@@ -5,11 +5,28 @@ Authors: Jakob von Raumer, Ulrik Buchholtz
 
 The Wedge Sum of Two Pointed Types
 -/
-import hit.pointed_pushout .connectedness types.unit
+import hit.pushout .connectedness types.unit
 
 open eq pushout pointed unit trunc_index
 
-definition pwedge (A B : Type*) : Type* := ppushout (pconst punit A) (pconst punit B)
+definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B)
+local attribute wedge [reducible]
+definition pwedge (A B : Type*) : Type* := pointed.mk' (wedge A B)
+
+namespace wedge
+
+  protected definition rec {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x))
+    (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) (glue ⋆) (Pinr pt))
+    (y : wedge A B) : P y :=
+  by induction y; apply Pinl; apply Pinr; induction x; exact Pglue
+
+  protected definition elim {A B : Type*} {P : Type} (Pinl : A → P)
+    (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge A B) : P :=
+  by induction y with a b x; exact Pinl a; exact Pinr b; induction x; exact Pglue
+
+end wedge
+
+attribute wedge.rec wedge.elim [recursor 7] [unfold 7]
 
 namespace wedge