From 070d687c7f820cf8b6edb471f6949e369f307809 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 24 Sep 2018 17:29:16 +0200 Subject: [PATCH] add functoriality of gloopn' --- hott/algebra/inf_group_theory.hlean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/hott/algebra/inf_group_theory.hlean b/hott/algebra/inf_group_theory.hlean index 63b3e3fd4..cbe7b9d89 100644 --- a/hott/algebra/inf_group_theory.hlean +++ b/hott/algebra/inf_group_theory.hlean @@ -374,8 +374,13 @@ namespace group definition gapn (n : ℕ) [H : is_succ n] {A B : Type*} (f : A →* B) : Ωg[n] A →∞g Ωg[n] B := inf_homomorphism.mk (Ω→[n] f) (by induction H with n; exact apn_con n f) + definition gapn' (n : ℕ) {A B : InfGroup} (f : A →∞g B) : Ωg'[n] A →∞g Ωg'[n] B := + inf_homomorphism.mk (Ω→[n] (pmap_of_inf_homomorphism f)) + (by cases n with n; exact inf_homomorphism.struct f; exact apn_con n (pmap_of_inf_homomorphism f)) + notation `Ωg→` := gap1 notation `Ωg→[`:95 n:0 `]`:0 := gapn n + notation `Ωg'→[`:95 n:0 `]`:0 := gapn' n definition gloop_isomorphism_gloop {A B : Type*} (f : A ≃* B) : Ωg A ≃∞g Ωg B := inf_isomorphism.mk (Ωg→ f) (to_is_equiv (loop_pequiv_loop f))