Consider the constructive logic with a modality □ with the following modal axioms:
□(a → b) → □ a → □ b□ a → a□ a → □ □ a
I believe this is the logic CS4, excluding ◇.
I have had the □ modality explained to me as comonadic, but it seems in this logic it is not, as it is not an endofunctor on the category: we can not prove ∀ a b . (a → b) → □ a → □ b. It would be an endofunctor on the discrete category whose elements are the propositions of the logic; i am not sure whether this is useful. However, it is clearly comonoidal, by the axioms □ a → a and □ a → □ □ a. Have we a well-known notion of such a "comonad-ish" structure?
$\newcommand{\thm}[1]{\begin{array}\\ \hline #1\end{array}}$ As mentioned in the comment, you are conflating several sorts of arrows/mappings in a way that the categorical presentation would not necessarily do. The three notions are:
The internal hom object $[a,b]$ which corresponds to the proposition $a ⇒ b$, as propositions correspond to objects (so, for example $\square a$ is also an object).
Hom sets $C(a,b)$ which correspond to hypothetical judgments/entailments $a ⊢ b$. Exhibiting an arrow $f : a → b$ is like giving a deduction $\begin{array}\\ \hline a ⊢ b\end{array}$
The functorial action, which is like an inference between entailments. $$\frac{a ⊢ b}{\square a ⊢ \square b}$$ because it says that if one entailment exists, a corresponding entailment exists.
There are other ways to organize things, but this illustrates the sort of thing that goes on in all of them, I think.
Now, the counit and comultiplication of the comonad correspond to valid entailments $$\thm{\square a ⊢ a}$$ $$\thm{\square a ⊢ \square \square a}$$ not propositions, although from them we can deduce corresponding theorems $$\thm{⊢ \square a ⇒ a}$$ $$\thm{⊢ \square a ⇒ \square \square a}$$
The functoriality rule of $\square$ above doesn't give similar results, though, and doesn't correspond to your universally quantified proposition being a theorem. Instead it says that if there is a logical entailment between two propositions, then there is also one between their modal analogues. It's typical for this to work because entailment is about the syntactic, logical structure relating propositions, not about the 'truth' of propositions. [1] And even though we have the above inference between entailments, there is not necessarily a valid entailment: $$\thm{a ⇒ b ⊢ \square a ⇒ \square b}$$ which would lead to the problematic theorem you mentioned.
The moral of the story, I suppose, is: category theory (and type theory, and logic) have multiple sorts of 'arrows' between their structures. Don't assume they are all interchangeable with one another. Sometimes they're related (but not the same), and some cases (like the category of sets) are rather degenerate; but often the differences between them are significant and important to think about.
[1] As Alex points out, using the necessitation rule, we can reason:
$$\begin{array} \\ a ⊢ b \\ \hline ⊢ a ⇒ b \\ \hline ⊢ \square(a ⇒ b) \end{array}$$
combining this with the K axiom we can then deduce $$⊢ \square a ⇒ \square b$$ and then reason back to $$\square a ⊢ \square b$$ So this inference is justified under those conditions.