For a while I believed finite unambiguity to be equivalent to the other definitions of unambiguity.

Definition 1. Finite Unambiguity finite-unambiguity

Define a grammar $𝐴$ to be finitely unambiguous if $𝐴\&𝐴\cong 𝐴$.

There is likely a better name for this.

Definition 2. Unambiguity as Subterminality unambiguity-as-subterminality

A grammar $𝐴$ is unambiguous if the unique map into the terminal object is a monomorphism. That is, $𝐴$ is a subobject of $\top$.

Definition 3. Unambiguity as Unique Map into Codomain unambiguity-as-unique-map

A grammar $𝐴$ is unambiguous if for all grammars $𝐵$ and maps $𝑒,𝑒\prime :𝐴⊢𝐵$ we have $𝑒=𝑒\prime$.

In a category with terminal objects, this is equivalent to unambiguity defined via subterminality.

Definition 3.1. Unambiguity as Subterminality unambiguity-as-subterminality

A grammar $𝐴$ is unambiguous if the unique map into the terminal object is a monomorphism. That is, $𝐴$ is a subobject of $\top$.

We may use an analogy from the category of sets, however I had missed the infinite case when translating this idea to grammars.

It is true that if a grammar is unambiguous, then it is finitely unambiguous. However, the converse does not hold unless the grammar has finitely many parse trees for each string. This finiteness condition is a semantic one. If this proof of unambiguity were to be internalized, then it could maybe be captured through the lens of some grammar of finite cardinals.

Let $𝐴≔{⨁}_{𝑛:\mathbb{N}}\top$. $𝐴$ is finitely unambiguous but not unambiguous. The isomorphism between $𝐴$ and $𝐴\&𝐴$ amounts to building a bijection between $\mathbb{N}$ and $\mathbb{N}\times \mathbb{N}$, which is straightforward.