diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean
new file mode 100644
index 000000000..cd742a1de
--- /dev/null
+++ b/hott/algebra/group_theory.hlean
@@ -0,0 +1,260 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+Basic group theory
+
+This file will be rewritten in the future, when we develop are more systematic notation for
+describing homomorphisms
+-/
+
+import algebra.category.category algebra.hott
+
+open eq algebra pointed function is_trunc pi category equiv is_equiv
+set_option class.force_new true
+
+namespace group
+
+  definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
+  definition pType_of_Group [reducible] (G : Group) : Type* := pointed.mk' G
+  definition Set_of_Group (G : Group) : Set := trunctype.mk G _
+
+  definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
+  Group.mk G _
+
+  definition comm_group_Group_of_CommGroup [instance] [constructor] (G : CommGroup)
+    : comm_group (Group_of_CommGroup G) :=
+  begin esimp, exact _ end
+
+  definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) :=
+  Group.struct G
+
+  /- group homomorphisms -/
+
+  definition is_homomorphism [class] [reducible]
+    {G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Type :=
+  Π(g h : G₁), φ (g * h) = φ g * φ h
+
+  section
+  variables {G G₁ G₂ G₃ : Type} {g h : G₁} (ψ : G₂ → G₃) {φ₁ φ₂ : G₁ → G₂} (φ : G₁ → G₂)
+            [group G] [group G₁] [group G₂] [group G₃]
+            [is_homomorphism ψ] [is_homomorphism φ₁] [is_homomorphism φ₂] [is_homomorphism φ]
+
+  definition respect_mul /- φ -/ : Π(g h : G₁), φ (g * h) = φ g * φ h :=
+  by assumption
+
+  theorem respect_one /- φ -/ : φ 1 = 1 :=
+  mul.right_cancel
+    (calc
+      φ 1 * φ 1 = φ (1 * 1) : respect_mul φ
+            ... = φ 1 : ap φ !one_mul
+            ... = 1 * φ 1 : one_mul)
+
+  theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
+  eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one)
+
+  definition is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
+  begin
+    apply function.is_embedding_of_is_injective,
+    intro g g' p,
+    apply eq_of_mul_inv_eq_one,
+    apply H,
+    refine !respect_mul ⬝ _,
+    rewrite [respect_inv φ, p],
+    apply mul.right_inv
+  end
+
+  definition is_homomorphism_compose {ψ : G₂ → G₃} {φ : G₁ → G₂}
+    (H1 : is_homomorphism ψ) (H2 : is_homomorphism φ) : is_homomorphism (ψ ∘ φ) :=
+  λg h, ap ψ !respect_mul ⬝ !respect_mul
+
+  definition is_homomorphism_id (G : Type) [group G] : is_homomorphism (@id G) :=
+  λg h, idp
+
+  end
+
+  structure homomorphism (G₁ G₂ : Group) : Type :=
+    (φ : G₁ → G₂)
+    (p : is_homomorphism φ)
+
+  infix ` →g `:55 := homomorphism
+
+  definition group_fun [unfold 3] [coercion] := @homomorphism.φ
+  definition homomorphism.struct [instance] [priority 2000] {G₁ G₂ : Group} (φ : G₁ →g G₂)
+    : is_homomorphism φ :=
+  homomorphism.p φ
+
+  variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
+
+  definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h :=
+  respect_mul φ g h
+
+  theorem to_respect_one /- φ -/ : φ 1 = 1 :=
+  respect_one φ
+
+  theorem to_respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ :=
+  respect_inv φ g
+
+  definition to_is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
+  is_embedding_homomorphism φ @H
+
+  definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (G₁ →g G₂) :=
+  begin
+    have H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
+    begin
+      fapply equiv.MK,
+      { intro φ, induction φ, constructor, assumption},
+      { intro v, induction v, constructor, assumption},
+      { intro v, induction v, reflexivity},
+      { intro φ, induction φ, reflexivity}
+    end,
+    apply is_trunc_equiv_closed_rev, exact H
+  end
+
+  local attribute group_pType_of_Group pointed.mk' [reducible]
+  definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ :=
+  pmap.mk φ (respect_one φ)
+
+  definition homomorphism_eq (p : group_fun φ₁ ~ group_fun φ₂) : φ₁ = φ₂ :=
+  begin
+    induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p,
+    exact ap (homomorphism.mk φ₁) !is_prop.elim
+  end
+
+  /- categorical structure of groups + homomorphisms -/
+
+  definition homomorphism_compose [constructor] [trans] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ :=
+  homomorphism.mk (ψ ∘ φ) (is_homomorphism_compose _ _)
+
+  definition homomorphism_id [constructor] [refl] (G : Group) : G →g G :=
+  homomorphism.mk (@id G) (is_homomorphism_id G)
+
+  infixr ` ∘g `:75 := homomorphism_compose
+  notation 1       := homomorphism_id _
+
+  structure isomorphism (A B : Group) :=
+    (to_hom : A →g B)
+    (is_equiv_to_hom : is_equiv to_hom)
+
+  infix ` ≃g `:25 := isomorphism
+  attribute isomorphism.to_hom [coercion]
+  attribute isomorphism.is_equiv_to_hom [instance]
+
+  definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ :=
+  equiv.mk φ _
+
+  definition isomorphism_of_equiv [constructor] (φ : G₁ ≃ G₂)
+    (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ :=
+  isomorphism.mk (homomorphism.mk φ p) !to_is_equiv
+
+  definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
+  Group_eq (equiv_of_isomorphism φ) (respect_mul φ)
+
+  definition isomorphism_of_eq {G₁ G₂ : Group} (φ : G₁ = G₂) : G₁ ≃g G₂ :=
+  isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ))
+    begin intros, induction φ, reflexivity end
+
+  definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ :=
+  homomorphism.mk φ⁻¹
+    abstract begin
+    intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
+    rewrite [respect_mul φ, +right_inv φ]
+    end end
+
+  definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G :=
+  isomorphism.mk 1 !is_equiv_id
+
+  definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ :=
+  isomorphism.mk (to_ginv φ) !is_equiv_inv
+
+  definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
+  isomorphism.mk (ψ ∘g φ) !is_equiv_compose
+
+  postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm
+  infixl ` ⬝g `:75 := isomorphism.trans
+
+  -- TODO
+  -- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) :=
+  -- begin
+  --   fapply equiv.MK,
+  --   { exact eq_of_isomorphism},
+  --   { intro p, apply transport _ p, reflexivity},
+  --   { intro p, induction p, esimp, },
+  --   { }
+  -- end
+
+  /- category of groups -/
+
+  definition precategory_group [constructor] : precategory Group :=
+  precategory.mk homomorphism
+                 @homomorphism_compose
+                 @homomorphism_id
+                 (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp))
+                 (λG₁ G₂ φ, homomorphism_eq (λg, idp))
+                 (λG₁ G₂ φ, homomorphism_eq (λg, idp))
+
+  -- TODO
+  -- definition category_group : category Group :=
+  -- category.mk precategory_group
+  -- begin
+  --   intro G₁ G₂,
+  --   fapply adjointify,
+  --   { intro φ, fapply Group_eq, },
+  --   { },
+  --   { }
+  -- end
+
+  /- given an equivalence A ≃ B we can transport a group structure on A to a group structure on B -/
+
+  section
+
+    parameters {A B : Type} (f : A ≃ B) [group A]
+
+    definition group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b')
+
+    definition group_equiv_one : B := f one
+
+    definition group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹
+
+    local infix * := group_equiv_mul
+    local postfix ^ := group_equiv_inv
+    local notation 1 := group_equiv_one
+
+    theorem group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) :=
+    by rewrite [↑group_equiv_mul, +left_inv f, mul.assoc]
+
+    theorem group_equiv_one_mul (b : B) : 1 * b = b :=
+    by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, one_mul, right_inv f]
+
+    theorem group_equiv_mul_one (b : B) : b * 1 = b :=
+    by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, mul_one, right_inv f]
+
+    theorem group_equiv_mul_left_inv (b : B) : b^ * b = 1 :=
+    by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv,
+                +left_inv f, mul.left_inv]
+
+    definition group_equiv_closed : group B :=
+    ⦃group,
+      mul          := group_equiv_mul,
+      mul_assoc    := group_equiv_mul_assoc,
+      one          := group_equiv_one,
+      one_mul      := group_equiv_one_mul,
+      mul_one      := group_equiv_mul_one,
+      inv          := group_equiv_inv,
+      mul_left_inv := group_equiv_mul_left_inv,
+    is_set_carrier := is_trunc_equiv_closed 0 f⦄
+
+  end
+
+  definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G ≃g G0 :=
+  begin
+    fapply isomorphism_of_equiv,
+    { apply equiv_unit_of_is_contr},
+    { intros, reflexivity}
+  end
+
+  definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 :=
+  eq_of_isomorphism (trivial_group_of_is_contr G)
+
+end group
diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index 36f050eec..067191599 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -8,7 +8,7 @@ homotopy groups of a pointed space
 
 import .trunc_group types.trunc .group_theory
 
