From bb3995c573d50c91698e3295041befb9fbdeadab Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Fri, 7 Jul 2017 23:04:27 +0100 Subject: [PATCH] isomorphism of truncations of h-groups --- move_to_lib.hlean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 05aa604..ac785a8 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -439,6 +439,13 @@ namespace group definition isomorphism_of_is_contr {G H : Group} (hG : is_contr G) (hH : is_contr H) : G ≃g H := trivial_group_of_is_contr G ⬝g (trivial_group_of_is_contr H)⁻¹ᵍ + definition trunc_isomorphism_of_equiv {A B : Type} [inf_group A] [inf_group B] (f : A ≃ B) + (h : is_mul_hom f) : Group.mk (trunc 0 A) (trunc_group A) ≃g Group.mk (trunc 0 B) (trunc_group B) := + begin + apply isomorphism_of_equiv (equiv.mk (trunc_functor 0 f) (is_equiv_trunc_functor 0 f)), intros x x', + induction x with a, induction x' with a', apply ap tr, exact h a a' + end + end group open group namespace fiber