Added Z mod n as Fin

CHANGELOG.md

@@ -83,9 +83,9 @@ Additions to existing modules
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
 
-* In `Data.Fin.Properties`:
+* In `Data.Fin.Base`:
   ```agda
-  zeroFromNonZero : .⦃ NonZero n ⦄ → Fin n
+  zero⁺ : .⦃ NonZero n ⦄ → Fin n
   ```
 
 * In `Data.Fin.Mod`:

src/Data/Fin/Base.agda

@@ -35,6 +35,11 @@ data Fin : ℕ → Set where
   zero : Fin (suc n)
   suc  : (i : Fin n) → Fin (suc n)
 
+-- Homogeneous Constructors
+
+zero⁺ : .⦃ _ : ℕ.NonZero n ⦄ → Fin n
+zero⁺ {n = suc _} = zero
+
 -- A conversion: toℕ "i" = i.
 
 toℕ : Fin n → ℕ

src/Data/Fin/Mod/Properties.agda

@@ -121,8 +121,8 @@ sucMod-predMod (suc i) = sucMod-inject₁ i
 ------------------------------------------------------------------------
 -- _+_
 
-+-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zeroFromNonZero _+_
++-identityˡ : .{{ _ : NonZero n }} → LeftIdentity zero⁺ _+_
 +-identityˡ {suc n} i rewrite +ℕ-identityʳ {m = toℕ i} {n} _ = fromℕ<-toℕ _ (toℕ≤pred[n] _)
 
-+-identityʳ : .{{ _ : NonZero n }} → RightIdentity zeroFromNonZero _+_
++-identityʳ : .{{ _ : NonZero n }} → RightIdentity zero⁺ _+_
 +-identityʳ {suc _} _ = refl

src/Data/Fin/Properties.agda

@@ -68,9 +68,6 @@ private
 nonZeroIndex : Fin n → ℕ.NonZero n
 nonZeroIndex {n = suc _} _ = _
 
-zeroFromNonZero : .⦃ _ : ℕ.NonZero n ⦄ → Fin n
-zeroFromNonZero {n = suc _} = zero
-
 ------------------------------------------------------------------------
 -- Bundles