-open nat eq pointed trunc is_trunc algebra
+open nat eq pointed trunc is_trunc algebra group function equiv unit
 
 namespace eq
 
@@ -64,8 +64,7 @@ namespace eq
     exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end)
   end
 
-  open equiv unit
-  theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A = G0 :=
+  theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 :=
   begin
     apply trivial_group_of_is_contr,
     apply is_trunc_trunc_of_is_trunc,
@@ -80,32 +79,15 @@ namespace eq
 
   definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp
 
-  definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A = πg[n +1] Ω A :=
+  definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] Ω A :=
   begin
-    fapply Group_eq,
+    fapply isomorphism_of_equiv,
     { apply equiv_of_eq, exact ap (ptrunc 0) (loop_space_succ_eq_in A (succ n))},
     { exact abstract [irreducible] begin refine trunc.rec _, intro p, refine trunc.rec _, intro q,
       rewrite [▸*,-+tr_eq_cast_ap, +trunc_transport], refine !trunc_transport ⬝ _, apply ap tr,
       apply loop_space_succ_eq_in_concat end end},
   end
 
-  definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A = πg[n +1] Ω[m] A :=
-  begin
-    revert A, induction m with m IH: intro A,
-    { reflexivity},
-    { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
-      exact ap (ghomotopy_group n) !loop_space_succ_eq_in⁻¹}
-  end
-
-  theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ)
-    (H : is_set (Ω[n] A)) : πg[m+n+1] A = G0 :=
-  !homotopy_group_add ⬝ !trivial_homotopy_of_is_set
-
-  theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m)
-    (H2 : is_set (Ω[n] A)) : πg[m+1] A = G0 :=
-  obtain (k : ℕ) (p : n + k = m), from le.elim H1,
-  ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k) ⬝ trivial_homotopy_add_of_is_set_loop_space k H2
-
   definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
     : π*[n] A →* π*[n] B :=
   ptrunc_functor 0 (apn n f)
