rename

martinescardo · Sep 8, 2023 · 9b1cbd4 · 9b1cbd4
1 parent 82ce8f9
commit 9b1cbd4
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 5 deletions.
diff --git a/source/Groups/Free.lagda → source/Groups/FreeLarge.lagda b/source/Groups/Free.lagda → source/Groups/FreeLarge.lagda
@@ -33,7 +33,7 @@ church-rosser. This seems to be a bug, but we are not sure.
 
 \begin{code}
 
-module Groups.Free where
+module Groups.FreeLarge 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.Free
+open import Groups.FreeLarge
 open import Groups.Type
 open import MLTT.List
 open import Relations.SRTclosure

diff --git a/source/Groups/index.lagda b/source/Groups/index.lagda
@@ -6,7 +6,7 @@ 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.Free                         -- by Bezem, Coquand, Dybjer and Escardo
+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

diff --git a/source/InjectiveTypes/MathematicalStructuresMoreGeneral.lagda b/source/InjectiveTypes/MathematicalStructuresMoreGeneral.lagda
@@ -425,7 +425,6 @@ Monoid-Π-condition {𝓤} =
     σ-remark : σ p A α ＝ (_·_ , e)
     σ-remark = refl
 
-
     I : is-set (Π A)
     I = Π-is-set fe' (λ h →
          case F h of
@@ -446,7 +445,6 @@ Monoid-Π-condition {𝓤} =
                 case F h of
                  λ (Ah-is-set , ln , rn , assoc) → assoc (f h) (g h) (k h))
 
-
 ainjectivity-of-Monoid : ainjective-type (Monoid {𝓤}) 𝓤 𝓤
 ainjectivity-of-Monoid {𝓤} =
  ainjectivity-of-type-of-structures