From e90c657dcb4798f8a1f082a83b6ce1f575ff7ad3 Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 9 Jun 2017 10:08:21 -0600 Subject: [PATCH 1/6] Add dirsum_down_lift. --- algebra/direct_sum.hlean | 43 +++++++++++++++++++++++++++++++++++----- 1 file changed, 38 insertions(+), 5 deletions(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index b21ccd3..142ae36 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -8,7 +8,7 @@ Constructions with groups import .quotient_group .free_commutative_group .product_group -open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops +open eq is_equiv algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops lift namespace group @@ -118,7 +118,7 @@ namespace group } end - variables {I J : Set} {Y Y' Y'' : I → AbGroup} + variables {I J : Type} [is_set I] [is_set J] {Y Y' Y'' : I → AbGroup} definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' := dirsum_elim (λi, dirsum_incl Y' i ∘g f i) @@ -146,7 +146,7 @@ namespace group intro i y, exact sorry end - definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') : + definition dirsum_functor_homotopy (f f' : Πi, Y i →g Y' i) (p : f ~2 f') : dirsum_functor f ~ dirsum_functor f' := begin apply dirsum_homotopy, @@ -167,13 +167,13 @@ namespace group { intro ds, refine (homomorphism_comp_compute (dirsum_functor (λ i, f i)) (dirsum_functor (λ i, (f i)⁻¹ᵍ)) _)⁻¹ ⬝ _, refine dirsum_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵍ) ds ⬝ _, - refine @dirsum_functor_homotopy I Y' Y' _ (λ i, !gid) (λ i, to_right_inv (equiv_of_isomorphism (f i))) ds ⬝ _, + refine dirsum_functor_homotopy _ (λ i, !gid) (λ i, to_right_inv (equiv_of_isomorphism (f i))) ds ⬝ _, exact !dirsum_functor_gid }, { intro ds, refine (homomorphism_comp_compute (dirsum_functor (λ i, (f i)⁻¹ᵍ)) (dirsum_functor (λ i, f i)) _)⁻¹ ⬝ _, refine dirsum_functor_compose (λ i, (f i)⁻¹ᵍ) (λ i, f i) ds ⬝ _, - refine @dirsum_functor_homotopy I Y Y _ (λ i, !gid) (λ i x, + refine dirsum_functor_homotopy _ (λ i, !gid) (λ i x, proof to_left_inv (equiv_of_isomorphism (f i)) x qed @@ -183,3 +183,36 @@ namespace group end end group + +namespace group + + definition dirsum_down_left.{u v} {I : Type.{u}} [is_set I] {Y : I → AbGroup} + : dirsum (Y ∘ down.{u v}) ≃g dirsum Y := + let to_hom := @dirsum_functor_left _ _ _ _ Y down.{u v} in + let from_hom := dirsum_elim (λi, dirsum_incl (Y ∘ down) (up i)) in + begin + fapply isomorphism.mk, + { exact to_hom }, + fapply adjointify, + { exact from_hom }, + { intro ds, + refine (homomorphism_comp_compute to_hom from_hom ds)⁻¹ ⬝ _, + refine @dirsum_homotopy I _ Y (dirsum Y) (to_hom ∘g from_hom) !gid _ ds, + intro i y, + refine homomorphism_comp_compute to_hom from_hom _ ⬝ _, + refine ap to_hom (dirsum_elim_compute (λi, dirsum_incl (Y ∘ down) (up i)) i y) ⬝ _, + refine dirsum_elim_compute _ (up i) y ⬝ _, + reflexivity + }, + { intro ds, + refine (homomorphism_comp_compute from_hom to_hom ds)⁻¹ ⬝ _, + refine @dirsum_homotopy _ _ (Y ∘ down) (dirsum (Y ∘ down)) (from_hom ∘g to_hom) !gid _ ds, + intro i y, induction i with i, + refine homomorphism_comp_compute from_hom to_hom _ ⬝ _, + refine ap from_hom (dirsum_elim_compute (λi, dirsum_incl Y (down i)) (up i) y) ⬝ _, + refine dirsum_elim_compute _ i y ⬝ _, + reflexivity + } + end + +end group From 61e3a9ce0e0808373514ac6b8b0e5ba5673816dc Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 9 Jun 2017 12:25:09 -0400 Subject: [PATCH 2/6] redefine homology to use smash with prespectra --- algebra/seq_colim.hlean | 19 ++++++++++++++++--- colim.hlean | 6 ++++++ homology/homology.hlean | 4 ++-- homotopy/smash.hlean | 6 +++--- homotopy/spectrum.hlean | 22 ++++++++++++++-------- 5 files changed, 41 insertions(+), 16 deletions(-) diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean index d19c4fe..b184bda 100644 --- a/algebra/seq_colim.hlean +++ b/algebra/seq_colim.hlean @@ -6,7 +6,7 @@ namespace group section - parameters (A : ℕ → AbGroup) (f : Πi , A i → A (i + 1)) + parameters (A : ℕ → AbGroup) (f : Πi , A i →g A (i + 1)) variables {A' : AbGroup} definition seq_colim_carrier : AbGroup := dirsum A @@ -72,8 +72,21 @@ namespace group definition seq_colim_functor [constructor] {A A' : ℕ → AbGroup} {f : Πi , A i →g A (i + 1)} {f' : Πi , A' i →g A' (i + 1)} - (h : Πi, A i →g A' i) : seq_colim A f →g seq_colim A' f' := - sorry --_ ∘g _ + (h : Πi, A i →g A' i) (p : Πi, hsquare (f i) (f' i) (h i) (h (i+1))) : + seq_colim A f →g seq_colim A' f' := + seq_colim_elim (λi, seq_colim_incl i ∘g h i) + begin + intro i a, + refine !homomorphism_comp_compute ⬝ _ ⬝ !homomorphism_comp_compute⁻¹, + refine _ ⬝ ap (seq_colim_incl (succ i)) (p i a)⁻¹, + apply seq_colim_glue + end + -- definition seq_colim_functor_compose [constructor] {A A' A'' : ℕ → AbGroup} + -- {f : Πi , A i →g A (i + 1)} {f' : Πi , A' i →g A' (i + 1)} {f'' : Πi , A'' i →g A'' (i + 1)} + -- (h : Πi, A i →g A' i) (p : Πi (a : A i), h (i+1) (f i a) = f' i (h i a)) + -- (h : Πi, A i →g A' i) (p : Πi (a : A i), h (i+1) (f i a) = f' i (h i a)) : + -- seq_colim A f →g seq_colim A' f' := + -- sorry end group diff --git a/colim.hlean b/colim.hlean index 57daa6b..1e5c279 100644 --- a/colim.hlean +++ b/colim.hlean @@ -377,6 +377,12 @@ namespace seq_colim exact !pcompose_pid end + definition seq_colim_equiv_zigzag (g : Π⦃n⦄, A n → A' n) (h : Π⦃n⦄, A' n → A (succ n)) + (p : Π⦃n⦄ (a : A n), h (g a) = f a) (q : Π⦃n⦄ (a : A' n), g (h a) = f' a) : + seq_colim f ≃ seq_colim f' := + sorry + + definition is_equiv_seq_colim_rec (P : seq_colim f → Type) : is_equiv (seq_colim_rec_unc : (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)), diff --git a/homology/homology.hlean b/homology/homology.hlean index f220b76..e656240 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -112,8 +112,8 @@ notation `pH_` n `[`:0 binders `, ` r:(scoped E, parametrized_homology E n) `]`: definition unpointed_homology (X : Type) (E : spectrum) (n : ℤ) : AbGroup := H_ n[X₊, E] -definition homology_functor [constructor] {X Y : Type*} {E F : spectrum} (f : X →* Y) (g : E →ₛ F) (n : ℤ) - : homology X E n →g homology Y F n := +definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f : X →* Y) + (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n := pshomotopy_group_fun n (smash_prespectrum_fun f g) definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} := diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean index 82d5a98..1f0723e 100644 --- a/homotopy/smash.hlean +++ b/homotopy/smash.hlean @@ -664,7 +664,7 @@ namespace smash (!smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans) ⬝pv** smash_functor_pconst_pcompose (pid A) (pid A) g - /- these lemmas are use to show that smash_functor_right is natural in all arguments -/ + /- Using these lemmas we show that smash_functor_right is natural in all arguments -/ definition smash_functor_right_natural_right (f : C →* C') : psquare (smash_functor_right A B C) (smash_functor_right A B C') (ppcompose_left f) (ppcompose_left (pid A ∧→ f)) := @@ -926,8 +926,8 @@ namespace smash refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer)⁻¹, exact hrfl }, end - definition smash_flip_smash_functor (f : A →* C) (g : B →* D) : psquare - (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) := + definition smash_flip_smash_functor (f : A →* C) (g : B →* D) : + psquare (smash_flip A B) (smash_flip C D) (f ∧→ g) (g ∧→ f) := begin apply phomotopy.mk (smash_flip_smash_functor' f g), refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_ap011 ⬝ _, apply ap011_flip, diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 0be9bea..ce7c8df 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -98,7 +98,7 @@ namespace spectrum | succ_str.of_nat zero := z | succ_str.of_nat (succ k) := S (succ_str.of_nat k) - definition psp_of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_prespectrum N) : gen_prespectrum +ℤ := + definition psp_of_gen_indexed [constructor] {N : succ_str} (z : N) (E : gen_prespectrum N) : prespectrum := psp_of_nat_indexed (gen_prespectrum.mk (λn, E (succ_str.of_nat z n)) (λn, gen_prespectrum.glue E (succ_str.of_nat z n))) definition is_spectrum_of_gen_indexed [instance] {N : succ_str} (z : N) (E : gen_prespectrum N) [H : is_spectrum E] @@ -257,20 +257,26 @@ namespace spectrum /- homotopy group of a prespectrum -/ - definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup := - group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k))) + definition pshomotopy_group_hom (n : ℤ) (E : prespectrum) (k : ℕ) + : πag[k + 2] (E (-n - 2 + k)) →g πag[k + 3] (E (-n - 2 + (k + 1))) := begin - intro k, - refine _ ∘ π→g[k+2] (glue E _), - refine (homotopy_group_succ_in _ (k+2))⁻¹ᵉ* ∘ _, - refine homotopy_group_pequiv (k+2) (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc))) + refine _ ∘g π→g[k+2] (glue E _), + refine (ghomotopy_group_succ_in _ (k+1))⁻¹ᵍ ∘g _, + refine homotopy_group_isomorphism_of_pequiv (k+1) + (loop_pequiv_loop (pequiv_of_eq (ap E !add.assoc))) end + definition pshomotopy_group (n : ℤ) (E : prespectrum) : AbGroup := + group.seq_colim (λ(k : ℕ), πag[k+2] (E (-n - 2 + k))) (pshomotopy_group_hom n E) + notation `πₚₛ[`:95 n:0 `]`:0 := pshomotopy_group n definition pshomotopy_group_fun (n : ℤ) {E F : prespectrum} (f : E →ₛ F) : πₚₛ[n] E →g πₚₛ[n] F := - sorry --group.seq_colim_functor _ _ + group.seq_colim_functor (λk, π→g[k+2] (f (-n - 2 +[ℤ] k))) + begin + exact sorry + end notation `πₚₛ→[`:95 n:0 `]`:0 := pshomotopy_group_fun n From 3c51bbea1f8129806b97b7cd405c7987548d8480 Mon Sep 17 00:00:00 2001 From: spiceghello Date: Fri, 9 Jun 2017 10:36:10 -0600 Subject: [PATCH 3/6] minor --- homology/homology.hlean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/homology/homology.hlean b/homology/homology.hlean index e656240..3c90cd3 100644 --- a/homology/homology.hlean +++ b/homology/homology.hlean @@ -116,6 +116,17 @@ definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f : (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n := pshomotopy_group_fun n (smash_prespectrum_fun f g) +definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) : + is_exact_g (homology_functor f (sid (gen_spectrum.to_prespectrum E)) n) + (homology_functor (pcod f) (sid (gen_spectrum.to_prespectrum E)) n) := +begin + esimp[is_exact_g], + -- fconstructor, + -- { intro a, exact sorry }, + -- { intro a, exact sorry } + exact sorry +end + definition homology_theory_spectrum.{u} [constructor] (E : spectrum.{u}) : homology_theory.{u} := begin fapply homology_theory.mk, @@ -125,7 +136,7 @@ begin exact sorry, exact sorry, exact sorry, - exact sorry, + apply homology_theory_spectrum_is_exact, exact sorry -- sorry -- sorry From 88dc53d11398c0cfcea6265a893baa366befc1a5 Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 9 Jun 2017 11:22:15 -0600 Subject: [PATCH 4/6] Add the missing 'p'. --- homotopy/fwedge.hlean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean index 9b3c985..246a114 100644 --- a/homotopy/fwedge.hlean +++ b/homotopy/fwedge.hlean @@ -167,7 +167,7 @@ namespace fwedge ... ~* fwedge_pmap (λ i, !pid ∘* pinl i) : by exact fwedge_pmap_phomotopy (λ i, phomotopy.symm (pid_pcompose (pinl i))) ... ~* !pid : by exact fwedge_pmap_eta !pid - definition fwedge_functor_compose {I : Type} {F F' F'' : I → Type*} (g : Π i, F' i →* F'' i) + definition fwedge_functor_pcompose {I : Type} {F F' F'' : I → Type*} (g : Π i, F' i →* F'' i) (f : Π i, F i →* F' i) : fwedge_functor (λ i, g i ∘* f i) ~* fwedge_functor g ∘* fwedge_functor f := calc fwedge_functor (λ i, g i ∘* f i) ~* fwedge_pmap (λ i, (pinl i ∘* g i) ∘* f i) @@ -183,7 +183,7 @@ namespace fwedge ... ~* fwedge_functor g ∘* fwedge_functor f : by exact fwedge_pmap_eta (fwedge_functor g ∘* fwedge_functor f) - definition fwedge_functor_homotopy {I : Type} {F F' : I → Type*} {f g : Π i, F i →* F' i} + definition fwedge_functor_phomotopy {I : Type} {F F' : I → Type*} {f g : Π i, F i →* F' i} (h : Π i, f i ~* g i) : fwedge_functor f ~* fwedge_functor g := fwedge_pmap_phomotopy (λ i, pwhisker_left (pinl i) (h i)) @@ -192,13 +192,13 @@ namespace fwedge let pfrom := fwedge_functor (λ i, (f i)⁻¹ᵉ*) in begin fapply pequiv_of_pmap, exact pto, - fapply is_equiv.adjointify, exact pfrom, - { intro y, refine (fwedge_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵉ*) y)⁻¹ ⬝ _, - refine fwedge_functor_homotopy (λ i, pright_inv (f i)) y ⬝ _, + fapply adjointify, exact pfrom, + { intro y, refine (fwedge_functor_pcompose (λ i, f i) (λ i, (f i)⁻¹ᵉ*) y)⁻¹ ⬝ _, + refine fwedge_functor_phomotopy (λ i, pright_inv (f i)) y ⬝ _, exact fwedge_functor_pid y }, - { intro y, refine (fwedge_functor_compose (λ i, (f i)⁻¹ᵉ*) (λ i, f i) y)⁻¹ ⬝ _, - refine fwedge_functor_homotopy (λ i, pleft_inv (f i)) y ⬝ _, + { intro y, refine (fwedge_functor_pcompose (λ i, (f i)⁻¹ᵉ*) (λ i, f i) y)⁻¹ ⬝ _, + refine fwedge_functor_phomotopy (λ i, pleft_inv (f i)) y ⬝ _, exact fwedge_functor_pid y } end From 2e55a4a4efe08ff0fb3ae015160943657dbcdd0f Mon Sep 17 00:00:00 2001 From: spiceghello Date: Fri, 9 Jun 2017 11:51:04 -0600 Subject: [PATCH 5/6] fwedge_prespectrum --- homotopy/spectrum.hlean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index ce7c8df..6e7b713 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -5,7 +5,7 @@ Authors: Michael Shulman, Floris van Doorn -/ -import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim +import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim .fwedge open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group seq_colim succ_str EM EM.ops function @@ -593,5 +593,17 @@ spectrify_fun (smash_prespectrum_fun f g) definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum := spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*) + /- Wedge of prespectra -/ + +open fwedge + + definition fwedge_prespectrum.{u v} {I : Type.{v}} (X : I -> prespectrum.{u}) : prespectrum.{max u v} := + begin + fconstructor, + { intro n, exact fwedge (λ i, X i n) }, + { intro n, fapply fwedge_pmap, + intro i, exact Ω→ !pinl ∘* !glue + } + end end spectrum From 0acc5c786d91d842395b0c8911f3e6fa1fbbf40c Mon Sep 17 00:00:00 2001 From: favonia Date: Fri, 9 Jun 2017 11:55:34 -0600 Subject: [PATCH 6/6] Add fwedge_down_left. --- homotopy/fwedge.hlean | 41 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean index 246a114..102addd 100644 --- a/homotopy/fwedge.hlean +++ b/homotopy/fwedge.hlean @@ -7,7 +7,7 @@ The Wedge Sum of a family of Pointed Types -/ import homotopy.wedge ..move_to_lib ..choice -open eq pushout pointed unit trunc_index sigma bool equiv trunc choice unit is_trunc sigma.ops lift +open eq is_equiv pushout pointed unit trunc_index sigma bool equiv trunc choice unit is_trunc sigma.ops lift function definition fwedge' {I : Type} (F : I → Type*) : Type := pushout (λi, ⟨i, Point (F i)⟩) (λi, ⋆) definition pt' [constructor] {I : Type} {F : I → Type*} : fwedge' F := inr ⋆ @@ -123,6 +123,15 @@ namespace fwedge { exact con.left_inv (respect_pt g) } end + definition fwedge_pmap_pinl [constructor] {I : Type} {F : I → Type*} : fwedge_pmap (λi, pinl i) ~* pid (⋁ F) := + begin + fconstructor, + { intro x, induction x, + reflexivity, reflexivity, + apply eq_pathover, apply hdeg_square, refine !elim_glue ⬝ !ap_id⁻¹ }, + { reflexivity } + end + definition fwedge_pmap_equiv [constructor] {I : Type} (F : I → Type*) (X : Type*) : ⋁F →* X ≃ Πi, F i →* X := begin @@ -203,8 +212,34 @@ namespace fwedge } end - definition plift_fwedge.{u v} {I : Type} {F : I → pType.{u}} : plift.{u v} (⋁ F) ≃* ⋁ (λ i, plift.{u v} (F i)) := + definition plift_fwedge.{u v} {I : Type} (F : I → pType.{u}) : plift.{u v} (⋁ F) ≃* ⋁ (plift.{u v} ∘ F) := calc plift.{u v} (⋁ F) ≃* ⋁ F : by exact !pequiv_plift ⁻¹ᵉ* - ... ≃* ⋁ (λ i, plift.{u v} (F i)) : by exact fwedge_pequiv (λ i, !pequiv_plift) + ... ≃* ⋁ (λ i, plift.{u v} (F i)) : by exact fwedge_pequiv (λ i, !pequiv_plift) + + definition fwedge_down_left.{u v} {I : Type} (F : I → pType) : ⋁ (F ∘ down.{u v}) ≃* ⋁ F := + let pto := @fwedge_pmap (lift.{u v} I) (F ∘ down) (⋁ F) (λ i, pinl (down i)) in + let pfrom := @fwedge_pmap I F (⋁ (F ∘ down.{u v})) (λ i, pinl (up.{u v} i)) in + begin + fapply pequiv_of_pmap, + { exact pto }, + fapply adjointify, + { exact pfrom }, + { intro x, exact calc pto (pfrom x) = fwedge_pmap (λ i, (pto ∘* pfrom) ∘* pinl i) x : by exact (fwedge_pmap_eta (pto ∘* pfrom) x)⁻¹ + ... = fwedge_pmap (λ i, pto ∘* (pfrom ∘* pinl i)) x : by exact fwedge_pmap_phomotopy (λ i, passoc pto pfrom (pinl i)) x + ... = fwedge_pmap (λ i, pto ∘* pinl (up.{u v} i)) x : by exact fwedge_pmap_phomotopy (λ i, pwhisker_left pto (fwedge_pmap_beta (λ i, pinl (up.{u v} i)) i)) x + ... = fwedge_pmap pinl x : by exact fwedge_pmap_phomotopy (λ i, fwedge_pmap_beta (λ i, (pinl (down.{u v} i))) (up.{u v} i)) x + ... = x : by exact fwedge_pmap_pinl x + }, + { intro x, exact calc pfrom (pto x) = fwedge_pmap (λ i, (pfrom ∘* pto) ∘* pinl i) x : by exact (fwedge_pmap_eta (pfrom ∘* pto) x)⁻¹ + ... = fwedge_pmap (λ i, pfrom ∘* (pto ∘* pinl i)) x : by exact fwedge_pmap_phomotopy (λ i, passoc pfrom pto (pinl i)) x + ... = fwedge_pmap (λ i, pfrom ∘* pinl (down.{u v} i)) x : by exact fwedge_pmap_phomotopy (λ i, pwhisker_left pfrom (fwedge_pmap_beta (λ i, pinl (down.{u v} i)) i)) x + ... = fwedge_pmap pinl x : by exact fwedge_pmap_phomotopy (λ i, + begin induction i with i, + exact fwedge_pmap_beta (λ i, (pinl (up.{u v} i))) i + end + ) x + ... = x : by exact fwedge_pmap_pinl x + } + end end fwedge