diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean
index ab7e0ef0e..ffcaff4ac 100644
--- a/hott/algebra/groupoid.hlean
+++ b/hott/algebra/groupoid.hlean
@@ -2,22 +2,20 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jakob von Raumer
 -- Ported from Coq HoTT
-import .precategory.basic .precategory.morphism .group
+import .precategory.basic .precategory.morphism .group types.pi
 
-open eq function prod sigma truncation morphism nat path_algebra unit
+open eq function prod sigma pi truncation morphism nat path_algebra unit prod sigma.ops
 
 structure foo (A : Type) := (bsp : A)
 
-structure groupoid [class] (ob : Type) extends precategory ob :=
+structure groupoid [class] (ob : Type) extends parent : precategory ob :=
 (all_iso : Π ⦃a b : ob⦄ (f : hom a b),
-  @is_iso ob (precategory.mk hom _ _ _ assoc id_left id_right) a b f)
+  @is_iso ob parent a b f)
 
 namespace groupoid
 
 attribute all_iso [instance]
 
---set_option pp.universes true
---set_option pp.implicit true
 universe variable l
 open precategory
 definition path_groupoid (A : Type.{l})
@@ -77,11 +75,18 @@ begin
       apply mul_right_inv,
 end
 
--- TODO: This is probably wrong
-open equiv is_equiv
-definition group_equiv {A : Type.{l}} [fx : funext]
-  : group A ≃ Σ (G : groupoid.{l l} unit), @hom unit G ⋆ ⋆ = A :=
-sorry
-
+protected definition hom_group {A : Type} [G : groupoid A] (a : A) :
+  group (hom a a) :=
+begin
+  fapply group.mk,
+    intros (f, g), apply (comp f g),
+    apply homH,
+    intros (f, g, h), apply ((assoc f g h)⁻¹),
+    apply (ID a),
+    intro f, apply id_left,
+    intro f, apply id_right,
+    intro f, exact (morphism.inverse f),
+    intro f, exact (morphism.inverse_compose f),
+end
 
 end groupoid
diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean
index ed8d5ec03..462d39001 100644
--- a/hott/algebra/precategory/morphism.hlean
+++ b/hott/algebra/precategory/morphism.hlean
@@ -92,7 +92,7 @@ namespace morphism
   theorem section_of_id : section_of (ID a) = id :=
   section_eq_intro !id_compose
 
-  theorem iso_of_id : ID a⁻¹ = id :=
+  theorem iso_of_id [H : is_iso (ID a)] : (ID a)⁻¹ = id :=
   inverse_eq_intro_left !id_compose
 
   theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g]
@@ -237,20 +237,27 @@ namespace morphism
       ... = f ∘ id : inverse_compose q
       ... = f : id_right f
 
-  theorem inv_pp [H' : is_iso p] : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ :=
+  theorem inv_pp [H' : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ :=
   have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹,
   have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) = p⁻¹ ∘ p, from ap _ (compose_V_pp q p),
   have H3 : p⁻¹ ∘ p = id, from inverse_compose p,
   inverse_eq_intro_left (H1 ⬝ H2 ⬝ H3)
+
   --the proof using calc is hard for the unifier (needs ~90k steps)
   -- inverse_eq_intro_left
   --   (calc
   --     (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹
   --     ... = (p⁻¹) ∘ p : congr_arg (λx, p⁻¹ ∘ x) (compose_V_pp q p)
   --     ... = id : inverse_compose p)
-  theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▹ inv_pp (q⁻¹) g
-  theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▹ inv_pp q (f⁻¹)
-  theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▹ inv_Vp q (r⁻¹)
+  theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q :=
+  inverse_involutive q ▹ inv_pp (q⁻¹) g
+
+  theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ :=
+  inverse_involutive f ▹ inv_pp q (f⁻¹)
+
+  theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q :=
+  inverse_involutive r ▹ inv_Vp q (r⁻¹)
+
   end
   section
   variables {ob : Type} {C : precategory ob} include C