rename back

martinescardo · Sep 8, 2023 · 164dc8a · 164dc8a
1 parent 262f0b6
commit 164dc8a
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 17 deletions.
diff --git a/source/Groups/FreeLarge.lagda → source/Groups/Free.lagda b/source/Groups/FreeLarge.lagda → source/Groups/Free.lagda
@@ -33,7 +33,7 @@ church-rosser. This seems to be a bug, but we are not sure.
 
 \begin{code}
 
-module Groups.FreeLarge where
+module Groups.Free where
 
 open import MLTT.Spartan
 open import MLTT.Two

diff --git a/source/Groups/FreeOverLargeLocallySmallSet.lagda b/source/Groups/FreeOverLargeLocallySmallSet.lagda
@@ -64,7 +64,7 @@ module Groups.FreeOverLargeLocallySmallSet
         (pt : propositional-truncations-exist)
        where
 
-open import Groups.FreeLarge
+open import Groups.Free
 open import Groups.Type
 open import MLTT.List
 open import Relations.SRTclosure

diff --git a/source/Groups/index.lagda b/source/Groups/index.lagda
@@ -4,20 +4,24 @@
 
 module Groups.index where
 
-import Groups.Aut                          -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Cokernel                     -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.FreeLarge                    -- by Bezem, Coquand, Dybjer and Escardo
-import Groups.FreeOverLargeLocallySmallSet -- by Bezem, Coquand, Dybjer and Escardo.
-import Groups.GroupActions                 -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Homomorphisms                -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Image                        -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Kernel                       -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Opposite                     -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Quotient                     -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Subgroups                    -- by Martin Escardo, copied to this place by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Torsors                      -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Triv                         -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Type-Supplement              -- by Ettore Aldrovandi and Keri D'Angelo
-import Groups.Type                         -- by Martin Escardo
+import Groups.Type                         -- by [1]
+import Groups.Subgroups                    -- by [1], copied to this place by [3]
+import Groups.Free                         -- by [2]
+import Groups.FreeOverLargeLocallySmallSet -- by [2]
+import Groups.Aut                          -- by [3]
+import Groups.Cokernel                     -- by [3]
+import Groups.GroupActions                 -- by [3]
+import Groups.Homomorphisms                -- by [3]
+import Groups.Image                        -- by [3]
+import Groups.Kernel                       -- by [3]
+import Groups.Opposite                     -- by [3]
+import Groups.Quotient                     -- by [3]
+import Groups.Torsors                      -- by [3]
+import Groups.Triv                         -- by [3]
+import Groups.Type-Supplement              -- by [3]
 
 \end{code}
+
+[1] Martin Escardo
+[2] Bezem, Coquand, Dybjer and Escardo
+[3] Ettore Aldrovandi and Keri D'Angelo