redefine is_trunc_ppi and is_trunc_spi with unbundled families

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

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*)
+  definition is_trunc_maxm2_ppi (k l : ℤ) (H3 : l ≤ n+1+k) (P : A → Type*)
-    : is_trunc (maxm2 k) (Π*(a : A), P a) :=
+    (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_trunc_ppi_of_is_conn A (maxm1m1 n) (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k) _
-      (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k)
+      (le.trans (maxm2_monotone H3) (maxm2_le n k)) P H2)
-      (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) (maxm2_le n k)) pt))
 
-  definition is_strunc_spi_of_is_conn (k : ℤ) (P : A → (n+1+k)-spectrum)
+  definition is_strunc_spi_of_is_conn (k l : ℤ) (H3 : l ≤ n+1+k) (P : A → spectrum)
-    : is_strunc k (spi A P) :=
+    (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)
+    exact is_trunc_maxm2_ppi A n (k+m) _ (le.trans (add_le_add_right H3 _)
-      (λ a, ptrunctype.mk (P a m)
+            (le_of_eq (add.assoc (n+1) k m))) (λ a, P a m) (λa, H2 a m)
-       (is_trunc_maxm2_change_int (P a m) (add.assoc (n+1) k m)
-         (truncspectrum.struct (P a) m)) pt)
   end
 
 end
 
-definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum)
+definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → spectrum)
-  : is_strunc k (spi A P) :=
+  (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])
+  { exact @is_strunc_spi_of_is_conn A (-[1+ 0]) (is_conn.is_conn_minus_two A) k _ K P H2 }
-    (is_conn.is_conn_minus_two A) k
-    (λ a, truncspectrum.mk (P a) (is_strunc_of_le (P a) K
-          (truncspectrum.struct (P a)))) }
 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) :=

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*)
+  -- definition is_trunc_ppi_of_is_conn (k : ℕ₋₂) (P : A → Type*)
-    : is_trunc k.+1 (Π*(a : A), P a) :=
+  --   : 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
+      apply @is_trunc_equiv_closed_rev _ _ k.+1 (ppi_loop_equiv f),
-        (ppi_loop_equiv f),
       apply IH, intro a,
-      apply ptrunctype.mk (Ω (pType.mk (P a) (f a))),
+      apply is_trunc_loop, apply H4 }
-      { apply is_trunc_loop, exact is_trunc_ptrunctype (P a) },
-      { exact pt } }
   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*)
+  definition is_trunc_ppi (A : Type*) (n k : ℕ₋₂) (H : n ≤ k) (P : A → Type*)
-    : is_trunc k (Π*(a : A), P a) :=
+    (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,
+    { apply is_contr_of_merely_prop,
-      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) -2
+      { 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) P H2 },
-                  (trunc_index.le.step H)) pt) },
       { 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
+      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) k _ K P H2 } }
-          (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) K) pt) } }
   end
 
 end is_conn