reduce<G>

As daunting as specializing reduce to G might seem, it is quite straightforward following the models in the previous two sections. The most difficult portion is getting the type of reduce<G> correct, which we again assert without justificiation:
reduce<G> :: $\gamma$ $\rightarrow$($\gamma$ $\rightarrow$$\gamma$ $\rightarrow$$\gamma$) $\rightarrow$( $\forall \mathcal{F}$. ($\forall \beta$. ($\beta$ $\rightarrow$$\gamma$) $\rightarrow$$\mathcal{F}$ $\beta$ $\rightarrow$$\gamma$) $\rightarrow$( $\forall \alpha$. ($\alpha$ $\rightarrow$$\gamma$) $\rightarrow$G $\mathcal{F}$ $\alpha$ $\rightarrow$$\gamma$))

The isomorphic datatype is even simpler than the previous ones:
data G$^\circ$ $\mathcal{F}$ $\alpha$ = $\alpha$ :*: ($\mathcal{F}$ (G $\mathcal{F}$ $\alpha$))
fromG :: G $\rightarrow$G$^\circ$
fromG (Branch x xg) = x :*: xg
toG :: G$^\circ$ $\rightarrow$G
toG (x :*: xg) = Branch x xg

The specialization proceeds just as before, with two ``new'' arguments:
reduce<G> $c$ $\oplus$ rf ra = (reduce<G$^\circ$> $c$ $\oplus$ rf ra>) o fromG
reduce<G$^\circ$> $c$ $\oplus$ rf ra = red<G$^\circ$>
where
red<G$^\circ$
red<$\alpha$ :*: ($\mathcal{F}$ (G $\mathcal{F}$ $\alpha$))>
red<:*:> red<$\alpha$> red<$\mathcal{F}$ (G $\mathcal{F}$ $\alpha$)>
red<:*:> red<$\alpha$> (red<$\mathcal{F}$> red<G $\mathcal{F}$ $\alpha$>)
red<:*:> red<$\alpha$> (red<$\mathcal{F}$> (red<G> red<$\mathcal{F}$> red<$\alpha$>))
red<:*:> ra (rf (red<G> rf ra))
red<:*:> ra (rf ((reduce<G> $c$ $\oplus$) rf ra))