From aa54adf7701f87213c8cc12b744fe611812bccf0 Mon Sep 17 00:00:00 2001
From: Yuri Sulyma <yuri.sulyma@gmail.com>
Date: Thu, 8 Jun 2017 20:01:41 -0600
Subject: [PATCH] Use psquare/phsquare in spectrum

---
 homotopy/spectrum.hlean | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 7e4fdb2..2c9023e 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -133,7 +133,12 @@ namespace spectrum
 
   structure smap {N : succ_str} (E F : gen_prespectrum N) :=
     (to_fun : Π(n:N), E n →* F n)
-    (glue_square : Π(n:N), glue F n ∘* to_fun n ~* Ω→ (to_fun (S n)) ∘* glue E n)
+    (glue_square : Π(n:N), psquare
+      (to_fun n)
+      (Ω→ (to_fun (S n)))
+      (glue E n)
+      (glue F n)
+    )
 
   open smap
   infix ` →ₛ `:30 := smap
@@ -180,9 +185,12 @@ namespace spectrum
 
   structure shomotopy {N : succ_str} {E F : gen_prespectrum N} (f g : E →ₛ F) :=
     (to_phomotopy : Πn, f n ~* g n)
-    (glue_homotopy : Πn, pwhisker_left (glue F n) (to_phomotopy n) ⬝* glue_square g n
-                         =      -- Ideally this should be a "phomotopy2"
-                         glue_square f n ⬝* pwhisker_right (glue E n) (ap1_phomotopy (to_phomotopy (S n))))
+    (glue_homotopy : Πn, phsquare
+                         (pwhisker_left (glue F n) (to_phomotopy n))
+                         (pwhisker_right (glue E n) (ap1_phomotopy (to_phomotopy (S n))))
+                         (glue_square f n)
+                         (glue_square g n)
+    )
 
   infix ` ~ₛ `:50 := shomotopy