When does a left adjoint between Heyting algebras preserve 1?

Following the suggestion by Alex Kruckman, let us consider a more general situation. Let $A,B$ be complete cartesian closed categories, and $f : A \to B$ be a functor (between the underlying categories) which is left adjoint to a functor $g : B \to C$. We want to find conditions when

• $f$ preserves binary products, i.e. for all $a,a' \in A$ the canonical morphism $f(a \times a') \to f(a) \times f(a')$ is an isomorphism.
• $f$ preserves the terminal object, i.e. the canonical morphism $f(1) \to 1$ is an isomorphism.

By the Yoneda Lemma, $f$ preserves binary products iff for all $a,a' \in A$ and $t \in B$ the induced morphism $$\hom(f(a) \times f(a'),t) \to \hom(f(a \times a'),t)$$ is an isomorphism. Now let us compute both sides: $$\begin{array}{cll} \hom(f(a) \times f(a'),t) & \cong & \hom(f(a),\underline{\hom}(f(a'),t)) \\ & \cong & \hom(a,g(\underline{\hom}(f(a'),t)))\\\\ \hom(f(a \times a'),t) & \cong & \hom(a \times a',g(t)) \\ & \cong & \hom(a,\underline{\hom}(a',g(t)))\end{array}$$ This shows that there is a canonical morphism (again by the Yoneda Lemma) $$g(\underline{\hom}(f(a'),t)) \to \underline{\hom}(a',g(t))$$ which is an isomorphism for all $a',t$ iff $f$ preserves binary products (Yoneda once again).

Similarly, $f(1) \to 1$ is an isomorphism iff for all $t \in B$ the induced morphism $$\hom(1,t) \to \hom(f(1),t) \cong \hom(1,g(t))$$ is an isomorphism, i.e. $g$ induces isomorphisms on "global sections".

Actually the same proofs work when $A,B$ are symmetric monoidal categories and $f$ is an oplax monoidal functor, for which we want to find conditions that it is a strong monoidal functor. Here is an example from algebraic geometry: If $f : X \to Y$ is a morphism of ringed spaces, then $f^* : \mathsf{Mod}(Y) \to \mathsf{Mod}(X)$ is strong monoidal. For example, $f^* \mathcal{O}_Y \cong \mathcal{O}_X$ since $f_*$ induces isomorphisms on global sections (by the very definition of $f_*$).

If $A,B$ are complete Heyting algebras (i.e. skeletal complete cartesian closed categories), we have $\hom(1,t) = \{\mathrm{id}_1\}$ for $t=1$ and $=\emptyset$ otherwise. This shows: $f(1)=1$ iff $g^{-1}(\{1\})=\{1\}$.

I've been thinking about this question for a bit. It seems to me that we can't be looking for an answer too "similar" to $g(fa\to b)=a\to gb$ because this is an equation in $A$, and such an equation will not (I believe) suffice for $f1=1$. The idea is that requiring $f1=1$ asks that "$1\in B$ must be in the image of $f$", whereas requiring $f$ to be meet-preserving doesn't ask that "every meet in $B$ must be of the form $f(a_1\wedge a_2)$ for some $a_1,a_2\in A$".

So, in my opinion, a reasonable answer to the question would be to come up with an indirect way of writing $1\in B$ in terms of $\to$ and then simply require $f1$ to equal that expression. For example, it turns out that $1=fa\to f1$ for all $a\in A$, and thus we could say that $f$ preserves 1 if and only if $$f1=fa\to f1$$ for all $a\in A$. I am not totally satisfied with this answer, but I will at least prove it.

Proof: Let's first establish what properties we can use. Since $B$ is a Heyting algebra we have $$\tag{1}b\wedge c\leq d\quad\Leftrightarrow\quad b\leq c\to d$$ for all $b,c,d\in B$. We are also given that $f$ is left adjoint to $g$, which means that $$\tag{2}fa\leq b\quad\Leftrightarrow\quad a\leq gb$$ for all $a\in A$ and all $b\in B$.

Now since $f1\leq f1$ we have $1\leq g(f1)$ by (2), so if $a\in A$ then we have $fa\leq f1$ by (2) again because $a\leq 1\leq g(f1)$. Therefore $1\wedge fa\leq f1$ for all $a\in A$, and as such $1\leq fa\to f1$ for all $a\in A$ by (1). Hence $fa\to f1=1$ for all $a\in A$.