fix(*): fix broken files

group_theory/basic.hlean

@@ -13,17 +13,11 @@ Basic group theory
   The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
 -/
 
-<<<<<<< HEAD
-import algebra.group types.pointed types.pi
-
-open eq algebra pointed function is_trunc pi
-
-=======
 import types.pointed types.pi algebra.bundled algebra.category.category
 
 open eq algebra pointed function is_trunc pi category equiv is_equiv
 set_option class.force_new true
->>>>>>> origin/master
+
 namespace group
 
   definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one

group_theory/constructions.hlean

@@ -356,7 +356,7 @@ namespace group
 
   end
   end free_group open free_group
-  export [reduce_hints] free_group
+--  export [reduce_hints] free_group
   variables (X)
   definition group_free_group [constructor] : group (free_group_carrier X) :=
   group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one

homotopy/sample.hlean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ulrik Buchholtz
 -/
-import types.trunc types.arrow_2 types.fiber .susp
+import types.trunc types.arrow_2 types.fiber homotopy.susp
 
 open eq is_trunc is_equiv nat equiv trunc function fiber
 
@@ -153,7 +153,7 @@ namespace homotopy
   -- Corollary 7.5.5
   definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B}
     (p : f ~ g) (H : is_conn_map n f) : is_conn_map n g :=
-  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H 
+  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
 
   -- all types are -2-connected
   definition minus_two_conn [instance] (A : Type) : is_conn -2 A :=