Let $\cal C$ and $\cal D$ be cartesian closed categories, which I will treat type theoretically (i.e. the objects are called types, and $A\to B$ is the exponential object; lambda terms like $\lambda x y.\,\langle y,x\rangle$ represent homs in the category). An applicative functor $F:{\cal C}\to{\cal D}$ consists of the following data:
- A object part $A\in{\cal C} \implies F(A)\in{\cal D}$
- An "application" operator: if $f:F(A\to B)$ and $x:F(A)$ then $f\cdot x:F(B)$
- A unit: if $A\in{\cal C}$ and $a:A$ then $\eta(a):F(A)$
subject to the following axioms:
- $\eta(f)\cdot \eta(a)=\eta(f\,a)$
- $f\cdot \eta(a)=\eta(\lambda g.g\;a)\cdot f$
- $\eta(\circ)\cdot g\cdot f\cdot x=g\cdot (f\cdot x)$
- $\eta(\mathrm{id})\cdot x=x$
(where $\circ$ is the lambda term $\lambda gfx.\,g\,(f\,x)$ and $\mathrm{id}=\lambda x.\,x$). From this, we can define the morphism part of the functor: given a hom $f:A\to B$, we let $F(f):F(A)\to F(B)$ such that $F(f)=\lambda x.\,\eta(f)\cdot x$, and it can be shown that this satisfies the functor laws.
The question is this:
Given $F,G:{\cal C}\to{\cal D}$ with the same object part and the same application operator, are $F$ and $G$ equal? In other words, does the application uniquely determine the unit?
After some extensive investigation I am leaning toward "no", but I've yet to come up with a model that refutes it.
I'm not very familiar with type theory and the notation you're using, so it's possible I'm missing something, but I can't make sense of "if $A ∈ \mathcal C$ and $a : A$ then $η(a) : F(A)$", since $A$ and $FA$ live in different categories. In any case, I'll assume $F$ is an endofunctor, which is the only context I've seen applicativeness defined in anyway. In that case, the answer to your question is yes, and the proof is just a generalization of the fact that a semigroup structure on a set uniquely determines the unit if one exists.
To see this, we'll use the well known fact that applicative functors in programming correspond to lax monoidal endofunctors with tensorial strength on a closed monoidal category. Given that, the proof ends up being one simple diagram, and is at the bottom, but I'll also try to give a quick rundown of the above mentioned equivalence to try to make this somewhat more approachable to people from both camps.
First, let's say that we're given two monoidal closed categories $\mathcal C$ and $\mathcal D$. Then there are two structures a functor $F : \mathcal C → \mathcal D$ can preserve: the monoidal one, and the closed one. Fortunately, since these two structures determine each other, a way of preserving one will also determine a way of preserving the other.
In this case, we're interested in lax monoidal functors, ie. functors equipped with natural transformations $FA ⊗ FB → F(A ⊗ B)$ and $I → FI$ such that things commute. In terms of the closed structures, these correspond to lax closed functors, ie. functors equipped with transformations $F[A, B] → [FA, FB]$ and $I → FI$. The reason I write this is because mathematicians might be more familiar with the first perspective, since we usually view the monoidal structure as primary or at least simpler part of this. Programmers on the other hand usually start with the second perspective, since it more directly expresses what these kinds of functors allow them to do.
We see now that an applicative functor is almost the same thing as a closed endofunctor, which are the same thing as lax monoidal endofunctors. The difference is that applicative functors are equipped with a unit transformation $η : A → FA$, while closed/monoidal functors only come equipped with a unit element $η : I → FI$.
To bridge this, note that there is another piece of structure $F$ can preserve when it is an endofunctor. Since $\mathcal C$ is enriched in itself, it makes sense to ask that our endofunctor $F$ be $\mathcal C$-enriched too, ie. it should come with morphisms $F_{AB} : [A, B] → [FA, FB]$ along with the usual unenriched $\mathrm{Hom}(A, B) → \mathrm{Hom}(FA, FB)$. With a bit of juggling (described briefly on nLab) you can show that this enrichment corresponds to a transformation $A ⊗ FB → F(A ⊗ B)$, also known as tensorial strength for $F$.
Now we see that every monoidal/closed functor with tensorial strength gives rise to an applicative endofunctor in your sense. We only need to "upgrade" the morphism $I → FI$ to a transformation $A → FA$, which we can easily do using the strength of $F$: $A ≅ A ⊗ I → A ⊗ FI → F(A⊗I) → FA$. This is basically the enriched version of the usual bijection $F1 ≅ \mathrm{Nat}(\mathrm{Id}, F)$ for endofunctors on $\mathrm{Set}$.
As a sidenote, the tensorial strength is often left unmentioned, because functors of interest automatically come with a canonical instance of it. This is true in $\mathrm{Set}$, where every endofunctor is obviously enriched, and the same is true in categories of interest for programmers, which as far as I understand should basically amount to the mapping $f ↦ Ff$ being computable.
In any case, we can now show that the unit morphism $η : I → FI$ of any lax monoidal functor is uniquely constrained by the rest of the monoidal structure. To that end, let $F : \mathcal C → \mathcal D$ be a lax monoidal functor with structure morphisms $η : I → FI$ and $φ : FA ⊗ FB → F(A ⊗ B)$, and assume that $η' : I → FI$ also acts as a unit for $F$. Write $λ$, $ρ$ for unitors in $\mathcal C$ and $\mathcal D$, and denote the isomorphism $λ = ρ : I ⊗ I → I$ with $μ$. Then the following cube commutes.
The top and left squares are naturality of $λ$ and $ρ$, while the bottom and right one are coherence conditions on $F$. Note that for $\mathcal C = 1$ and $\mathcal D = \mathrm{Set}$ lax monoidal functors exactly correspond to monoids, and the above diagram boils down to the very familiar argument: $η = η'η = η'$.