diff --git a/personoj/logical.lp b/personoj/logical.lp
index c3db436deb183092082dc99eb2266abf0badefd7..c7ebe31dd1470f4d79b8cd4bf34d4e5c2485607b 100644
--- a/personoj/logical.lp
+++ b/personoj/logical.lp
@@ -14,4 +14,3 @@ rule if {prop} $p $then $else ↪ ($p ⇒ $then) ⇒ (λ _, (¬ $p) ⇒ $else);
 symbol iff P Q ≔ (P ⇒ (λ _, Q)) ∧ (λ _, Q ⇒ (λ _, P));
 
 symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λ x, ¬ (P x)));
-
diff --git a/personoj/nat.lp b/personoj/nat.lp
index 28a44499b65a88468f115a49f2d7f900c8be4826..dcf50b68f4cf64275eec8ef4a9d4cb2cbf6b7139 100644
--- a/personoj/nat.lp
+++ b/personoj/nat.lp
@@ -9,3 +9,13 @@ rule eqnat (succ $n) (succ $m) ↪ eqnat $n $m
 with eqnat zero (succ _) ↪ false
 with eqnat (succ _) zero ↪ false
 with eqnat zero zero ↪ true;
+
+// Recursor on integers
+symbol nrec {t: Set} : Nat → El t → (Nat → El t → El t) → El t;
+rule nrec {$t} (succ $n) $base $f ↪ $f $n (nrec {$t} $n $base $f);
+rule nrec zero $base _ ↪ $base;
+
+// We introduce an object level Nat to have polymorphism on the recursor.
+symbol nat/o: Set;
+rule El nat/o ↪ Nat;
+symbol + (sn m: Nat) ≔ nrec sn m (λ _ npm, succ npm); notation + infix 6;