From 984d564cc626c78b445c55167076938ac223d1b2 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 11:30:09 -0400
Subject: [PATCH] unbundle set in direct_sum

---
 algebra/direct_sum.hlean             | 4 ++--
 algebra/free_commutative_group.hlean | 2 +-
 algebra/free_group.hlean             | 8 ++++----
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index 5d8e388..acc32c3 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -14,10 +14,10 @@ namespace group
 
   section
 
-    parameters {I : Set} (Y : I → AbGroup)
+    parameters {I : Type} [is_set I] (Y : I → AbGroup)
     variables {A' : AbGroup} {Y' : I → AbGroup}
 
-    definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
+    definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)
     local abbreviation ι [constructor] := @free_ab_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
     | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ *  (ι ⟨i, y₁ * y₂⟩)⁻¹)
diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean
index 759be30..d34fef9 100644
--- a/algebra/free_commutative_group.hlean
+++ b/algebra/free_commutative_group.hlean
@@ -15,7 +15,7 @@ namespace group
 
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
-  variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}
+  variables (X : Type) {Y : Type} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
 
   /- Free Abelian Group of a set -/
   namespace free_ab_group
diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean
index 125332d..291a4a8 100644
--- a/algebra/free_group.hlean
+++ b/algebra/free_group.hlean
@@ -15,7 +15,7 @@ namespace group
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
   /- Free Group of a set -/
-  variables (X : Set) {l l' : list (X ⊎ X)}
+  variables (X : Type) [is_set X] {l l' : list (X ⊎ X)}
   namespace free_group
 
   inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
@@ -60,10 +60,10 @@ namespace group
   end
 
   definition free_group_one [constructor] : FG X := class_of []
-  definition free_group_inv [unfold 3] : FG X → FG X :=
+  definition free_group_inv [unfold 4] : FG X → FG X :=
   quotient_unary_map (reverse ∘ map sum.flip)
                      (λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
-  definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
+  definition free_group_mul [unfold 4 5] : FG X → FG X → FG X :=
   quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
 
   section
@@ -123,7 +123,7 @@ namespace group
   definition free_group_inclusion [constructor] (x : X) : free_group X :=
   class_of [inl x]
 
-  definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
+  definition fgh_helper [unfold 6] (f : X → G) (g : G) (x : X + X) : G :=
   g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
 
   theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')