Describe the category of groups of $C$, and show that it has finite products. 
(Assuming $C$ has finite products and a terminal object $t$)
Describe the category of groups of $C$, and show that it has finite products.

I can see that the objects of $\text{Grp}(C)$ are groups in $C$ where each object is of the form $\bar c=\langle c, \mu:c \times c \rightarrow c, \eta: t \rightarrow c \rangle$ and arrows $f: \bar c →\bar c' $ are maps such that $f(\bar c)=\bar c'$ satisfies the commutative diagram requirements of a group in $C$, but I'm having trouble showing $\text{Grp}(C)$ has finite products.
I would think it's due to some similarity betwen $\prod_i c_i$ and $\langle \bar c_1, \dots, \bar c_n \rangle$, but I can't pinpoint what is is.
Anyone have any ideas?
 A: You can get your intuition in the case $\mathcal{C}=\mathbf{Set}$. Given groups $G$ and $H$, the group $G \times H$ has unit and multiplication defined by
$$e_{G \times H} = \langle e_G, e_H \rangle \quad \text{and} \quad \langle g,h \rangle \cdot \langle g', h' \rangle = \langle g \cdot g', h \cdot h' \rangle$$
Transferring this to the general setting, suppose you have two internal groups
$$\bar c = (c,\eta : t \to c,\mu : c \times c \to c) \text{ and } \bar d =
 (d,\sigma : t \to d,\tau : d \times d \to d)$$
You would expect the underlying object of $\bar c \times \bar d$ to be $c \times d$. Now


*

*There is a map $t \to c \times d$ given by $\langle \eta,\sigma \rangle$;

*There is a map $(c \times d) \times (c \times d) \to c \times d$ given by the composite
$$(c \times d) \times (c \times d) \overset{\cong}{\longrightarrow} (c \times c) \times (d \times d) \overset{\mu \times \tau}{\longrightarrow} c \times d$$


You just need to check that this data truly does define an internal group in $\mathcal{C}$, and that it satisfies the appropriate universal property.
You should also prove that $\mathbf{Grp}(\mathcal{C})$ has a terminal object—this is straightforward. The existence of all finite products then follows from the existence of binary products and a terminal object.
A: I recommend Clive Newstead's answer over this one, but this is the "high-powered" way of answering the question. Each step is actually a fairly easy result, and I consider this (and surrounding theory) one of the more successful applications of "pure" category theory.
A Lawvere theory is a small category with an object $[1]$ and all its finite products which we'll write as $[n]$ for the $n$-fold finite product, so $[0]$ is the terminal object and $[2]=[1]\times[1]$. Besides the arrows implied by the finite products, for any particular theory we add additional arrows and assert certain diagrams commute. For the Lawvere theory of groups, $\mathcal{T}_{\mathbf{Grp}}$, this would mean having arrows $\mu : [2]\to[1]$, $\iota:[1]\to[1]$, and $\eta:[0]\to[1]$ with the usual commutative diagrams and all arrows induced by these.
A model of a Lawvere theory, $\mathcal{T}$, is then a finite-product preserving functor $F:\mathcal{T}\to\mathcal{E}$ where $\mathcal{E}$ is a category with finite-products. The category of models of a Lawvere theory $\mathcal{T}$ in $\mathcal{E}$ is the full subcategory of functors $\mathcal{T}\to\mathcal{E}$ consisting of the finite-product preserving functors, call it $[\mathcal{T},\mathcal{E}]_{fp}$. Thus, $\mathbf{Grp}(C)\simeq [\mathcal{T}_{\mathbf{Grp}},C]_{fp}$.
Now if $\mathcal{E}$ has limits of some shape, then the category of all functors $\mathcal{D}\to\mathcal{E}$ written $[\mathcal{D},\mathcal{E}]$ also has limits of that shape and they are evaluated pointwise, meaning the limit of a diagram of functors is just a functor that computes that limit by applying each functor in the diagram to its argument. In symbols, $(\text{Lim}D)(X)\cong \text{Lim}(I\mapsto D(I)(X))$. Since finite products are limits and limits commute with each other, the limit of a diagram of finite product preserving functors is finite product preserving. You have $$\begin{align}
(\text{Lim}D)(X\times Y) & \cong\text{Lim}(I\mapsto D(I)(X\times Y)) \\
& \cong\text{Lim}(I\mapsto D(I)(X)\times D(I)(Y)) \\
& \cong\text{Lim}(I \mapsto D(I)(X))\times\text{Lim}(I\mapsto D(I)(Y)) \\
& \cong(\text{Lim}D)(X)\times(\text{Lim}D)(Y)
\end{align}$$
As a consequence, all categories of models for any Lawvere theory have limits of a given shape if the target category ($\mathcal{E}$ above) does, and thus, in particular, have finite products since we usually require the target category to have at least those. Since $\mathbf{Set}$ has all limits, we immediately have $\mathbf{Grp}$, $\mathbf{Ring}$, $\mathbf{Lattice}$ have all limits. The same logic also works for colimits that commute with finite products, which are called sifted colimits for $\mathbf{Set}$-based categories.
Instead of considering finite product preserving functors, we can consider finite limit preserving functors also called left exact, and everything I've said above goes through with "finite product" replaced with "finite limit". The analogue to sifted colimits is then filtered colimits. Lawvere theories correspond to single-sorted algebraic theories, but multi-sorted algebraic theories are simply represented by arbitrary small categories with finite products, and everything above goes through without change including the generalization to finite limit preserving functors which are called essentially algebraic theories.
