Group objects via diagrams or generalized elements — Kripke–Joyal?

Question

The notion of a group object $G$ in a category with finite products can either be defined with a few commutative diagrams or via requiring that each hom set $\hom(X,G)$ is a group. There is a theorem that these two definitions are equivalent.

Question: Does the equivalence of these two definitions follow from Kripke–Joyal semantics (Theorem 3.2)?

After all, Kripke–Joyal semantics gives a characterization of truth in the internal language of a topos using generalized elements. (And the second definitions renders as "for each $X$, the generalized elements with stage $X$ constitute a group".)

Answer 1

Sort of. Traditional Kripke–Joyal semantics can only force the truth of predicates, not the existence of structure. So once you have multiplication, unit, and inversion maps, you could use KJ semantics to prove that the necessary diagrams commute if and only if they render each homset into a group. (At least, once you generalize KJ semantics to categories with finite products — I'm not sure I've seen it written down in more generality than categories with finite limits.)

However, Awodey, Gambino, and Hazratpour have recently generalized KJ semantics to dependent type theory (Kripke–Joyal forcing for type theory and uniform fibrations), and you might be able to use that version to deal with the algebraic structure as well.