michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of https://github.com/cmu-phil/Spectral

Browse source
This commit is contained in:
Egbert Rijke 2017-07-07 20:12:08 +01:00
commit 39526a821c
7 changed files with 241 additions and 97 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
homotopy/EM.hlean
View file

@ -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

120
homotopy/serre.hlean
View file

@ -8,7 +8,7 @@ set_option pp.binder_types true
namespace pointed
definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
ptrunc.elim (n.+1) !ptr
ptrunc.elim (n.+1) (ptr n A)
definition ptrunc_functor_postnikov_map {A B : Type*} (n : ℕ₋₂) (f : A →* B) :
ptrunc_functor n f ∘* postnikov_map A n ~* ptrunc.elim (n.+1) (!ptr ∘* f) :=
@ -68,39 +68,95 @@ this⁻¹ᵛ*
end pointed open pointed
namespace spectrum
/- begin move -/
definition is_strunc_strunc_pred (X : spectrum) (k : ℤ) : is_strunc k (strunc (k - 1) X) :=
λn, @(is_trunc_of_le _ (maxm2_monotone (add_le_add_right (sub_one_le k) n))) !is_strunc_strunc
definition ptrunc_maxm2_pred {n m : ℤ} (A : Type*) (p : n - 1 = m) :
ptrunc (maxm2 m) A ≃* ptrunc (trunc_index.pred (maxm2 n)) A :=
begin
cases n with n, cases n with n, apply pequiv_of_is_contr,
induction p, apply is_trunc_trunc,
apply is_contr_ptrunc_minus_one,
exact ptrunc_change_index (ap maxm2 (p⁻¹ ⬝ !add_sub_cancel)) A,
exact ptrunc_change_index (ap maxm2 p⁻¹) A
end
definition ptrunc_maxm2_pred_nat {n : ℕ} {m l : ℤ} (A : Type*)
(p : nat.succ n = l) (q : pred l = m) (r : maxm2 m = trunc_index.pred (maxm2 (nat.succ n))) :
@ptrunc_maxm2_pred (nat.succ n) m A (ap pred p ⬝ q) ~* ptrunc_change_index r A :=
begin
have ap maxm2 ((ap pred p ⬝ q)⁻¹ ⬝ add_sub_cancel n 1) = r, from !is_set.elim,
induction this, reflexivity
end
definition EM_type_pequiv_EM (A : spectrum) (n k : ℤ) (l : ℕ) (p : n + k = l) :
EM_type (A k) l ≃* EM (πₛ[n] A) l :=
begin
symmetry,
cases l with l,
{ exact shomotopy_group_pequiv_homotopy_group A p },
{ cases l with l,
{ apply EM1_pequiv_EM1, exact shomotopy_group_isomorphism_homotopy_group A p },
{ apply EMadd1_pequiv_EMadd1 (l+1), exact shomotopy_group_isomorphism_homotopy_group A p }}
end
/- end move -/
definition postnikov_smap [constructor] (X : spectrum) (k : ℤ) :
strunc k X →ₛ strunc (k - 1) X :=
strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k)
/-
we could try to prove that postnikov_smap is homotopic to postnikov_map, although the types
are different enough, that even stating it will be quite annoying
-/
definition postnikov_map_pred (A : Type*) (n : ℕ₋₂) :
ptrunc n A →* ptrunc (trunc_index.pred n) A :=
begin cases n with n, exact !pid, exact postnikov_map A n end
definition pfiber_postnikov_map_pred (A : Type*) (n : ℕ) :
pfiber (postnikov_map_pred A n) ≃* EM_type A n :=
begin
cases n with n,
apply pfiber_pequiv_of_is_contr, apply is_contr_ptrunc_minus_one,
exact pfiber_postnikov_map A n
end
definition pfiber_postnikov_map_pred' (A : spectrum) (n k l : ℤ) (p : n + k = l) :
pfiber (postnikov_map_pred (A k) (maxm2 l)) ≃* EM_spectrum (πₛ[n] A) l :=
begin
cases l with l l,
{ refine pfiber_postnikov_map_pred (A k) l ⬝e* _,
exact EM_type_pequiv_EM A n k l p },
{ apply pequiv_of_is_contr, apply is_contr_pfiber_pid,
apply is_contr_EM_spectrum_neg }
end
definition psquare_postnikov_map_ptrunc_elim (A : Type*) {n k l : ℕ₋₂} (H : is_trunc n (ptrunc k A))
(p : n = l.+1) (q : k = l) :
psquare (ptrunc.elim n (ptr k A)) (postnikov_map A l)
(ptrunc_change_index p A) (ptrunc_change_index q A) :=
begin
induction q, cases p,
refine _ ⬝pv* pvrfl,
apply ptrunc_elim_phomotopy2,
reflexivity
end
definition postnikov_smap_postnikov_map (A : spectrum) (n k l : ℤ) (p : n + k = l) :
psquare (postnikov_smap A n k) (postnikov_map_pred (A k) (maxm2 l))
(ptrunc_maxm2_change_int p (A k)) (ptrunc_maxm2_pred (A k) (ap pred p⁻¹ ⬝ add.right_comm n k (- 1))) :=
begin
cases l with l,
{ cases l with l, apply phomotopy_of_is_contr_cod, apply is_contr_ptrunc_minus_one,
refine psquare_postnikov_map_ptrunc_elim (A k) _ _ _ ⬝hp* _,
exact ap maxm2 (add.right_comm n (- 1) k ⬝ ap pred p ⬝ !pred_succ),
apply ptrunc_maxm2_pred_nat },
{ apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
end
definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) :
sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) k :=
begin
exact sorry
/- symmetry, apply spectrum_pequiv_of_nat_succ_succ, clear k, intro k,
apply EMadd1_pequiv k,
{ exact sorry
-- refine _ ⬝g shomotopy_group_strunc n A,
-- exact chain_complex.LES_isomorphism_of_trivial_cod _ _
-- (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
-- (trivial_homotopy_group_of_is_trunc _ (le_succ _))
},
{ exact sorry --apply is_conn_fun_trunc_elim, apply is_conn_fun_tr
},
{ -- have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
-- have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
-- apply is_trunc_pfiber
exact sorry
}-/
end
sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) (n + k) :=
proof
pfiber_pequiv_of_square _ _ (postnikov_smap_postnikov_map A n k (n + k) idp) ⬝e*
pfiber_postnikov_map_pred' A n k _ idp
qed
section atiyah_hirzebruch
parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
@ -141,10 +197,18 @@ section atiyah_hirzebruch
(λn s, πₛ[n] (sfiber (postnikov_smap (spi X Y) s))) ⟹ᵍ (λn, πₛ[n] (strunc s₀ (spi X Y))) :=
converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
lemma spi_EM_spectrum (k n : ℤ) :
EM_spectrum (πₛ[n] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k :=
sorry
lemma spi_EM_spectrum (n : ℤ) : Π(k : ℤ),
EM_spectrum (πₛ[n] (spi X Y)) (n + k) ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k :=
begin
exact sorry
-- apply spectrum_pequiv_of_nat_add 2, intro k,
-- fapply EMadd1_pequiv (k+1),
-- { exact sorry },
-- { exact sorry },
-- { apply is_trunc_ppi, rotate 1, intro x, },
end
set_option formatter.hide_full_terms false
definition atiyah_hirzebruch_convergence :
(λn s, opH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) :=
converges_to_g_isomorphism atiyah_hirzebruch_convergence'

116
homotopy/spectrum.hlean
View file

@ -59,6 +59,30 @@ namespace spectrum
exact add.assoc n 1 1
end
definition gluen {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ)
: X n →* Ω[k] (X (n +' k)) :=
by induction k with k f; reflexivity; exact !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X (n +' k)) ∘* f
-- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
: X n ≃* Ω[k] (X (n +' k)) :=
by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k))
⬝e* !loopn_succ_in⁻¹ᵉ*)
definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) :
(equiv_gluen X n (k+1))⁻¹ᵉ* ~*
(equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
begin
refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine pwhisker_left _ !pinv_pinv
end
definition succ_str_add_eq_int_add (n : ℤ) (m : ℕ) : @succ_str.add sint n m = n + m :=
begin
induction m with m IH,
{ symmetry, exact add_zero n },
{ exact ap int.succ IH ⬝ add.assoc n m 1 }
end
-- a square when we compose glue with transporting over a path in N
definition glue_ptransport {N : succ_str} (X : gen_prespectrum N) {n n' : N} (p : n = n') :
glue X n' ∘* ptransport X p ~* Ω→ (ptransport X (ap S p)) ∘* glue X n :=
@ -309,14 +333,16 @@ namespace spectrum
{ exact spectrum_pequiv_of_pequiv_succ -[1+succ n] IH }
end
-- definition spectrum_pequiv_of_nat_add {E F : spectrum} (m : ℕ)
-- (e : Π(n : ℕ), E (n + m) ≃* F (n + m)) : Π(n : ℤ), E n ≃* F n :=
-- begin
-- apply spectrum_pequiv_of_nat,
-- refine nat.rec_down _ m e _,
-- intro n f m, cases m with m,
-- end
definition spectrum_pequiv_of_nat_add {E F : spectrum} (m : ℕ)
(e : Π(n : ℕ), E (n + m) ≃* F (n + m)) : Π(n : ℤ), E n ≃* F n :=
begin
apply spectrum_pequiv_of_nat,
refine nat.rec_down _ m e _,
intro n f k, cases k with k,
exact spectrum_pequiv_of_pequiv_succ _ (f 0),
exact pequiv_ap E (ap of_nat (succ_add k n)) ⬝e* f k ⬝e*
pequiv_ap F (ap of_nat (succ_add k n))⁻¹
end
definition is_contr_spectrum_of_nat {E : spectrum} (e : Π(n : ℕ), is_contr (E n)) (n : ℤ) :
is_contr (E n) :=
@ -674,6 +700,56 @@ set_option pp.coercions true
refine !sglue_square ⬝v* ap1_psquare !pequiv_of_eq_commute
end
definition homotopy_group_spectrum_irrel_one {n m : ℤ} {k : ℕ} (E : spectrum) (p : n + 1 = m + k)
[Hk : is_succ k] : πg[k] (E n) ≃g π₁ (E m) :=
begin
induction Hk with k,
change π₁ (Ω[k] (E n)) ≃g π₁ (E m),
apply homotopy_group_isomorphism_of_pequiv 0,
symmetry,
have m + k = n, from (pred_succ (m + k))⁻¹ ⬝ ap pred (add.assoc m k 1 ⬝ p⁻¹) ⬝ pred_succ n,
induction (succ_str_add_eq_int_add m k ⬝ this),
exact equiv_gluen E m k
end
definition homotopy_group_spectrum_irrel {n m : ℤ} {l k : ℕ} (E : spectrum) (p : n + l = m + k)
[Hk : is_succ k] [Hl : is_succ l] : πg[k] (E n) ≃g πg[l] (E m) :=
have Πa b c : ℤ, a + (b + c) = c + (b + a), from λa b c,
!add.assoc⁻¹ ⬝ add.comm (a + b) c ⬝ ap (λx, c + x) (add.comm a b),
have n + 1 = m + 1 - l + k, from
ap succ (add_sub_cancel n l)⁻¹ ⬝ !add.assoc ⬝ ap (λx, x + (-l + 1)) p ⬝ !add.assoc ⬝
ap (λx, m + x) (this k (-l) 1) ⬝ !add.assoc⁻¹ ⬝ !add.assoc⁻¹,
homotopy_group_spectrum_irrel_one E this ⬝g
(homotopy_group_spectrum_irrel_one E (sub_add_cancel (m+1) l)⁻¹)⁻¹ᵍ
definition shomotopy_group_isomorphism_homotopy_group {n m : ℤ} {l : ℕ} (E : spectrum) (p : n + m = l)
[H : is_succ l] : πₛ[n] E ≃g πg[l] (E m) :=
have 2 - n + l = m + 2, from
ap (λx, 2 - n + x) p⁻¹ ⬝ !add.assoc⁻¹ ⬝ ap (λx, x + m) (sub_add_cancel 2 n) ⬝ add.comm 2 m,
homotopy_group_spectrum_irrel E this
definition shomotopy_group_pequiv_homotopy_group_ab {n m : ℤ} {l : ℕ} (E : spectrum) (p : n + m = l)
[H : is_at_least_two l] : πₛ[n] E ≃g πag[l] (E m) :=
begin
induction H with l,
exact shomotopy_group_isomorphism_homotopy_group E p
end
definition shomotopy_group_pequiv_homotopy_group {n m : ℤ} {l : ℕ} (E : spectrum) (p : n + m = l) :
πₛ[n] E ≃* π[l] (E m) :=
begin
cases l with l,
{ apply ptrunc_pequiv_ptrunc, symmetry,
change E m ≃* Ω (Ω (E (2 - n))),
refine !equiv_glue ⬝e* loop_pequiv_loop _,
refine !equiv_glue ⬝e* loop_pequiv_loop _,
apply pequiv_ap E,
have -n = m, from neg_eq_of_add_eq_zero p,
induction this,
rexact add.assoc (-n) 1 1 ⬝ add.comm (-n) 2 },
{ exact pequiv_of_isomorphism (shomotopy_group_isomorphism_homotopy_group E p) }
end
section
open chain_complex prod fin group
@ -936,23 +1012,6 @@ set_option pp.coercions true
definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
spectrum.MK (spectrify_type X) (spectrify_pequiv X)
definition gluen {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ)
: X n →* Ω[k] (X (n +' k)) :=
by induction k with k f; reflexivity; exact !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X (n +' k)) ∘* f
-- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
: X n ≃* Ω[k] (X (n +' k)) :=
by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k))
⬝e* !loopn_succ_in⁻¹ᵉ*)
definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) :
(equiv_gluen X n (k+1))⁻¹ᵉ* ~*
(equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
begin
refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine pwhisker_left _ !pinv_pinv
end
definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X :=
begin
fapply smap.mk,
@ -1082,6 +1141,13 @@ spectrify_fun (smash_prespectrum_fun f g)
(is_contr_spectrum_of_nat (λk, is_contr_EM k !is_trunc_lift) n)
!is_trunc_lift
definition is_contr_EM_spectrum_neg (G : AbGroup) (n : ℕ) : is_contr (EM_spectrum G (-[1+n])) :=
begin
induction n with n IH,
{ apply is_contr_loop, exact is_trunc_EM G 0 },
{ apply is_contr_loop_of_is_contr, exact IH }
end
/- Wedge of prespectra -/
open fwedge

32
homotopy/strunc.hlean
View file

@ -40,7 +40,7 @@ namespace spectrum
definition ptrunc_maxm2_change_int {k l : ℤ} (p : k = l) (X : Type*)
: ptrunc (maxm2 k) X ≃* ptrunc (maxm2 l) X :=
pequiv_ap (λ n, ptrunc (maxm2 n) X) p
ptrunc_change_index (ap maxm2 p) X
definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
: is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
@ -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) :=

21
move_to_lib.hlean
View file

@ -232,7 +232,7 @@ namespace int
definition le_add_one (n : ℤ) : n ≤ n + 1:=
le_add_nat n 1
end int
end int open int
namespace pmap
@ -250,6 +250,15 @@ namespace lift
end lift
namespace trunc
open trunc_index
definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ :=
equiv.MK add_two sub_two add_two_sub_two sub_two_add_two
definition is_set_trunc_index [instance] : is_set ℕ₋₂ :=
is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat
definition is_contr_ptrunc_minus_one (A : Type*) : is_contr (ptrunc -1 A) :=
is_contr_of_inhabited_prop pt
-- TODO: redefine loopn_ptrunc_pequiv
definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) :
@ -320,6 +329,9 @@ namespace trunc
have is_trunc k (ptrunc l X), from is_trunc_of_le _ p,
ptrunc.elim _ (ptr l X)
definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ :=
begin cases n with n, exact -2, exact n end
end trunc
namespace is_trunc
@ -419,6 +431,13 @@ namespace group
end group open group
namespace fiber
definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) :=
is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end
end fiber
namespace function
variables {A B : Type} {f f' : A → B}
open is_conn sigma.ops

3
pointed.hlean
View file

@ -2,7 +2,7 @@
-- Author: Floris van Doorn
import types.pointed2
import types.pointed2 .move_to_lib
open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group
@ -220,5 +220,4 @@ namespace pointed
begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end
end pointed

44
pointed_pi.hlean
View file

@ -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