7 added 238 characters in body edited Aug 1 '18 at 20:36 Mario Román 16177 bronze badges 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}$$ 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}$$ 6 added 633 characters in body edited Aug 1 '18 at 20:22 Mario Román 16177 bronze badges 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 anan algebra of this form, but not the initialthe 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. 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)  5 added 616 characters in body edited Aug 1 '18 at 20:01 Mario Román 16177 bronze badges 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. 4 added 55 characters in body edited Aug 1 '18 at 19:40 Mario Román 16177 bronze badges 3 added 177 characters in body edited Aug 1 '18 at 12:17 Mario Román 16177 bronze badges 2 added 331 characters in body edited Aug 1 '18 at 12:10 Mario Román 16177 bronze badges 1 answered Aug 1 '18 at 12:01 Mario Román 16177 bronze badges