Internal Finiteness

Define a grammar $𝐴$ to be finite (or perhaps subfinite) if it is a subobject of grammar of finite cardinals.

𝐴 ↪ 𝖥𝗂𝗇

Where $𝖥𝗂𝗇$ is defined as follows.

Definition 1. A Grammar of Finite Cardinals finite-cardinal-grammar

Define a grammar for each finite cardinal $𝑛 : ℕ$ .

[0] ≔ ⊥

[𝗌𝗎𝖼 (𝑛)] ≔ ⊤ \oplus [𝑛]

Then define the grammar of all finite cardinals as

𝖥𝗂𝗇 ≔ ⨁_{𝑛 : ℕ} [𝑛]