Constructing endofunctors [dt-0050]

Liam O'Connor

If we have a mapping on cpos $\mathcal {F} : \textbf {Cpo} \rightarrow \textbf {Cpo}$ that is made up of the primitives $\times$ , $+$ , $\otimes$ , $\oplus$ , $\mathbf {1}$ and $(\cdot )_\bot$ , we can generate a corresponding morphism mapping on continuous functions $\mathcal {F} : (A\twoheadrightarrow B) \rightarrow (\mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B))$ by using the corresponding morphism mappings of each of these operators. Thus any such mapping can be turned into an endofunctor.

ExampleMaking endofunctors for algebraic data types [dt-0051]

Liam O'Connor

$\begin {array}{llr} \textsf {Object mapping} & \textsf {Morphism mapping}\\[0.2em] \mathcal {F}(X) = X + \mathbf {1} & \mathcal {F}(f) = f + \mathsf {id}_\mathbf {1} & \quad \quad \text {((co)-natural numbers)} \\ \mathcal {F}(X) = \mathbf {1} + (\mathbb {Z}_\bot \times X) & \mathcal {F}(f) = \mathsf {id}_\mathbf {1} + (\mathsf {id}_{\mathbb {Z}_\bot } \times f) & \text {((co)-lists of integers)}\\ \end {array}$

Constructing endofunctors [dt-0050]

ExampleMaking endofunctors for algebraic data types [dt-0051]

Problem.

Categorical Aside. Initiality

Colimits in the category $\mathbf {Cpo}$ [dt-004P]

Definition. $\omega$ -chains of cpos in the category $\mathbf {Cpo}$ [dt-004Q]

Definition. Upper bounds in the category $\mathbf {Cpo}$ [dt-004R]

Definition. Least upper bounds in the category $\mathbf {Cpo}$ [dt-004S]

Definition. Endofunctors on $\textbf {Cpo}$ [dt-004T]

Remark. [dt-004U]

Definition. Cocontinuous endofunctors [dt-004V]

Definition. Fixed points of endofunctors on $\mathbf {Cpo}$ [dt-004W]

Note.

Theorem. Fixed point theorem for endofunctors on $\mathbf {Cpo}$ [dt-004X]

Example. Binary Numbers [dt-004Y]

Exercise. [dt-005M]

Solution.

Constructing endofunctors [dt-0050]

Example. Making endofunctors for algebraic data types [dt-0051]

Exercise. [dt-005N]

Solution.

Solution.

Solution.