Decomposition of completions of reloids ★★

Author(s): Porton

Conjecture   For composable reloids $ f $ and $ g $ it holds
    \item $ \operatorname{Compl} ( g \circ f) = ( \operatorname{Compl} g) \circ f $ if $ f $ is a co-complete reloid; \item $ \operatorname{CoCompl} ( f \circ g) = f \circ \operatorname{CoCompl} g $ if $ f $ is a complete reloid; \item $ \operatorname{CoCompl} ( ( \operatorname{Compl} g) \circ f) = \operatorname{Compl} ( g \circ   ( \operatorname{CoCompl} f)) = ( \operatorname{Compl} g) \circ ( \operatorname{CoCompl} f) $; \item $ \operatorname{Compl} ( g \circ ( \operatorname{Compl} f)) = \operatorname{Compl} ( g \circ   f) $; \item $ \operatorname{CoCompl} ( ( \operatorname{CoCompl} g) \circ f) = \operatorname{CoCompl} ( g   \circ f) $.

Keywords: co-completion; completion; reloid

A construction of direct product in the category of continuous maps between endo-funcoids ★★★

Author(s): Porton

Consider the category of (proximally) continuous maps (entirely defined monovalued functions) between endo-funcoids.

Remind from my book that morphisms $ f: A\rightarrow B $ of this category are defined by the formula $ f\circ A\sqsubseteq B\circ f $ (here and below by abuse of notation I equate functions with corresponding principal funcoids).

Let $ F_0, F_1 $ are endofuncoids,

We define $ F_0\times F_1 = \bigsqcup \left\{ \Phi \in \mathsf{FCD} \,|\, \pi_0 \circ \Phi \sqsubseteq F_0 \circ \pi_0 \wedge \pi_1 \circ \Phi \sqsubseteq F \circ \pi_1 \right\} $

(here $ \pi_0 $ and $ \pi_1 $ are cartesian projections).

Conjecture   The above defines categorical direct product (in the above mentioned category, with products of morphisms the same as in Set).

Keywords: categorical product; direct product