Deduplicate definitions (#1022)

Resolves #992.

Makefile

@@ -62,7 +62,7 @@ src/everything.lagda.md: agdaFiles
 		| cut -c 5-               \
 		| cut -f1 -d'.'           \
 		| sed 's/\//\./g'         \
-		| awk 'BEGIN { FS = "."; OFS = "."; lastdir = "" } { if ($$1 != lastdir) { print ""; lastdir = $$1 } print "open import " $$0 }' \
+		| awk 'BEGIN { FS = "."; OFS = "."; lastdir = "" } { if ($$1 != lastdir) { print ""; lastdir = $$1 } print "open import " $$0 " public"}' \
 		>> $@ ;\
 	echo "\`\`\`" >> $@ ;
 

src/finite-algebra.lagda.md

@@ -8,13 +8,8 @@ module finite-algebra where
 open import finite-algebra.commutative-finite-rings public
 open import finite-algebra.dependent-products-commutative-finite-rings public
 open import finite-algebra.dependent-products-finite-rings public
-open import finite-algebra.finite-abelian-groups public
-open import finite-algebra.finite-commutative-monoids public
 open import finite-algebra.finite-fields public
-open import finite-algebra.finite-groups public
-open import finite-algebra.finite-monoids public
 open import finite-algebra.finite-rings public
-open import finite-algebra.finite-semigroups public
 open import finite-algebra.homomorphisms-commutative-finite-rings public
 open import finite-algebra.homomorphisms-finite-rings public
 open import finite-algebra.products-commutative-finite-rings public

src/finite-algebra/commutative-finite-rings.lagda.md

@@ -591,7 +591,7 @@ module _
     preserves-concat-add-list-Ring-𝔽 finite-ring-Commutative-Ring-𝔽
 ```
 
-### Equip a finite type with a structure of commutative finite ring
+### Equipping a finite type with the structure of a commutative finite ring
 
 ```agda
 module _
@@ -603,14 +603,14 @@ module _
     UU l1
   structure-commutative-ring-𝔽 =
     Σ ( structure-ring-𝔽 X)
-      ( λ r → is-commutative-Ring-𝔽 (compute-structure-ring-𝔽 X r))
+      ( λ r → is-commutative-Ring-𝔽 (finite-ring-structure-ring-𝔽 X r))
 
-  compute-structure-commutative-ring-𝔽 :
+  finite-commutative-ring-structure-commutative-ring-𝔽 :
     structure-commutative-ring-𝔽 →
     Commutative-Ring-𝔽 l1
-  pr1 (compute-structure-commutative-ring-𝔽 (r , c)) =
-    compute-structure-ring-𝔽 X r
-  pr2 (compute-structure-commutative-ring-𝔽 (r , c)) = c
+  pr1 (finite-commutative-ring-structure-commutative-ring-𝔽 (r , c)) =
+    finite-ring-structure-ring-𝔽 X r
+  pr2 (finite-commutative-ring-structure-commutative-ring-𝔽 (r , c)) = c
 
   is-finite-structure-commutative-ring-𝔽 :
     is-finite structure-commutative-ring-𝔽

src/finite-algebra/dependent-products-finite-rings.lagda.md

@@ -156,5 +156,5 @@ module _
   ring-Π-Ring-𝔽 = Π-Ring (type-𝔽 I) (ring-Ring-𝔽 ∘ A)
 
   Π-Ring-𝔽 : Ring-𝔽 (l1 ⊔ l2)
-  Π-Ring-𝔽 = compute-ring-𝔽 ring-Π-Ring-𝔽 is-finite-type-Π-Ring-𝔽
+  Π-Ring-𝔽 = finite-ring-is-finite-Ring ring-Π-Ring-𝔽 is-finite-type-Π-Ring-𝔽
 ```