From 9d39f7771f083a1eb93da4512476f0ea4fbc9669 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 5 Jul 2017 15:42:27 +0100
Subject: [PATCH] redefine is_trunc_ppi and is_trunc_spi with unbundled
 families

---
 homotopy/EM.hlean     |  2 +-
 homotopy/strunc.hlean | 30 ++++++++++++-----------------
 pointed_pi.hlean      | 44 ++++++++++++++++++++++---------------------
 3 files changed, 36 insertions(+), 40 deletions(-)

diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 787a720..71fa19d 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -405,7 +405,7 @@ namespace EM
   begin
     cases n with n, { exact _ },
     cases Y with Y H1 H2, cases Y with Y y₀,
-    exact is_trunc_pmap_of_is_conn X n -1 (ptrunctype.mk Y _ y₀),
+    exact is_trunc_pmap_of_is_conn X n -1 _ (pointed.MK Y y₀) !le.refl H2,
   end
 
   open category functor nat_trans
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index f12c54a..db4f67c 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -251,39 +251,33 @@ section
   variables (A : Type*) (n : ℤ) [H : is_conn (maxm2 n) A]
   include H
 
-  definition is_trunc_maxm2_ppi (k : ℤ) (P : A → (maxm2 (n+1+k))-Type*)
-    : is_trunc (maxm2 k) (Π*(a : A), P a) :=
+  definition is_trunc_maxm2_ppi (k l : ℤ) (H3 : l ≤ n+1+k) (P : A → Type*)
+    (H2 : Πa, is_trunc (maxm2 l) (P a)) : is_trunc (maxm2 k) (Π*(a : A), P a) :=
   is_trunc_maxm2_of_maxm1 (Π*(a : A), P a) k
-    (@is_trunc_ppi_of_is_conn A (maxm1m1 n)
-      (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k)
-      (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) (maxm2_le n k)) pt))
+    (@is_trunc_ppi_of_is_conn A (maxm1m1 n) (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k) _
+      (le.trans (maxm2_monotone H3) (maxm2_le n k)) P H2)
 
-  definition is_strunc_spi_of_is_conn (k : ℤ) (P : A → (n+1+k)-spectrum)
-    : is_strunc k (spi A P) :=
+  definition is_strunc_spi_of_is_conn (k l : ℤ) (H3 : l ≤ n+1+k) (P : A → spectrum)
+    (H2 : Πa, is_strunc l (P a)) : is_strunc k (spi A P) :=
   begin
     intro m, unfold spi,
-    exact is_trunc_maxm2_ppi A n (k+m)
-      (λ a, ptrunctype.mk (P a m)
-       (is_trunc_maxm2_change_int (P a m) (add.assoc (n+1) k m)
-         (truncspectrum.struct (P a) m)) pt)
+    exact is_trunc_maxm2_ppi A n (k+m) _ (le.trans (add_le_add_right H3 _)
+            (le_of_eq (add.assoc (n+1) k m))) (λ a, P a m) (λa, H2 a m)
   end
 
 end
 
-definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum)
-  : is_strunc k (spi A P) :=
+definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → spectrum)
+  (H2 : Πa, is_strunc n (P a)) : is_strunc k (spi A P) :=
 begin
   assert K : n ≤ -[1+ 0] + 1 + k,
   { krewrite (int.zero_add k), exact H },
-  { exact @is_strunc_spi_of_is_conn A (-[1+ 0])
-    (is_conn.is_conn_minus_two A) k
-    (λ a, truncspectrum.mk (P a) (is_strunc_of_le (P a) K
-          (truncspectrum.struct (P a)))) }
+  { exact @is_strunc_spi_of_is_conn A (-[1+ 0]) (is_conn.is_conn_minus_two A) k _ K P H2 }
 end
 
 definition is_strunc_spi {A : Type*} (n : ℤ) (P : A → spectrum) (H : Πa, is_strunc n (P a))
   : is_strunc n (spi A P) :=
