From d6de922d1f0720ee7d2798177c5af537a67f14b0 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 25 Jan 2017 12:14:47 -0500
Subject: [PATCH] give last step of associativity of smash

there are still unproven lemma's
---
 homotopy/smash_adjoint.hlean | 31 ++++++++++++++++++++++++-------
 1 file changed, 24 insertions(+), 7 deletions(-)

diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index a0e45d9..9ede3d1 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -1,5 +1,5 @@
 -- Authors: Floris van Doorn
--- in collaboration with Egbert, Stefano, Robin
+-- in collaboration with Egbert, Stefano, Robin, Ulrik
 
 
 import .smash
@@ -479,6 +479,12 @@ namespace smash
     refine !smash_adjoint_pmap_natural_pt
   end
 
+  definition smash_assoc_elim_inv_natural_pt {A B C X X' : Type*} (f : X →* X') (g : (A ∧ B) ∧ C →* X) :
+    f ∘* (smash_assoc_elim_equiv A B C X)⁻¹ᵉ* g ~* (smash_assoc_elim_equiv A B C X')⁻¹ᵉ* (f ∘* g) :=
+  begin
+    exact sorry
+  end
+
   definition smash_assoc_elim_natural {A B C X X' : Type*} (f : X →* X') :
     ppcompose_left f ∘* smash_assoc_elim_equiv A B C X ~*
     smash_assoc_elim_equiv A B C X' ∘* ppcompose_left f :=
@@ -495,14 +501,25 @@ namespace smash
     -- refine !smash_adjoint_pmap_natural_pt
   end
 
-  -- definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
+  -- definition smash_assoc_to (A B C : Type*) : A ∧ (B ∧ C) →* (A ∧ B) ∧ C :=
   -- begin
-  --   fapply pequiv.MK,
-  --   { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid },
-  --   { exact !smash_assoc_elim_equiv !pid },
-  --   { },
-  --   { }
+
   -- end
 
 
+  -- TODO: remove pap
+  definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
+  begin
+    fapply pequiv.MK2,
+    { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid },
+    { exact !smash_assoc_elim_equiv !pid },
+    { refine !smash_assoc_elim_inv_natural_pt ⬝* _,
+      refine pap !smash_assoc_elim_equiv⁻¹ᵉ* !pcompose_pid ⬝* _,
+      apply phomotopy_of_eq, apply to_left_inv !smash_assoc_elim_equiv },
+    { refine !smash_assoc_elim_natural_pt ⬝* _,
+      refine pap !smash_assoc_elim_equiv !pcompose_pid ⬝* _,
+      apply phomotopy_of_eq, apply to_right_inv !smash_assoc_elim_equiv }
+  end
+
+
 end smash