Rename UU-Fin to Type-With-Cardinality-ℕ (#1316)

UniMath · Feb 14, 2025 · 08e7ad6 · 08e7ad6
1 parent d4d4a7b
commit 08e7ad6
Show file tree

Hide file tree

Showing 68 changed files with 1,572 additions and 1,234 deletions.
diff --git a/src/elementary-number-theory/falling-factorials.lagda.md b/src/elementary-number-theory/falling-factorials.lagda.md
@@ -40,7 +40,7 @@ Fin-falling-factorial-ℕ :
   (n m : ℕ) → Fin (falling-factorial-ℕ n m) ≃ (Fin m ↪ Fin n)
 Fin-falling-factorial-ℕ zero-ℕ zero-ℕ =
   equiv-is-contr
-    ( is-contr-Fin-one-ℕ)
+    ( is-contr-Fin-1)
     ( is-contr-equiv
       ( is-emb id)
       ( left-unit-law-Σ-is-contr
@@ -52,7 +52,7 @@ Fin-falling-factorial-ℕ zero-ℕ (succ-ℕ m) =
   equiv-is-empty id (λ f → map-emb f (inr star))
 Fin-falling-factorial-ℕ (succ-ℕ n) zero-ℕ =
   equiv-is-contr
-    ( is-contr-Fin-one-ℕ)
+    ( is-contr-Fin-1)
     ( is-contr-equiv
       ( is-emb ex-falso)
       ( left-unit-law-Σ-is-contr

diff --git a/src/finite-group-theory/abstract-quaternion-group.lagda.md b/src/finite-group-theory/abstract-quaternion-group.lagda.md
@@ -929,11 +929,11 @@ is-finite-Q8 = unit-trunc-Prop count-Q8
 Q8-Finite-Type : Finite-Type lzero
 Q8-Finite-Type = pair Q8 is-finite-Q8
 
-has-cardinality-eight-Q8 : has-cardinality 8 Q8
+has-cardinality-eight-Q8 : has-cardinality-ℕ 8 Q8
 has-cardinality-eight-Q8 = unit-trunc-Prop equiv-count-Q8
 
-Q8-UU-Fin-8 : UU-Fin lzero 8
-Q8-UU-Fin-8 = pair Q8 has-cardinality-eight-Q8
+Q8-Type-With-Cardinality-ℕ : Type-With-Cardinality-ℕ lzero 8
+Q8-Type-With-Cardinality-ℕ = pair Q8 has-cardinality-eight-Q8
 
 has-finite-cardinality-Q8 : has-finite-cardinality Q8
 has-finite-cardinality-Q8 = pair 8 has-cardinality-eight-Q8

diff --git a/src/finite-group-theory/alternating-concrete-groups.lagda.md b/src/finite-group-theory/alternating-concrete-groups.lagda.md
@@ -35,7 +35,7 @@ module _
   alternating-Concrete-Group : Concrete-Group (lsuc (lsuc lzero))
   alternating-Concrete-Group =
     concrete-group-kernel-hom-Concrete-Group
-      ( UU-Fin-Group lzero n)
-      ( UU-Fin-Group (lsuc lzero) 2)
+      ( Type-With-Cardinality-ℕ-Concrete-Group lzero n)
+      ( Type-With-Cardinality-ℕ-Concrete-Group (lsuc lzero) 2)
       ( cartier-delooping-sign n)
 ```
diff --git a/src/finite-group-theory/alternating-groups.lagda.md b/src/finite-group-theory/alternating-groups.lagda.md
@@ -30,11 +30,11 @@ The alternating group on a finite set `X` is the group of even permutations of
 
 ```agda
 module _
-  {l} (n : ℕ) (X : UU-Fin l n)
+  {l} (n : ℕ) (X : Type-With-Cardinality-ℕ l n)
   where
   alternating-Group : Group l
   alternating-Group = group-kernel-hom-Group
-    ( symmetric-Group (set-UU-Fin n X))
+    ( symmetric-Group (set-Type-With-Cardinality-ℕ n X))
     ( symmetric-Group (Fin-Set 2))
     ( sign-homomorphism n X)
 ```
diff --git a/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md b/src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md
@@ -128,7 +128,10 @@ module _
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 
   cartier-delooping-sign :
-    (n : ℕ) → hom-Concrete-Group (UU-Fin-Group l n) (UU-Fin-Group (lsuc l) 2)
+    (n : ℕ) →
+    hom-Concrete-Group
+      ( Type-With-Cardinality-ℕ-Concrete-Group l n)
+      ( Type-With-Cardinality-ℕ-Concrete-Group (lsuc l) 2)
   cartier-delooping-sign =
     quotient-delooping-sign
       ( orientation-Complete-Undirected-Graph)
@@ -146,29 +149,29 @@ module _
       ( comp-hom-Group
         ( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
         ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-        ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+        ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
         ( comp-hom-Group
           ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-          ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
-          ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+          ( Type-With-Cardinality-ℕ-Group l (n +ℕ 2))
+          ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
           ( hom-group-hom-Concrete-Group
-            ( UU-Fin-Group l (n +ℕ 2))
-            ( UU-Fin-Group (lsuc l) 2)
+            ( Type-With-Cardinality-ℕ-Concrete-Group l (n +ℕ 2))
+            ( Type-With-Cardinality-ℕ-Concrete-Group (lsuc l) 2)
             ( cartier-delooping-sign (n +ℕ 2)))
           ( hom-inv-iso-Group
-            ( group-Concrete-Group (UU-Fin-Group l (n +ℕ 2)))
+            ( Type-With-Cardinality-ℕ-Group l (n +ℕ 2))
             ( loop-group-Set (raise-Fin-Set l (n +ℕ 2)))
-            ( iso-loop-group-fin-UU-Fin-Group l (n +ℕ 2))))
+            ( iso-loop-group-fin-Type-With-Cardinality-ℕ-Group l (n +ℕ 2))))
         ( hom-inv-symmetric-group-loop-group-Set (raise-Fin-Set l (n +ℕ 2))))
       ( comp-hom-Group
         ( symmetric-Group (raise-Fin-Set l (n +ℕ 2)))
         ( symmetric-Group (Fin-Set (n +ℕ 2)))
-        ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
+        ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
         ( comp-hom-Group
           ( symmetric-Group (Fin-Set (n +ℕ 2)))
           ( symmetric-Group (Fin-Set 2))
-          ( group-Concrete-Group (UU-Fin-Group (lsuc l) 2))
-          ( symmetric-abstract-UU-fin-group-quotient-hom
+          ( Type-With-Cardinality-ℕ-Group (lsuc l) 2)
+          ( symmetric-abstract-type-with-cardinality-ℕ-group-quotient-hom
             ( orientation-Complete-Undirected-Graph)
             ( even-difference-orientation-Complete-Undirected-Graph)
             ( λ n _ →

diff --git a/src/finite-group-theory/concrete-quaternion-group.lagda.md b/src/finite-group-theory/concrete-quaternion-group.lagda.md
@@ -37,10 +37,10 @@ equiv-face-cube :
       ( map-axis-equiv-cube (succ-ℕ k) X Y e d a))
 equiv-face-cube k X Y e d a =
   pair
-    ( equiv-complement-element-UU-Fin k
-      ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d)
+    ( equiv-complement-element-Type-With-Cardinality-ℕ k
+      ( pair (dim-cube-Type-With-Cardinality-ℕ (succ-ℕ k) X) d)
       ( pair
-        ( dim-cube-UU-Fin (succ-ℕ k) Y)
+        ( dim-cube-Type-With-Cardinality-ℕ (succ-ℕ k) Y)
         ( map-dim-equiv-cube (succ-ℕ k) X Y e d))
       ( dim-equiv-cube (succ-ℕ k) X Y e)
       ( refl))
@@ -52,24 +52,24 @@ equiv-face-cube k X Y e d a =
             ( dim-equiv-cube (succ-ℕ k) X Y e)
             ( pair d
               ( λ z →
-                has-decidable-equality-has-cardinality
+                has-decidable-equality-has-cardinality-ℕ
                   ( succ-ℕ k)
                   ( has-cardinality-dim-cube (succ-ℕ k) X)
                   ( d)
                   ( z)))
             ( pair
               ( map-dim-equiv-cube (succ-ℕ k) X Y e d)
               ( λ z →
-                has-decidable-equality-has-cardinality
+                has-decidable-equality-has-cardinality-ℕ
                   ( succ-ℕ k)
                   ( has-cardinality-dim-cube (succ-ℕ k) Y)
                   ( map-dim-equiv-cube (succ-ℕ k) X Y e d)
                   ( z)))
             ( refl)
             ( d')))) ∘e
       ( axis-equiv-cube (succ-ℕ k) X Y e
-        ( inclusion-complement-element-UU-Fin k
-          ( pair (dim-cube-UU-Fin (succ-ℕ k) X) d) d')))
+        ( inclusion-complement-element-Type-With-Cardinality-ℕ k
+          ( pair (dim-cube-Type-With-Cardinality-ℕ (succ-ℕ k) X) d) d')))
 
 cube-with-labeled-faces :
   (k : ℕ) → UU (lsuc lzero)