Update nonzero-natural-numbers.lagda.md

UniMath · Mar 4, 2025 · c4619f5 · c4619f5
1 parent 4335da2
commit c4619f5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/elementary-number-theory/nonzero-natural-numbers.lagda.md b/src/elementary-number-theory/nonzero-natural-numbers.lagda.md
@@ -100,6 +100,7 @@ pred-nonzero-ℕ : nonzero-ℕ → ℕ
 pred-nonzero-ℕ (succ-ℕ n , _) = n
 pred-nonzero-ℕ (zero-ℕ , H) = ex-falso (H refl)
 
+pred-ℕ⁺ : nonzero-ℕ → ℕ
 pred-ℕ⁺ = pred-nonzero-ℕ
 
 is-section-succ-nonzero-ℕ' : is-section succ-nonzero-ℕ' pred-nonzero-ℕ