From 21c6e8f7e54c90cb22f25a22d0223fb8d5679ead Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 23 Jun 2016 21:53:50 +0100 Subject: [PATCH] small changes after changes in HoTT library --- homotopy/LES_of_homotopy_groups_old.hlean | 2 +- homotopy/spectrum.hlean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/homotopy/LES_of_homotopy_groups_old.hlean b/homotopy/LES_of_homotopy_groups_old.hlean index 0c57021..cdeca83 100644 --- a/homotopy/LES_of_homotopy_groups_old.hlean +++ b/homotopy/LES_of_homotopy_groups_old.hlean @@ -708,7 +708,7 @@ namespace chain_complex namespace old definition CommGroup_LES_of_homotopy_groups3 (n : +6ℕ) : CommGroup.{u} := CommGroup.mk (LES_of_homotopy_groups3 f (pr1 n + 1, pr2 n)) (comm_group_LES_of_homotopy_groups3 f (pr1 n) (pr2 n)) - +exit definition homomorphism_LES_of_homotopy_groups_fun3 : Π(k : +6ℕ), CommGroup_LES_of_homotopy_groups3 f (S k) →g CommGroup_LES_of_homotopy_groups3 f k | (k, fin.mk 0 H) := diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean index 0197517..7511941 100644 --- a/homotopy/spectrum.hlean +++ b/homotopy/spectrum.hlean @@ -33,7 +33,7 @@ end eq open eq namespace pointed definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := - pequiv_of_pmap (g ∘* f) (is_equiv_compose f g) + pequiv_of_pmap (g ∘* f) (is_equiv_compose g f) infixr ` ∘*ᵉ `:60 := pequiv_compose @@ -63,7 +63,7 @@ namespace pointed ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap (λh, h pt) p ⬝ resp_pt g : sigma_equiv_sigma_right (λp, pathover_eq_equiv_Fl p (resp_pt f) (resp_pt g)) ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), resp_pt f = ap10 p pt ⬝ resp_pt g - : sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_ap10 p _) _)) + : sigma_equiv_sigma_right (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), resp_pt f = p pt ⬝ resp_pt g : sigma_equiv_sigma_left' eq_equiv_homotopy ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ resp_pt g = resp_pt f