@@ -140,7 +122,39 @@ namespace eq
     apply ap tr, apply apn_con
   end
 
-  open group function
+  definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
+    : πg[n+1] A →g πg[n+1] B :=
+  begin
+    fconstructor,
+    { exact phomotopy_group_functor (n+1) f},
+    { apply phomotopy_group_functor_mul}
+  end
+
+  definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B)
+    : πg[n+1] A ≃g πg[n+1] B :=
+  begin
+    apply isomorphism.mk (homotopy_group_homomorphism n f),
+    esimp, apply is_equiv_trunc_functor, apply is_equiv_apn,
+  end
+
+  definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A ≃g πg[n +1] Ω[m] A :=
+  begin
+    revert A, induction m with m IH: intro A,
+    { reflexivity},
+    { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _,
+      apply homotopy_group_isomorphism_of_pequiv,
+      exact pequiv_of_eq !loop_space_succ_eq_in⁻¹}
+  end
+
+  theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ)
+    (H : is_set (Ω[n] A)) : πg[m+n+1] A ≃g G0 :=
+  !homotopy_group_add ⬝g !trivial_homotopy_of_is_set
+
+  theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m)
+    (H2 : is_set (Ω[n] A)) : πg[m+1] A ≃g G0 :=
+  obtain (k : ℕ) (p : n + k = m), from le.elim H1,
+  isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g
+  trivial_homotopy_add_of_is_set_loop_space k H2
 
   /- some homomorphisms -/
 
@@ -162,14 +176,6 @@ namespace eq
     exact ap tr !con_inv
   end
 
-  definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
-    : πg[n+1] A →g πg[n+1] B :=
-  begin
-    fconstructor,
-    { exact phomotopy_group_functor (n+1) f},
-    { apply phomotopy_group_functor_mul}
-  end
-
   notation `π→g[`:95  n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f
 
 end eq
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index a4b81d20e..fdf1f0076 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -77,11 +77,4 @@ namespace algebra
     (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
   Group_eq_of_eq (ua f) (λg h, !cast_ua ⬝ resp_mul g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹)
 
-  definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G = G0 :=
-  begin
-    fapply Group_eq,
-    { apply equiv_unit_of_is_contr},
-    { intros, reflexivity}
-  end
-
 end algebra
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index e257d97be..df8a14ce0 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -7,8 +7,8 @@ Declaration of the circle
 -/
 
 import .sphere
-import types.bool types.int.hott types.equiv
-import algebra.homotopy_group algebra.hott .connectedness
+import types.int.hott
+import algebra.homotopy_group .connectedness
 
 open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra
 
@@ -293,7 +293,7 @@ namespace circle
   preserve_binary_of_inv_preserve base_eq_base_equiv concat (@add ℤ _) decode_add p q
 
   --the carrier of π₁(S¹) is the set-truncation of base = base.
-  open algebra trunc
+  open algebra trunc group
 
   definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ :=
   trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed
@@ -301,16 +301,16 @@ namespace circle
   definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p :=
   eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])
 
-  definition fundamental_group_of_circle : π₁(S¹.) = gℤ :=
+  definition fundamental_group_of_circle : π₁(S¹.) ≃g gℤ :=
   begin
-    apply (Group_eq fg_carrier_equiv_int),
+    apply (isomorphism_of_equiv fg_carrier_equiv_int),
     intros g h,
     induction g with g', induction h with h',
     apply encode_con,
   end
 
   open nat
-  definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. = G0 :=
+  definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. ≃g G0 :=
   begin
     refine @trivial_homotopy_add_of_is_set_loop_space S¹. 1 n _,
     apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv