Return to Answer

Where the relevant diagram is the following one.

$$\require{AMScd}\begin{CD} (1+A+A\times A,A \times A) @>>> (1+C+C\times C,C \times C)\\ @V(Zero+Succ+Add,Equ)VV @VV(z+s+a,e)V\\ (A,B) @>(u1,u2)>> (C,D) \end{CD}$$

What if we also want an "equality" function to be part of the algebra? There may be a better approach for this, but we can consider algebras on the category whose objects are pairs of types. An algebra is of the form $F(A,B) \to (A,B)$ for some endofunctor $F$, and in this case, we consider algebras of the form $(1 + A + A \times A, A \times A) \to (A,B)$. The natural numbers ($A$) and the booleans ($B$) endowed with zero $1 \to A$, the successor function $A \to A$, addition $A \times A \to A$, and the equality function $A \times A \to B$ would be an algebra of this form, but not the initial algebra.

What if we also want an "equality" function to be part of the algebra? There may be a better approach for this, but we can consider algebras on the category whose objects are pairs of types. An algebra is of the form $F(A,B) \to (A,B)$ for some endofunctor $F$, and in this case, we consider algebras of the form $(1 + A + A \times A, A \times A) \to (A,B)$. The natural numbers ($A$) and the booleans ($B$) endowed with zero $1 \to A$, the successor function $A \to A$, addition $A \times A \to A$, and the equality function $A \times A \to B$ would be an algebra of this form, but not the initial algebra. I think the initial algebra in this case could be written in Haskell as follows.

-- Initial algebra (where the object is a pair of types!).
data A = Zero | Succ A | Add A A
data B = Equ A A

-- Given any other algebra.
data C
data D
z :: C
s :: C -> C
a :: C -> C -> C
e :: C -> C -> D

-- There is a unique morphism (two morphisms) from the initial
-- algebra making the relevant diagram commute.
u1 :: A -> C
u1 Zero = z
u1 (Succ x) = s (u1 x)
u1 (Add x y) = a (u1 x) (u1 y)

u2 :: B -> D
u2 (Equ x y) = e (u1 x) (u1 y)

What if we also want an "equality" function to be part of the algebra? There may be a better approach for this, but we can consider algebras on the category whose objects are pairs of types. An algebra is of the form $F(A,B) \to (A,B)$ for some endofunctor $F$, and in this case, we consider algebras of the form $(1 + A + A \times A, A \times A) \to (A,B)$. The natural numbers ($A$) and the booleans ($B$) endowed with zero $1 \to A$, the successor function $A \to A$, addition $A \times A \to A$, and the equality function $A \times A \to B$ would be an algebra of this form, but not the initial algebra.