-is_strunc_spi_of_le n n !le.refl (λa, truncspectrum.mk (P a) (H a))
+is_strunc_spi_of_le n n !le.refl P H
 
 definition is_strunc_sp_cotensor (n : ℤ) (A : Type*) {Y : spectrum} (H : is_strunc n Y)
   : is_strunc n (sp_cotensor A Y) :=
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index ba5ab02..6a35cea 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -494,7 +494,7 @@ namespace is_conn
   variables (A : Type*) (n : ℕ₋₂) [H : is_conn (n.+1) A]
   include H
 
-  definition is_contr_ppi_match (P : A → (n.+1)-Type*)
+  definition is_contr_ppi_match (P : A → Type*) (H : Πa, is_trunc (n.+1) (P a))
     : is_contr (Π*(a : A), P a) :=
   begin
     apply is_contr.mk pt,
@@ -504,44 +504,46 @@ namespace is_conn
     { krewrite (is_conn.elim_β n), apply con.left_inv }
   end
 
-  definition is_trunc_ppi_of_is_conn (k : ℕ₋₂) (P : A → (n.+1+2+k)-Type*)
-    : is_trunc k.+1 (Π*(a : A), P a) :=
+  -- definition is_trunc_ppi_of_is_conn (k : ℕ₋₂) (P : A → Type*)
+  --   : is_trunc k.+1 (Π*(a : A), P a) :=
+
+  definition is_trunc_ppi_of_is_conn (k l : ℕ₋₂) (H2 : l ≤ n.+1+2+k)
+    (P : A → Type*) (H3 : Πa, is_trunc l (P a)) :
+    is_trunc k.+1 (Π*(a : A), P a) :=
   begin
-    induction k with k IH,
+    have H4 : Πa, is_trunc (n.+1+2+k) (P a), from λa, is_trunc_of_le (P a) H2,
+    clear H2 H3, revert P H4,
+    induction k with k IH: intro P H4,
     { apply is_prop_of_imp_is_contr, intro f,
-      apply is_contr_ppi_match },
+      apply is_contr_ppi_match A n P H4 },
     { apply is_trunc_succ_of_is_trunc_loop
         (trunc_index.succ_le_succ (trunc_index.minus_two_le k)),
       intro f,
-      apply @is_trunc_equiv_closed_rev _ _ k.+1
-        (ppi_loop_equiv f),
+      apply @is_trunc_equiv_closed_rev _ _ k.+1 (ppi_loop_equiv f),
       apply IH, intro a,
-      apply ptrunctype.mk (Ω (pType.mk (P a) (f a))),
-      { apply is_trunc_loop, exact is_trunc_ptrunctype (P a) },
-      { exact pt } }
+      apply is_trunc_loop, apply H4 }
   end
 
-  definition is_trunc_pmap_of_is_conn (k : ℕ₋₂) (B : (n.+1+2+k)-Type*)
-    : is_trunc k.+1 (A →* B) :=
+
+  definition is_trunc_pmap_of_is_conn (k l : ℕ₋₂) (B : Type*) (H2 : l ≤ n.+1+2+k)
+    (H3 : is_trunc l B) : is_trunc k.+1 (A →* B) :=
   @is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B)
-    (is_trunc_ppi_of_is_conn A n k (λ a, B))
+    (is_trunc_ppi_of_is_conn A n k l H2 (λ a, B) _)
 
   end
 
   -- this is probably much easier to prove directly
-  definition is_trunc_ppi (A : Type*) (n k : ℕ₋₂) (H : n ≤ k) (P : A → n-Type*)
-    : is_trunc k (Π*(a : A), P a) :=
+  definition is_trunc_ppi (A : Type*) (n k : ℕ₋₂) (H : n ≤ k) (P : A → Type*)
+    (H2 : Πa, is_trunc n (P a)) : is_trunc k (Π*(a : A), P a) :=
   begin
     cases k with k,
-    { apply trunc.is_contr_of_merely_prop,
-      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) -2
-          (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a)
-                  (trunc_index.le.step H)) pt) },
+    { apply is_contr_of_merely_prop,
+      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) -2 _
+                (trunc_index.le.step H) P H2 },
       { exact tr pt } },
     { assert K : n ≤ -1 +2+ k,
       { rewrite (trunc_index.add_plus_two_comm -1 k), exact H },
-      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) k
-          (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) K) pt) } }
+      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) k _ K P H2 } }
   end
 
 end is_conn