chap-unfixed.tex

\chapter{Unfixed categories}

\fxwarning{This is a draft not thoroughly checked for
errors.}

\section{Axiomatics for unfixed morphisms}

\begin{defn}
\emph{Category with restricted identities} is defined
axiomatically:

\emph{Restricted identity}~$\id^{\mathcal{C}(A,B)}_X$
and \emph{projection} $A\mapsto[A]$ are
described by the axioms:
\begin{enumerate}
\item $\mathcal{C}$~is a category with the set of
objects~$\mathfrak{Z}$;
\item every $\Hom$-set $\mathcal{C}(A,B)$ is a lattice;
\item $\mathfrak{Z}$~and~$\mathfrak{A}$~are lattices;
\item $A\to[A]$ is a lattice embedding
from $\mathcal{C}(A,B)$ to $\mathfrak{A}$ whenever~$A$
ranges a $\Hom$-set $\mathcal{C}(A,B)$;
\item $\id^{\mathcal{C}(A,B)}_X\in\Hom_{\mathcal{C}}(A,B)$
whenever $\mathfrak{A}\ni X\sqsubseteq [A]\sqcap[B]$;
\item $\id^{\mathcal{C}(A,A)}_{[A]} = 1^{\mathcal{C}}_A$;
\item $\id^{\mathcal{C}(B,C)}_Y \circ \id^{\mathcal{C}(A,B)}_X = \id^{\mathcal{C}(A,C)}_{X\sqcap Y}$;
\item $\forall A\in\mathfrak{A}\exists B\in\mathfrak{Z}:
A\sqsubseteq[B]$.
\end{enumerate}

\fxnote{In a future version of this text the above
definition may be replaced with a more general one.}

For a \emph{partially ordered category with restricted identities} introduce additional axiom $X\sqsubseteq Y\Rightarrow
\id^{\mathcal{C}(A,B)}_X\sqsubseteq\id^{\mathcal{C}(A,B)}_Y$.

For \emph{dagger categories with restricted identities} introduce additional axiom
$\left(\id^{\mathcal{C}(A,B)}_X\right)^\dagger =
\id^{\mathcal{C}(B,A)}_X$.
\end{defn}

\begin{defn}
I call a category with restricted identities
\emph{injective} when the axiom $X\ne Y\Rightarrow
\id^{\mathcal{C}(A,B)}_X\ne\id^{\mathcal{C}(A,B)}_Y$
whenever $X,Y\sqsubseteq[A]\sqcap[B]$ holds.
\end{defn}

\begin{defn}
Define $\mathcal{E}_{\mathcal{C}}^{A,B} =
\id^{\mathcal{C}(A,B)}_{[A]\sqcap[B]}$.
\end{defn}

\begin{prop}\label{e-mono-epi}
  ~  
  \begin{enumerate}
    \item If $[A]\sqsubseteq[B]$ then $\mathcal{E}_{\mathcal{C}}^{A,B}$ is a
    monomorphism.
    
    \item If $[A]\sqsupseteq[B]$ then $\mathcal{E}_{\mathcal{C}}^{A,B}$ is an
    epimorphism.
  \end{enumerate}
\end{prop}

\begin{proof}
  We'll prove only the first as the second is dual.
  
  Let $\mathcal{E}_{\mathcal{C}}^{A,B} \circ f = \mathcal{E}_{\mathcal{C}}^{A,B} \circ g$. Then
  $\mathcal{E}_{\mathcal{C}}^{B,A} \circ \mathcal{E}_{\mathcal{C}}^{A,B}
  \circ f = \mathcal{E}_{\mathcal{C}}^{B,A} \circ \mathcal{E}_{\mathcal{C}}^{A,B} \circ g$;
  $1^A \circ f = 1^A \circ g$; $f = g$.
\end{proof}

\begin{prop}
  $\mathcal{E}_{\mathcal{C}}^{B,C} \circ \mathcal{E}_{\mathcal{C}}^{A,B} = \mathcal{E}_{\mathcal{C}}^{A,C}$
  if $B \sqsupseteq A \sqcap C$ (for every sets $A$, $B$, $C$).
\end{prop}

\begin{proof}
  $\mathcal{E}_{\mathcal{C}}^{B,C} \circ \mathcal{E}_{\mathcal{C}}^{A,B} = \mathcal{E}_{\mathcal{C}}^{A,C}$
  is equivalent to:
  
  $\id^{\mathcal{C}(B,C)}_{B \sqcap C} \circ \id^{\mathcal{C}(A,B)}_{A \sqcap B} = \id^{\mathcal{C}(A,C)}_{A \sqcap C}$ what is obviously true.
\end{proof}

\section{Rectangular embedding-restriction}

\begin{defn}
  $\iota_{B_0, B_1} f = \mathcal{E}_{\mathcal{C}}^{\Dst f,B_1} \circ f \circ
  \mathcal{E}_{\mathcal{C}}^{B_0,\Src f}$ for $f \in
  \Hom_{\mathcal{C}} (A_0 , A_1)$.
\end{defn}

For brevity $\iota_B f = \iota_{B, B} f$.

\begin{obvious}
$\iota_{B_0, B_1} f\sqsubseteq f$.
\end{obvious}

\begin{prop}
  $\iota_{\Src f, \Dst f} f = f$.
\end{prop}

\begin{proof}
  $\iota_{\Src f, \Dst f} f = \mathcal{E}_\mathcal{C}^{\Dst f,\Dst f} \circ f \circ \mathcal{E}_\mathcal{C}^{\Src f,\Src f} =
  1_{\mathcal{C}}^{\Dst f} \circ f \circ 1_{\mathcal{C}}^{\Src f} = f$.
\end{proof}

\begin{prop}
  The function $\iota_{B_0, B_1} |_{f \in \Hom_{\mathcal{C}} (A_0 ,
  A_1)}$ is injective, provided that
  $A_0\sqsubseteq B_0$ and $A_1\sqsubseteq B_1$.
\end{prop}

\begin{proof}
  Because $\mathcal{E}_{\mathcal{C}}^{A_1,B_1}$ is a monomorphism and $\mathcal{E}_{\mathcal{C}}^{A_0,B_0}$ is an epimorphism.
\end{proof}

\begin{cor}\label{iota-emb}
  The function $\iota_{B_0, B_1} |_{f \in \Hom_{\mathcal{C}} (A_0 ,
  A_1)}$ is order embedding if $A_0 \sqsubseteq B_0 \wedge A_1 \sqsubseteq B_1$ for ordered categories
  with restricted identities.
\end{cor}

\section{Image and domain}

Let define that
$\mathscr{S}\mathcal{A}=\setcond{K\in\mathfrak{Z}}{
\exists X\in\mathcal{A}:X\subseteq K}$
holds not only for filters but for any set~$\mathcal{A}$ of
sets.

\begin{obvious}
$\mathscr{S}\mathcal{A}\supseteq\mathcal{A}$.
\end{obvious}

\begin{defn}
~
\begin{enumerate}
\item $\operatorname{IM} f = \setcond{Y \in \mathfrak{Z}}{\mathcal{E}_{\mathcal{C}}^{Y, \Dst f} \circ \mathcal{E}_{\mathcal{C}}^{\Dst f,
Y} \circ f = f} = \setcond{Y \in \mathfrak{Z}}{\id^{\mathcal{C}(\Dst f,\Dst f)}_{[Y]\sqcap[\Dst f]} \circ f = f}$;
\item $\operatorname{DOM} f = \setcond{X \in \mathfrak{Z}}{f\circ\mathcal{E}_{\mathcal{C}}^{\Src f, X} \circ \mathcal{E}_{\mathcal{C}}^{X, \Src f} = f} = \setcond{X \in \mathfrak{Z}}{f \circ \id^{\mathcal{C}(\Src f,\Src f)}_{[X]\sqcap[\Src f]} = f}$.
\end{enumerate}
\end{defn}

\begin{defn}
~
\begin{enumerate}
\item $\operatorname{Im} f = \setcond{Y\in\operatorname{IM} f}{Y\sqsubseteq\Dst f}$;
\item $\operatorname{Dom} f = \setcond{X\in\operatorname{DOM} f}{X\sqsubseteq\Src f}$.
\end{enumerate}
\end{defn}

\begin{prop}
~
\begin{enumerate}
\item $\operatorname{IM} f = \mathscr{S}\operatorname{Im} f$;
\item $\operatorname{DOM} f = \mathscr{S}\operatorname{Dom} f$;
\item $\operatorname{Im} f = \rsupfun{\Dst f\cap}\operatorname{IM} f$;
\item $\operatorname{Dom} f = \rsupfun{\Dst f\cap}\operatorname{DOM} f$.
\end{enumerate}
\end{prop}

\begin{proof}
$\operatorname{IM} f =
\setcond{Y \in \mathfrak{Z}}{\id^{\mathcal{C}(\Dst f,\Dst f)}_{[Y]\sqcap[\Dst f]} \circ f = f}$.

Suppose $Y\in\operatorname{IM}f$. Then take $Y'=Y\sqcap\Dst f$. We have $Y\sqsupseteq Y'$ and $Y'\in\operatorname{Im}f$. So $Y\in\mathscr{S}\operatorname{Im}f$. If $Y\in\mathscr{S}\operatorname{Im}f$ then $Y\in\operatorname{IM}f$ obviously.
So $\operatorname{IM} f = \mathscr{S}\operatorname{Im} f$.

$\rsupfun{\Dst f\cap}\operatorname{IM}f\subseteq
\operatorname{Im}f$ is obvious. If
$\operatorname{Im}f\subseteq\rsupfun{\Dst f\cap}\operatorname{IM}f$ is also obvious.

The rest follows from symmetry.
\end{proof}

\begin{conjecture}
$\operatorname{Im} f$ may be not a filter for an injective
category with restricted morphisms.
\end{conjecture}

\begin{prop}\label{dst-in-im}
$\Dst f\in\operatorname{Im} f$; $\Src f\in\operatorname{Dom} f$ for every morphism~$f$ of a category with restricted
identities.
\end{prop}

\begin{proof}
Prove $\Dst f\in\operatorname{Im} f$ (the other is similar):
We need to prove that $\mathcal{E}_{\mathcal{C}}^{\Dst f, \Dst f} \circ \mathcal{E}_{\mathcal{C}}^{\Dst f,
\Dst f} \circ f = f$ what follows from
$\mathcal{E}_{\mathcal{C}}^{\Dst f, \Dst f} \circ \mathcal{E}_{\mathcal{C}}^{\Dst f, \Dst f} = 1^{\Dst f}$.
\end{proof}

\begin{prop}
$\operatorname{IM}f$, $\operatorname{Im}f$,
$\operatorname{DOM}f$, $\operatorname{Dom}f$
are upper sets.
\end{prop}

\begin{proof}
For $\operatorname{Im}f$, $\operatorname{Dom}f$ it follows
from the previous proposition.

For $\operatorname{IM}f$, $\operatorname{DOM}f$ it follows
from the thesis for
$\operatorname{Im}f$, $\operatorname{Dom}f$.
\end{proof}

\begin{defn}
~
\begin{enumerate}
\item An ordered category with restricted identities is
\emph{with ordered image} iff $f\sqsubseteq g\Rightarrow
\operatorname{IM}f\subseteq\operatorname{IM}g$.
\item An ordered category with restricted identities is
\emph{with ordered domain} iff $f\sqsubseteq g\Rightarrow
\operatorname{DOM}f\subseteq\operatorname{DOM}g$.
\item An ordered category with restricted identities is
\emph{with ordered domain and image} iff it is both
with ordered domain and with ordered image.
\end{enumerate}
\end{defn}

\begin{obvious}
~
\begin{enumerate}
\item An ordered category with restricted identities is
with ordered image iff $f\sqsubseteq g\Rightarrow
\operatorname{Im}f\subseteq\operatorname{Im}g$.
\item An ordered category with restricted identities is
with ordered domain iff $f\sqsubseteq g\Rightarrow
\operatorname{Dom}f\subseteq\operatorname{Dom}g$.
\item An ordered category with restricted identities is
with ordered domain and image iff it is both
with ordered domain and with ordered image.
\end{enumerate}
\end{obvious}

\begin{obvious}
~
\begin{enumerate}
\item For an ordered category~$\mathcal{C}$ with restricted identities
to be with ordered image it's enough that
$\id^{\mathcal{C}(\Dst f,\Dst f)}_{[X]}\circ f=f\land
g\sqsubseteq f\Rightarrow
\id^{\mathcal{C}(\Dst f,\Dst f)}_{[X]}\circ g=g$
for every parallel morphisms~$f$ and $g$ and
$\mathfrak{Z}\ni X\sqsubseteq\Dst f$.
\item For an ordered category~$\mathcal{C}$ with restricted identities
to be with ordered domain it's enough that
$f\circ\id^{\mathcal{C}(\Src f,\Src f)}_{[X]}=f\land
g\sqsubseteq f\Rightarrow
g\circ\id^{\mathcal{C}(\Src f,\Src f)}_{[X]}=g$
for every parallel morphisms~$f$ and $g$ and
$\mathfrak{Z}\ni X\sqsubseteq\Src f$.
\end{enumerate}
\end{obvious}

\begin{conjecture}
There exists a category with restricted identities which
is not with ordered image.
\end{conjecture}

\begin{obvious}
For an ordered category with restricted identities with
ordered domain and image we have
$\iota_{\Src f,\Dst f}\iota_{A,B}f=f\land g\sqsubseteq f
\Rightarrow
\iota_{\Src f,\Dst f}\iota_{A,B}g=g$
for parallel morphisms~$f$ and~$g$.
\end{obvious}

\begin{defn}
~
\begin{enumerate}
\item $\im f = \min\operatorname{Im} f$;
\item $\dom f = \min\operatorname{Dom} f$.
\end{enumerate}
\end{defn}

\begin{note}
It seems that $\im$ and $\dom$ are defined not for every
category with restricted identities.
\end{note}

\begin{prop}
~
\begin{enumerate}
\item $\im f = \min\operatorname{IM} f$;
\item $\dom f = \min\operatorname{DOM} f$.
\end{enumerate}
\end{prop}

\begin{proof}
It follows from $\operatorname{IM}f=\mathscr{S}\operatorname{Im}f$
(and likewise for~$\dom f$).
\end{proof}

\section{Equivalent morphisms}

\begin{prop}\label{two-iotas}
  $\iota_{A, B} \iota_{X, Y} f = \iota_{A, B} f$ for every sets $A$, $B$, $X$,
  $Y$ whenever $\operatorname{DOM} f$ and $\operatorname{IM} f$ are filters and $X \in
  \operatorname{DOM} f$, $Y \in \operatorname{IM} f$.
\end{prop}

\begin{proof}
  $\iota_{A, B} f =\mathcal{E}_{\mathcal{C}}^{\Dst f, B} \circ f \circ
  \mathcal{E}_{\mathcal{C}}^{A, \Src f} = \text{(by definition of
  $\operatorname{IM} f$ and $\operatorname{DOM} f$)} =\mathcal{E}_{\mathcal{C}}^{\Dst f,
  B} \circ \mathcal{E}_{\mathcal{C}}^{Y, \Dst f} \circ
  \mathcal{E}_{\mathcal{C}}^{\Dst f, Y} \circ f \circ
  \mathcal{E}_{\mathcal{C}}^{X, \Src f} \circ
  \mathcal{E}_{\mathcal{C}}^{\Src f, X} \circ
  \mathcal{E}_{\mathcal{C}}^{A, \Src f} =\mathcal{E}_{\mathcal{C}}^{Y,
  B} \circ \mathcal{E}_{\mathcal{C}}^{\Dst f, Y} \circ f \circ
  \mathcal{E}_{\mathcal{C}}^{X, \Src f} \circ
  \mathcal{E}_{\mathcal{C}}^{A, X} = \iota_{A, B} \iota_{X, Y} f$
  
  because $\mathcal{E}^{\Dst f, B} \circ \mathcal{E}^{Y, \Dst f}
  \circ \mathcal{E}^{\Dst f, Y} = \id^{\mathcal{C}(\Dst f, B)}_{Y \sqcap
  \Dst f \sqcap B} = \id^{\mathcal{C}(Y, B)}_{Y \sqcap B} \circ \id^{\mathcal{C}(\Dst f,Y)}_{Y \sqcap \Dst f} = \mathcal{E}^{Y, B} \circ
  \mathcal{E}^{\Dst f, Y}$ and thus
  $\mathcal{E}_{\mathcal{C}}^{\Dst f, B} \circ
  \mathcal{E}_{\mathcal{C}}^{Y, \Dst f} \circ
  \mathcal{E}_{\mathcal{C}}^{\Dst f, Y} =\mathcal{E}_{\mathcal{C}}^{Y,
  B} \circ \mathcal{E}_{\mathcal{C}}^{\Dst f, Y}$ and similarly for
  $\mathcal{E}_{\mathcal{C}}^{X, \Src f} \circ
  \mathcal{E}_{\mathcal{C}}^{\Src f, X} \circ
  \mathcal{E}_{\mathcal{C}}^{A, \Src f}$.
\end{proof}

\begin{defn}
I call two morphisms $f\in\mathcal{C}(A_0,B_0)$ and
$g\in\mathcal{C}(A_1,B_1)$
of a category with restricted morphisms \emph{equivalent}
(and denote $f\sim g$) when
\[\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g.\]
\end{defn}

\begin{prop}
$f\sim g$~iff $\iota_{A,B}f=\iota_{A,B}g$ for
some~$A\in\operatorname{DOM}f\cap\operatorname{DOM}g$,~$B\in\operatorname{IM}f\cap\operatorname{IM}g$.
\end{prop}

\begin{proof}
Both
\[\iota_{A,B}f=\iota_{A,B}g\Rightarrow
\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g\]
and
\[\iota_{A,B}f=\iota_{A,B}g\Leftarrow
\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g\]
follow from proposition~\ref{two-iotas}.
\end{proof}

\begin{thm}\label{uf-sim-cond}
Let
$f:A_0\to B_0$~and~$g:A_1\to B_1$
(for a partially ordered category with restricted identities).
The following are pairwise equivalent:
\begin{enumerate}
\item\label{uf-sim-cond-sim} $f\sim g$;
\item\label{uf-sim-cond-eq} $\iota_{A_1,B_1}f=g$ and $\iota_{A_0,B_0}g=f$;
\item\label{uf-sim-cond-sb} $\iota_{A_1,B_1}f\sqsupseteq g$ and $\iota_{A_0,B_0}g\sqsupseteq f$.
\end{enumerate}
\end{thm}

\begin{proof}
~
\begin{description}
\item[\ref{uf-sim-cond-sim}$\Rightarrow$\ref{uf-sim-cond-eq}]
$\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g$;
$\iota_{A_1,B_1}\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_1,B_1}\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g$;
$\iota_{A_1,B_1}f=\iota_{A_1,B_1}g$;
$\iota_{A_1,B_1}f=g$. $\iota_{A_0,B_0}g=f$ is similar.

\item[\ref{uf-sim-cond-sb}$\Rightarrow$\ref{uf-sim-cond-sim}]
Let $\iota_{A_1, B_1} f \sqsupseteq g$ and $\iota_{A_0, B_0} g \sqsupseteq f$.

$\iota_{A_1, B_1} \iota_{A_0, B_0} g \sqsupseteq g$;

$\mathcal{E}^{B_0, B_1} \circ \mathcal{E}^{B_1, B_0} \circ g \circ
\mathcal{E}^{A_0, A_1} \circ \mathcal{E}^{A_1, A_0}\sqsupseteq g$;

$\id^{\mathcal{C} (B_1, B_1)}_{[B_0]\sqcap[B_1]} \circ g \circ
\id^{\mathcal{C} (A_1, A_1)}_{[A_0]\sqcap[A_1]} \sqsupseteq g$;
$\id^{\mathcal{C} (B_1, B_1)}_{[B_0]\sqcap[B_1]} \circ g \sqsupseteq g$;
$\id^{\mathcal{C} (B_1, B_1)}_{[B_0]\sqcap[B_1]} \circ g = g$;

$\id^{\mathcal{C} (B_0 \sqcap B_1, B_1)}_{[B_0]\sqcap[B_1]} \circ
\id^{\mathcal{C} (B_1, B_0 \sqcap B_1)}_{[B_0]\sqcap[B_1]} \circ g = g$;
$\mathcal{E}^{B_0 \sqcap B_1, B_1} \circ \mathcal{E}^{B_1, B_0 \sqcap B_1}
\circ g = g$. Thus $B_0 \sqcap B_1 \in \operatorname{Im} g$. Similarly $A_0 \sqcap A_1
\in \operatorname{Dom} g$.

So $\iota_{A_0 \sqcup A_1, B_0 \sqcup B_1} f = \iota_{A_0 \sqcup A_1, B_0
\sqcup B_1} \iota_{A_0, B_0} g = \iota_{A_0 \sqcup A_1, B_0 \sqcup B_1} g$.

\item[\ref{uf-sim-cond-eq}$\Rightarrow$\ref{uf-sim-cond-sb}]
Obvious.
\end{description}
\end{proof}

\begin{prop}
Above defined equivalence of morphisms (for a small category)
is an equivalence relation.
\end{prop}

\begin{proof}
~
\begin{description}
\item[Reflexivity] Obvious.

\item[Symmetry] Obvious.

\item[Transitivity] Let $f\sim g$ and $g\sim h$ for
$f:A_0\to B_0$, $g:A_1\to B_1$, $h:A_2\to B_2$.
Then
$\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g$ and
$\iota_{A_1\sqcup A_2,B_1\sqcup B_2}g=\iota_{A_1\sqcup A_2,B_1\sqcup B_2}h$.

Thus
\[\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f=\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}\iota_{A_0\sqcup A_1,B_0\sqcup B_1}g\] and
\[\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}\iota_{A_1\sqcup A_2,B_1\sqcup B_2}g=\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}\iota_{A_1\sqcup A_2,B_1\sqcup B_2}h\]
that is (proposition~\ref{two-iotas})
\[\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}f=\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}g\]
and
\[\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}g=\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}h.\]
Combining,
$\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}f=\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}h$ and thus
\[\iota_{A_0\sqcup A_2,B_0\sqcup B_2}\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}f=\iota_{A_0\sqcup A_2,B_0\sqcup B_2}\iota_{A_0\sqcup A_1\sqcup A_2,B_0\sqcup B_1\sqcup B_2}h;\]
(again proposition~\ref{two-iotas}) $\iota_{A_0\sqcup A_2,B_0\sqcup B_2}f=\iota_{A_0\sqcup A_2,B_0\sqcup B_2}h$
that is $f\sim h$.
\end{description}
\end{proof}

\begin{prop}
$[f] = \setcond{\iota_{A,B}f}{
A\in\operatorname{DOM}f,B\in\operatorname{IM}f}$.
\end{prop}

\begin{proof}
If~$A\in\operatorname{DOM}f$,~$B\in\operatorname{IM}f$
then
\[\iota_{A\sqcup\Src f,B\sqcup\Dst f}\iota_{A,B}f =
\iota_{A\sqcup\Src f,B\sqcup\Dst f}f.\] Thus
$\iota_{A,B}f\sim f$ that is $\iota_{A,B}f\in[f]$.

Let now $g\in[f]$ that is $f\sim g$;
\[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}f=
\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}g.\]
Take $A=\Src g$, $B=\Dst g$. We have
\begin{gather*}
\iota_{A,B}\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}f=
\iota_{A,B}\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}g;\\
\iota_{A,B}f=\iota_{A,B}g = g.
\end{gather*}
\end{proof}

\begin{prop}
~
\begin{enumerate}
\item $\operatorname{IM} f = \setcond{Y \in \mathfrak{Z}}{
  \mathcal{E}_{\mathcal{C}}^{\Dst f, Y} \circ f \sim f}$;
\item $\operatorname{DOM} f = \setcond{X \in \mathfrak{Z}}{
  f\circ\mathcal{E}_{\mathcal{C}}^{X, \Src f} \sim f}$.
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{multline*}
\mathcal{E}_{\mathcal{C}}^{\Dst f, Y} \circ f \sim f
\Leftrightarrow
\iota_{\Src f,Y\sqcup\Dst f}
(\mathcal{E}_{\mathcal{C}}^{\Dst f, Y} \circ f) =
\iota_{\Src f,Y\sqcup\Dst f}f \Leftrightarrow \\
\mathcal{E}^{Y,Y\sqcup\Dst f}\circ\mathcal{E}^{\Dst f, Y} \circ f \circ \mathcal{E}^{\Src f,\Src f} =
\mathcal{E}^{\Dst f,Y\sqcup\Dst f}\circ f\circ\mathcal{E}^{\Src f,\Src f} \Leftrightarrow \\
\mathcal{E}^{Y,Y\sqcup\Dst f}\circ\mathcal{E}^{\Dst f, Y}\circ f=\mathcal{E}^{\Dst f,Y\sqcup\Dst f}\circ f
\Leftrightarrow \text{(proposition~\ref{e-mono-epi})} \\ \Leftrightarrow
\mathcal{E}^{Y\sqcup\Dst f,\Dst f}\circ \mathcal{E}^{Y,Y\sqcup\Dst f}\circ\mathcal{E}^{\Dst f, Y}\circ f=\mathcal{E}^{Y\sqcup\Dst f,\Dst f}\circ \mathcal{E}^{\Dst f,Y\sqcup\Dst f}\circ f \Leftrightarrow \\
\mathcal{E}^{Y,\Dst f}\circ\mathcal{E}^{\Dst f,Y}\circ f = f.
\end{multline*}
From this our thesis follows obviously.
\end{proof}

\begin{prop}\label{iota-less}
$\iota_{A_1,B_1}\iota_{A_0,B_0}f\sqsubseteq\iota_{A_1,B_1}f$.
\end{prop}

\begin{proof}
$\iota_{A_1,B_1}\iota_{A_0,B_0}f=
\mathcal{E}^{B_0,B_1}\circ\mathcal{E}^{\Dst f,B_0}\circ f\circ
\mathcal{E}^{A_0,\Src f}\circ\mathcal{E}^{A_1,A_0}=
\id^{\mathcal{C}(B_0,B_1)}_{[B_0]\sqcap[B_1]}\circ\id^{\mathcal{C}(\Dst f,B_0)}_{[\Dst f]\sqcap[B_0]}
\circ f\circ
\id^{\mathcal{C}(A_0,\Src f)}_{[A_0]\sqcap[\Src f]}\circ
\id^{\mathcal{C}(A_1,A_0)}_{[A_1]\sqcap[A_0]}=
\id^{\mathcal{C}(\Dst f,B_1)}_{[\Dst f]\sqcap[B_0]\sqcap[B_1]}
\circ f\circ
\id^{\mathcal{C}(A_1,\Src f)}_{[A_0]\sqcap[A_1]\sqcap[\Src f]}
\sqsubseteq
\id^{\mathcal{C}(\Dst f,B_1)}_{[\Dst f]\sqcap[B_1]}
\circ f\circ
\id^{\mathcal{C}(A_1,\Src f)}_{[A_1]\sqcap[\Src f]}=
\iota_{A_1,B_1}f$.
\end{proof}

\section{Binary product}

\begin{defn}
The category \emph{with binary product morphism}
is a category with restricted identities and additional axioms
\begin{enumerate}
\item $\id^{\mathcal{C}(B,B)}_Y\circ f\circ\id^{\mathcal{C}(A,A)}_X=f\sqcap(X\times_{A,B}Y)$
(holding for every $A,B\in\mathfrak{Z}$,
$\mathfrak{A}\ni X\sqsubseteq[A]$,
$\mathfrak{A}\ni Y\sqsubseteq[B]$,
$X\times_{A,B}Y\in\mathcal{C}(A,B)$
and morphism~$f\in\mathcal{C}(A,B)$);
\item $\iota_{A_1,B_1}(X\times_{A_0,B_0}Y)=
X\times_{A_1,B_1}Y$ whenever
$X\sqsubseteq[A_0]\sqcap[A_1]$ and $Y\sqsubseteq[B_0]\sqcap[B_1]$.
\end{enumerate}
\end{defn}

\begin{prop}
$[A]\times_{A,B}[B]$ is the greatest morphism
$\top^{\mathcal{C}(A,B)}:A\to B$.
\end{prop}

\begin{proof}
It's enough to prove $f\sqcap([A]\times_{A,B}[B])=f$ for every
$f:A\to B$. Really,
$f\sqcap([A]\times_{A,B}[B])=
\id^{\mathcal{C}(B,B)}_B\circ f\circ\id^{\mathcal{C}(A,A)}_A=
1^B\circ f\circ 1^A=f$.
\end{proof}

\begin{prop}
For every category with binary product morphism
\[X\times_{A,B}Y=
\id^{\mathcal{C}(B,B)}_Y\circ\top^{\mathcal{C}(A,B)}\circ
\id^{\mathcal{C}(A,A)}_X\]
\end{prop}

\begin{proof}
$X\times_{A,B}Y\sqsupseteq
\id^{\mathcal{C}(B,B)}_Y\circ\top^{\mathcal{C}(A,B)}\circ\id^{\mathcal{C}(A,A)}_X$
because
$\id^{\mathcal{C}(B,B)}_Y\circ\top^{\mathcal{C}(A,B)}\circ\id^{\mathcal{C}(A,A)}_X=
\top^{\mathcal{C}(A,B)}\sqcap(X\times_{A,B}Y)$.

$\id^{\mathcal{C}(B,B)}_Y\circ\top^{\mathcal{C}(A,B)}\circ\id^{\mathcal{C}(A,A)}_X\sqsupseteq
\id^{\mathcal{C}(B,B)}_Y\circ(X\times_{A,B}Y)\circ
\id^{\mathcal{C}(A,A)}_X=
(X\times_{A,B}Y)\sqcap(X\times_{A,B}Y)=X\times_{A,B}Y$.
\end{proof}

\begin{prop}
$\iota_{A,B}(f\sqcap g)=\iota_{A,B}f\sqcap\iota_{A,B}g$
for every parallel morphisms~$f$ and~$g$ and objects~$A$
and~$B$, whenever all $\mathcal{E}^{X,Y}$ are metamonovalued
and metainjective.
\end{prop}

\begin{proof}
$\iota_{A,B}(f\sqcap g)=
\mathcal{E}^{\Dst f,B}\circ(f\sqcap g)\circ
\mathcal{E}^{A,\Src f}=
(\mathcal{E}^{\Dst f,B}\circ f\circ\mathcal{E}^{A,\Src f})\sqcap
(\mathcal{E}^{\Dst f,B}\circ g\circ\mathcal{E}^{A,\Src f})=
\iota_{A,B}f\sqcap\iota_{A,B}g$.
\end{proof}

\begin{prop}
$(X_0\times_{A,B}Y_0)\sqcap(X_1\times_{A,B}Y_1)=
(X_0\sqcap X_1)\times_{A,B}(Y_0\sqcap Y_1)$.
\end{prop}

\begin{proof}
$(X_0\times_{A,B}Y_0)\sqcap(X_1\times_{A,B}Y_1)=
\id^{\mathcal{C}(B,B)}_{Y_1}\circ(X_0\times_{A,B}Y_0)\circ
\id^{\mathcal{C}(A,A)}_{X_1}=
\id^{\mathcal{C}(B,B)}_{Y_1}\circ
\id^{\mathcal{C}(B,B)}_{Y_0}\circ
\top^{\mathcal{C}(A,B)}\circ
\id^{\mathcal{C}(A,A)}_{X_1}\circ
\id^{\mathcal{C}(A,A)}_{X_0}=
\id^{\mathcal{C}(B,B)}_{Y_0\sqcap Y_1}\circ
\top^{\mathcal{C}(A,B)}\circ
\id^{\mathcal{C}(A,A)}_{X_0\sqcap X_1}=
(X_0\sqcap X_1)\times_{A,B}(Y_0\sqcap Y_1)$.
\end{proof}

\begin{prop}
For a category with binary product morphism
$\operatorname{Im}f$, $\operatorname{Dom}f$,
$\operatorname{IM}f$, and $\operatorname{DOM}f$
are filters.
\end{prop}

\begin{proof}
That they are upper sets was proved above.

To prove that $\operatorname{Im} f$ is a filter it remains
to show $A, B \in \operatorname{Im} f \Leftrightarrow
A \sqcap B \in \operatorname{Im} f$. Really,
$A, B \in \operatorname{Im} f \Leftrightarrow \top \times A \sqsupseteq f \land \top
\times B \sqsupseteq f \Rightarrow \top \times (A \sqcap B) \sqsupseteq f
\Leftrightarrow A \sqcap B \in \operatorname{Im} f$.

$\operatorname{Dom} f$ is similar.

The thesis for~$\operatorname{IM}f$,~$\operatorname{DOM}f$
follows from above proved
for~$\operatorname{Im}f$,~$\operatorname{Dom}f$.
\end{proof}

\begin{note}
For example for below defined category of funcoids
(with binary product morphism), these filters are filters
on filters on sets not filters of sets and thus are not
the same as~$\im$ and~$\dom$.
\end{note}

\section{Operations on the set of unfixed morphisms}

\subsection{Semigroup of unfixed morphisms}

\begin{prop}\label{iota-comp}
  Let $f : A_0 \rightarrow A_1$ and $g : A_1 \rightarrow A_2$ and $A_1
  \sqsubseteq B_1$. Then $\iota_{B_0, B_2} (g \circ f) = \iota_{B_1, B_2} g
  \circ \iota_{B_0, B_1} f$.
\end{prop}

\begin{proof}
  $\iota_{B_0, B_2} (g \circ f) = \mathcal{E}_{\mathcal{C}}^{A_2,B_2}
  \circ g \circ f \circ \mathcal{E}_{\mathcal{C}}^{B_0,A_0} = \mathcal{E}_{\mathcal{C}}^{A_2,B_2} \circ g \circ 1^{A_1} \circ f
  \circ \mathcal{E}_{\mathcal{C}}^{B_0,A_0} = \mathcal{E}_{\mathcal{C}}^{A_2,B_2} \circ g \circ \id^{\mathcal{C}(\Dst f,\Src g)}_{A_1} \circ f
  \circ \mathcal{E}_{\mathcal{C}}^{B_0,A_0} = \mathcal{E}_{\mathcal{C}}^{A_2,B_2} \circ g \circ \mathcal{E}^{B_1,A_1}
  \circ \mathcal{E}^{A_1,B_1} \circ f \circ \mathcal{E}_{\mathcal{C}}^{B_0,A_0} = \iota_{B_1, B_2} g \circ \iota_{B_0,
  B_1} f$.
\end{proof}

\begin{defn}
We will turn the category~$\mathcal{C}$ into a semigroup
$\mathcal{U}\mathcal{C}$
(\emph{the semigroup of unfixed morphisms}) by
the formula $[g]\circ[f] = [g\circ f]$ whenever~$f$ and~$g$
are composable morphisms.
\end{defn}

We need to prove that $[g]\circ[f]$ does not depend on
choice of~$f$ and~$g$ (provided that~$f$ and~$g$
are composable). We also need to prove that $[g]\circ[f]$
is always defined for every morphisms (not necessarily
composable)~$f$ and~$g$. That the resulting structure is
a semigroup (that is,~$\circ$ is associative) is then
obvious.

\begin{proof}
That $[g]\circ[f]$ is defined in at least one way for every
morphisms~$f$ and~$g$ is simple to prove. Just consider the
morphisms
$f'=\iota_{\Src f,\Dst f\sqcup\Src g}f\sim f$ and
$g'=\iota_{\Dst f\sqcup\Src g,\Dst g}g\sim g$.
Then we can take $[g]\circ[f]=[g'\circ f']$.

It remains to prove that $[g]\circ[f]$ does not depend on
choice of~$f$ and~$g$. Really, take arbitrary composable
pairs of morphisms $(f_0:A_0\to B_0,g_0:B_0\to C_0)$ and
$(f_1:A_1\to B_1,g_1:B_1\to C_1)$ such that
$f_0\sim f_1$ and $g_0\sim g_1$. It remains to prove that
$g_0\circ f_0\sim g_1\circ f_1$.
We have
\begin{multline*}
\iota_{B_0\sqcup B_1,C_0\sqcup C_1}g_0 \circ
\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f_0
= \text{(proposition~\ref{iota-comp})} = \\
\mathcal{E}_{\mathcal{C}}^{C_0,C_0\sqcup C_1}\circ g_0 \circ
f_0\circ\mathcal{E}_{\mathcal{C}}^{A_0\sqcup A_1,B_0} =
\iota_{A_0\sqcup A_1,C_0\sqcup C_1}(g_0\circ f_0).
\end{multline*}
Similarly
\[\iota_{B_0\sqcup B_1,C_0\sqcup C_1}g_1 \circ
\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f_1 =
\iota_{A_0\sqcup A_1,C_0\sqcup C_1}(g_1\circ f_1).\]

But
\[\iota_{B_0\sqcup B_1,C_0\sqcup C_1}g_0 \circ
\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f_0 =
\iota_{B_0\sqcup B_1,C_0\sqcup C_1}g_1 \circ
\iota_{A_0\sqcup A_1,B_0\sqcup B_1}f_1\]
thus having
$\iota_{A_0\sqcup A_1,C_0\sqcup C_1}(g_0\circ f_0) =
\iota_{A_0\sqcup A_1,C_0\sqcup C_1}(g_1\circ f_1)$ and so
$g_0\circ f_0\sim g_1\circ f_1$.
\end{proof}

\subsection{Restricted identities}

\begin{defn}
\emph{Restricted identity} for unfixed morphisms is
defined as: $\id_X = [\id^{\mathcal{C}(A,B)}_X]$ for
an $X\sqsubseteq[A]\sqcap[B]$.
\end{defn}

We need to prove that it does not depend on the choice
of~$A$ and~$B$.

\begin{proof}
Let $\mathfrak{A}\ni X\sqsubseteq[A_0]\sqcap[B_0]$ and
$\mathfrak{A}\ni X\sqsubseteq[A_1]\sqcap[B_1]$ for
$A_0,B_0,A_1,B_1\in\mathfrak{Z}$. We need to prove
$\id^{\mathcal{C}(A_0,B_0)}_X\sim
\id^{\mathcal{C}(A_1,B_1)}_X$.

Really, $\iota_{A_1,B_1}\id^{\mathcal{C}(A_0,B_0)}_X =
\mathcal{E}^{B_0,B_1}\circ\id^{\mathcal{C}(A_0,B_0)}_X
\circ \mathcal{E}^{A_1,A_0} =
\id^{\mathcal{C}(B_0,B_1)}_{[B_0]\sqcap[B_1]}\circ
\id^{\mathcal{C}(A_0,B_0)}_X\circ
\id^{\mathcal{C}(A_1,A_0)}_{[A_0]\sqcap[A_1]} =
\id^{\mathcal{C}(A_1,B_1)}_{[A_0]\sqcap[A_1]\sqcap[B_0]\sqcap[B_1]\sqcap X} =
\id^{\mathcal{C}(A_1,B_1)}_X$.
Similarly
$\iota_{A_0,B_0}\id^{\mathcal{C}(A_1,B_1)}_X =
\id^{\mathcal{C}(A_0,B_0)}_X$.

So $\id^{\mathcal{C}(A_0,B_0)}_X\sim
\id^{\mathcal{C}(A_1,B_1)}_X$.
\end{proof}

\begin{prop}
$\id_Y\circ\id_X=\id_{X\sqcap Y}$ for
every~$X,Y\in\mathfrak{A}$.
\end{prop}

\begin{proof}
Take arbitrary $\id^{\mathcal{C}(A,B_0)}_X\in\id_X$ and
$\id^{\mathcal{C}(B_1,C)}_Y\in\id_Y$.

Obviously,
$\id^{\mathcal{C}(A,B_0\sqcup B_1)}_X\in\id_X$ and
$\id^{\mathcal{C}(B_0\sqcup B_1,C)}_Y\in\id_Y$.
Thus
$\id_Y\circ\id_X=
[\id^{\mathcal{C}(B_0\sqcup B_1,C)}_Y]\circ
[\id^{\mathcal{C}(A,B_0\sqcup B_1)}_X]=
[\id^{\mathcal{C}(A,C)}_{X\sqcap Y}]=
\id_{X\sqcap Y}$.
\end{proof}

\subsection{Poset of unfixed morphisms}

\begin{lem}
$f\sqsubseteq g\Rightarrow
\iota_{A,B}f\sqsubseteq\iota_{A,B}g$ for every
morphisms~$f$ and~$g$ such that
$\Src f=\Src g$ and $\Dst f=\Dst g$.
\end{lem}

\begin{proof}
$\iota_{A,B}f\sqsubseteq\iota_{A,B}g \Leftrightarrow
\mathcal{E}^{\Dst f,B}\circ f\circ\mathcal{E}^{A,\Src f}
\sqsubseteq
\mathcal{E}^{\Dst g,B}\circ g\circ\mathcal{E}^{A,\Src g}
\Leftrightarrow
\id^{\mathcal{C}(\Dst f,B)}_{[B]\sqcap[\Dst f]}\circ f\circ\id^{\mathcal{C}(A,\Src f)}_{[A]\sqcap[\Src f]}
\sqsubseteq
\id^{\mathcal{C}(\Dst g,B)}_{[B]\sqcap[\Dst g]}\circ g\circ\id^{\mathcal{C}(A,\Src g)}_{[A]\sqcap[\Src g]}
\Leftarrow f\sqsubseteq g$ because
$\id^{\mathcal{C}(\Dst f,B)}_{[B]\sqcap[\Dst f]}=
\id^{\mathcal{C}(\Dst g,B)}_{[B]\sqcap[\Dst g]}$ and
$\id^{\mathcal{C}(A,\Src f)}_{[A]\sqcap[\Src f]}=
\id^{\mathcal{C}(A,\Src g)}_{[A]\sqcap[\Src g]}$.
\end{proof}

\begin{cor}\label{unxif-org-cong}
~
\begin{enumerate}
\item\label{unxif-org-cong-impl}
$f_0\sqsubseteq g_0\land f_0\sim f_1\land g_0\sim g_1
\Rightarrow f_1\sqsubseteq g_1$ whenever
$\Src f_0=\Src g_0$ and $\Dst f_0=\Dst g_0$ and
$\Src f_1=\Src g_1$ and $\Dst f_1=\Dst g_1$.
\item\label{unxif-org-cong-eq}
$f_0\sqsubseteq g_0\Leftrightarrow f_1\sqsubseteq g_1$ whenever
$\Src f_0=\Src g_0$ and $\Dst f_0=\Dst g_0$ and
$\Src f_1=\Src g_1$ and $\Dst f_1=\Dst g_1$ and
$f_0\sim f_1\land g_0\sim g_1$.
\end{enumerate}
\end{cor}

\begin{proof}
~
\begin{disorder}
\item[\ref{unxif-org-cong-impl}] Because
$f_1=\iota_{\Src f_1,\Dst f_1}f_0$ and
$g_1=\iota_{\Src g_1,\Dst g_1}f_0$.
\item[\ref{unxif-org-cong-eq}] A consequence of the
previous.
\end{disorder}
\end{proof}

The above corollary warrants validity of the following
definition:

\begin{defn}
The order on the set of unfixed morphisms is defined
by the formula
$[f]\sqsubseteq[g]\Leftrightarrow f\sqsubseteq g$
whenever $\Src f=\Src g\land\Dst f=\Dst g$.
\end{defn}

It is really an order:

\begin{proof}
~
\begin{description}
\item[Reflexivity] Obvious.
\item[Transitivity] Obvious.
\item[Antisymmetry] Let $[f]\sqsubseteq[g]$ and
$[g]\sqsubseteq[f]$ and $\Src f=\Src g\land\Dst f=\Dst g$.
Then $f\sqsubseteq g$ and $g\sqsubseteq f$ and thus
$f=g$ so having $[f]=[g]$.
\end{description}
\end{proof}

\begin{obvious}\label{unfix-mor-emb}
$f\mapsto[f]$ is an order embedding from the set
$\mathcal{C}(A,B)$ to unfixed morphisms, for every
objects~$A$,~$B$.
\end{obvious}

\begin{prop}\label{cmpl-lat-par}
If $S$ is a set of parallel morphisms of a partially ordered
category with an equivalence relation respecting the order, then
\begin{enumerate}
\item\label{cmpl-lat-par-cap}
$\bigsqcap_{X\in S}[X]$ exists and 
$\bigsqcap_{X\in S}[X]=[\bigsqcap S]$;

\item\label{cmpl-lat-par-cup}
$\bigsqcup_{X\in S}[X]$ exists and 
$\bigsqcup_{X\in S}[X]=[\bigsqcup S]$.
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{widedisorder}
\item[\ref{cmpl-lat-par-cap}]
$[\bigsqcap S]\sqsubseteq[X]$ for every~$X\in S$ because
$\bigsqcap S\sqsubseteq X$.

Let now $L\sqsubseteq[X]$ for every~$X\in S$ for an
equivalence class~$L$. Then $L\sqsubseteq[\bigsqcap S]$
because $l\sqsubseteq\bigsqcap S$ for~$l\in L$ because
$l\sqsubseteq X$ for every~$X\in S$.

Thus $[\bigsqcap S]$ is the greatest lower bound of
$\setcond{[X]}{X\in S}$.

\item[\ref{cmpl-lat-par-cup}] By duality.
\end{widedisorder}
\end{proof}

\begin{prop}
~
\begin{enumerate}
\item If every $\Hom$-set is a join-semilattice, then
the poset of unfixed morphism is a join-semilattice.
\item If every $\Hom$-set is a join-semilattice, then
the poset of unfixed morphism is a meet-semilattice.
\end{enumerate}
\end{prop}

\begin{proof}
Let~$f$ and~$g$ be arbitrary morphisms.
\begin{multline*}
[f]\sqcup[g] =
[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}f]\sqcup
[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}g] = \\
\text{(obvious~\ref{unfix-mor-emb})} =
[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}f\sqcup
\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}g]
\end{multline*}
and
\begin{multline*}
[f]\sqcap[g] =
[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}f]\sqcap
[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}g] = \\
\text{(obvious~\ref{unfix-mor-emb})} =
[\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}f\sqcap
\iota_{\Src f\sqcup\Src g,\Dst f\sqcup\Dst g}g].
\end{multline*}
\end{proof}

\begin{cor}
If every $\Hom$-set is a lattice, then
the poset of unfixed morphisms is a lattice.
\end{cor}

\begin{thm}
Meet of nonempty set of unfixed morphisms
exists provided that the orders of $\Hom$-sets are
posets, every nonempty subset of which has a meet, and
our category is with ordered domain
and image and that morphisms~$\mathcal{E}$ are metamonovalued
and metainjective.
\end{thm}

\begin{proof}
Let~$S$ be a nonempty set of unfixed morphisms. Take
an arbitrary unfixed morphism~$f\in S$. Take an
arbitrary $F\in f$. Let $A=\Src F$ and $B=\Dst F$.

$\bigsqcap S=\bigsqcap\rsupfun{f\sqcap}S=
\bigsqcap\rsupfun{[F]\sqcap}S=
\bigsqcap\setcond{[F]\sqcap[G]}{g\in S,G\in g}=
\bigsqcap\setcond{[\iota_{A\sqcup\Src G,B\sqcup\Dst G}F\sqcap\iota_{A\sqcup\Src G,B\sqcup\Dst G}G]}{g\in S,G\in g}$

We will prove
$\iota_{A\sqcup\Src G,B\sqcup\Dst G}F\sqcap\iota_{A\sqcup\Src G,B\sqcup\Dst G}G \sim F\sqcap\iota_{A,B}G$.

$\iota_{A\sqcup\Src G,B\sqcup\Dst G}F\sqcap\iota_{A\sqcup\Src G,B\sqcup\Dst G}G\sqsubseteq
\iota_{A\sqcup\Src G,B\sqcup\Dst G}F$ and
$\iota_{A\sqcup\Src G,B\sqcup\Dst G}\iota_{A,B}\iota_{A\sqcup\Src G,B\sqcup\Dst G}F=
\iota_{A\sqcup\Src G,B\sqcup\Dst G}F$, thus by
being with ordered domain and image
\begin{multline*}
\iota_{A\sqcup\Src G,B\sqcup\Dst G}F\sqcap\iota_{A\sqcup\Src G,B\sqcup\Dst G}G = \\
\iota_{A\sqcup\Src G,B\sqcup\Dst G}\iota_{A,B}(\iota_{A\sqcup\Src G,B\sqcup\Dst G}F\sqcap\iota_{A\sqcup\Src G,B\sqcup\Dst G}G) = \\
\text{(by being metamonovalued and metainjective)} = \\
\iota_{A\sqcup\Src G,B\sqcup\Dst G}(
\iota_{A,B}\iota_{A\sqcup\Src G,B\sqcup\Dst G}F\sqcap
\iota_{A,B}\iota_{A\sqcup\Src G,B\sqcup\Dst G}G) = \\
\iota_{A\sqcup\Src G,B\sqcup\Dst G}(
\iota_{A,B}F\sqcap\iota_{A,B}G) \sim
\iota_{A,B}F\sqcap\iota_{A,B}G=
F\sqcap\iota_{A,B}G.
\end{multline*}

Due the proved equivalence we have
$\bigsqcap S=
\bigsqcap\setcond{[F\sqcap\iota_{A,B}G]}{g\in S,G\in g}$.
Now we can apply proposition~\ref{cmpl-lat-par}:
$\bigsqcap S=
\left[\bigsqcap\setcond{F\sqcap\iota_{A,B}G}{g\in S,G\in g}\right]$. We have provided an explicit formula
for~$\bigsqcap S$.
\end{proof}

The poset of unfixed morphisms may be not a complete
lattice even if every $\Hom$-set is a complete lattice.
We will show this below for funcoids.

\subsection{Domain and image of unfixed morphisms}

\begin{prop}
$\operatorname{IM}f=
\setcond{Y\in\mathfrak{Z}}{\id_Y\circ[f]=[f]}$;
$\operatorname{DOM}f=
\setcond{X\in\mathfrak{Z}}{[f]\circ\id_X=[f]}$.
\end{prop}

\begin{proof}
We will prove only the first, as the second is similar.
$\id_Y\circ[f]=[f]\Leftrightarrow
\id^{\mathcal{C}(Y\sqcup\Dst f,Y\sqcup\Dst f)}_{Y}\circ
\mathcal{E}^{\Dst f,Y\sqcup\Dst f}\circ f=
\mathcal{E}^{\Dst f,Y\sqcup\Dst f}\circ f\Leftrightarrow
\id^{\mathcal{C}(\Dst f,Y\sqcup\Dst f)}_{[Y]\sqcap[\Dst f]}
\circ f=\mathcal{E}^{\Dst f,Y\sqcup\Dst f}
\circ f\Leftrightarrow
\mathcal{E}^{Y\sqcup\Dst f,\Dst f}
\circ \id^{\mathcal{C}(\Dst f,Y\sqcup\Dst f)}_{[Y]\sqcap[\Dst f]}
\circ f=f\Leftrightarrow
\id^{\mathcal{C}(\Dst f,\Dst f)}_{[Y]\sqcap[\Dst f]}\circ f=f
Y\in\operatorname{IM}f$.
\end{proof}

The above proposition allows to define:

\begin{defn}
$\operatorname{DOM}f=\operatorname{DOM}F$ and
$\operatorname{IM}f=\operatorname{IM}F$
for $F\in f$.
\end{defn}

\subsection{Rectangular restriction}

\begin{prop}
$\iota_{A,B}f=\iota_{A,B}g$ if $f\sim g$.
\end{prop}

\begin{proof}
Let $f\sim g$. Then $g=\iota_{\Src g,\Dst g}f$.
So $\iota_{A,B}g=\iota_{A,B}\iota_{\Src g,\Dst g}f
\sqsubseteq\text{(proposition~\ref{iota-less})}\sqsubseteq
\iota_{A,B}f$. Similarly,
$\iota_{A,B}f\sqsubseteq\iota_{A,B}g$. So
$\iota_{A,B}f=\iota_{A,B}g$.
\end{proof}

The above proposition allows to define:

\begin{defn}
$\iota_{A,B}F=\iota_{A,B}f$ for
an unfixed morphism~$F$ and arbitrary $f\in F$.
\end{defn}

\begin{defn}
$F\square_{A,B}=[\iota_{A,B}F]$ for every unfixed
morphism~$F$.
\end{defn}

\begin{prop}
$F\square_{A,B}=\id_B\circ F\circ\id_A$ for every
unfixed morphism~$F$ and objects~$A$ and~$B$.
\end{prop}

\begin{proof}
Take $f\in F$.
$F\square_{A,B}=[\iota_{A,B}F]=[\iota_{A,B}f]=
[\mathcal{E}^{\Dst f,B}\circ f\circ\mathcal{E}^{A,\Src f}]=
[\id^{\mathcal{C}(\Dst f,B)}_{B\sqcap\Dst f}\circ f\circ
\id^{\mathcal{C}(A,\Src f)}_{A\sqcap\Src f}]=
[\id^{\mathcal{C}(\Dst f,B)}_{B}\circ
\id^{\mathcal{C}(\Dst f,\Dst f)}_{\Dst f}\circ
f\circ
\id^{\mathcal{C}(\Src f,\Src f)}_{\Src f}\circ
\id^{\mathcal{C}(A,\Src f)}_{A}]=
[\id^{\mathcal{C}(\Dst f,B)}_{B}\circ f\circ
\id^{\mathcal{C}(A,\Src f)}_{A}]=
[\id^{\mathcal{C}(\Dst f,B)}_{B}]\circ [f]\circ
[\id^{\mathcal{C}(A,\Src f)}_{A}]=
\id_B\circ F\circ\id_A$.
\end{proof}

\begin{prop}
$f\square_{A_0,B_0}\square_{A_1,B_1}=
f\square_{A_0\sqcap A_1,A_1\sqcap B_1}$.
\end{prop}

\begin{proof}
From the previous
$f\square_{A_0,B_0}\square_{A_1,B_1}=
\id_{B_1}\circ\id_{B_0}\circ f\circ\id_{A_0}\circ\id_{A_1}=
\id_{B_0\sqcap B_1}\circ f\circ\id_{A_0\sqcap A_1}=
f\square_{A_0\sqcap A_1,A_1\sqcap B_1}$.
\end{proof}

\begin{defn}
$f|_X=f\circ\id_X$ for every unfixed morphism~$f$ and
$X\in\mathfrak{A}$.
\end{defn}

\begin{obvious}
$(f|_X)|_Y=f_{X\sqcap Y}$.
\end{obvious}

\subsection{Algebraic properties of the lattice of unfixed
morphisms}

The following proposition allows to easily prove algebraic
properties (cf. distributivity) of the poset of unfixed morphisms:

\begin{thm}\label{unfix-fix-bij}
The following are mutually inverse bijections:
\begin{enumerate}
\item\label{unfix-fix-bij-sd} Let~$A$ and~$B$ be objects. $f\mapsto[f]$ and $F\mapsto\iota_{A,B}F$
are mutually inverse order isomorphisms between
$\setcond{f\in\text{unfixed morphisms}}{A\in\operatorname{DOM}f,B\in\operatorname{IM}f}$
and~$\mathcal{C}(A,B)$.
If $A=B$ they are also semigroup isomorphisms.
\item\label{unfix-fix-bij-d} Let~$T$ be an unfixed morphism. $f\mapsto[f]$ and $F\mapsto\iota_{\Src t,\Dst t}F$ are mutually inverse order isomorphisms
between the lattice~$DT$ and $Dt$ whenever~$t\in T$.
\end{enumerate}
\end{thm}

\begin{proof}
We will prove that these functions are mutually inverse
bijections. That they are order-preserving is obvious.
\begin{widedisorder}
\item[\ref{unfix-fix-bij-sd}]
$\iota_{A,B}F\in\mathcal{C}(A,B)$ is obvious.

We need to prove that
$[f]\in\setcond{f\in\text{unfixed morphisms}}{A\in\operatorname{DOM}f,B\in\operatorname{IM}f}$.
For this it's enough to prove
$A\in\operatorname{DOM}[f]\land B\in\operatorname{IM}[f]$
what is the same as
$A\in\operatorname{DOM}f\land B\in\operatorname{IM}f$
what follows from proposition~\ref{dst-in-im}.

Because $f\mapsto[f]$ is an injection, it is
enough\footnote{\url{https://math.stackexchange.com/a/3007051/4876}}
to prove that 
$\iota_{A,B}[f]=f$. Really, $\iota_{A,B}[f]=\iota_{A,B}f=f$.

That they are semigroup isomorphisms follows from the
already proved formula $[g\circ f]=[g]\circ[f]$.

\item[\ref{unfix-fix-bij-d}]
Because of the previous, it is enough to prove that
$[f]\in DT\Leftrightarrow f\in Dt$. Really, it is equivalent
to $[f]\sqsubseteq T\Leftrightarrow f\sqsubseteq t$
what is obvious.
\end{widedisorder}
\end{proof}

\begin{prop}
If every $\Hom$-set is a distributive lattice, then
the poset of unfixed morphisms is a distributive lattice.
\end{prop}

\begin{proof}
It follows from the above isomorphism.
\end{proof}

\begin{prop}
If every $\Hom$-set is a co-brouwerian lattice, then
the poset of unfixed morphisms is a co-brouwerian lattice.
\end{prop}

\begin{proof}
It follows from the above isomorphism and the definition
of pseudodifference.
\end{proof}

\begin{prop}
If every $\Hom$-set is a lattice with quasidifference, then
the poset of unfixed morphisms is a lattice with
quasidifference.
\end{prop}

\begin{proof}
It follows from the above isomorphism and the definition
of quasidifference.
\end{proof}

\begin{prop}
~
\begin{enumerate}
\item If every $\Hom$-set is an atomic lattice, then
the poset of unfixed morphisms is an atomic lattice.
\item If every $\Hom$-set is an atomistic lattice, then
the poset of unfixed morphisms is an atomistic lattice.
\end{enumerate}
\end{prop}

\begin{proof}
Follows from the above isomorphism.
\end{proof}

\subsection{Binary product morphism}

\begin{defn}
For a category~$\mathcal{C}$ with binary product morphism
and $X,Y\in\mathfrak{A}$ define
$X\times Y=[X\times_{A,B}Y]$ where
$A\in\mathfrak{Z}$, $[A]\sqsupseteq X$,
$B\in\mathfrak{Z}$, $[B]\sqsupseteq Y$.
(Such~$A$ and~$B$ exist by an axiom of categories with
restricted identities.)
\end{defn}

We need to prove validity of this definition:

\begin{proof}
Let
$A_0\in\mathfrak{Z}$, $[A_0]\sqsupseteq X$,
$B_0\in\mathfrak{Z}$, $[B_0]\sqsupseteq Y$,
$A_1\in\mathfrak{Z}$, $[A_1]\sqsupseteq X$,
$B_1\in\mathfrak{Z}$, $[B_1]\sqsupseteq Y$.
We need to prove $X\times_{A_0,B_0}Y\sim X\times_{A_1,B_1}Y$,
but it trivially follows from an axiom in the definition of
category with binary product morphism.
\end{proof}

\begin{prop}
$(X_0\times Y_0)\sqcap(X_1\times Y_1)=
(X_0\sqcap X_1)\times(Y_0\sqcap Y_1)$ for every
$X_0,X_1,Y_0,Y_1\in\mathfrak{A}$.
\end{prop}

\begin{proof}
Take
$A_0\in\mathfrak{Z}$, $[A_0]\sqsupseteq X_0$,
$B_0\in\mathfrak{Z}$, $[B_0]\sqsupseteq Y_0$,
$A_1\in\mathfrak{Z}$, $[A_1]\sqsupseteq X_1$,
$B_1\in\mathfrak{Z}$, $[B_1]\sqsupseteq Y_1$.

Then
$(X_0\times Y_0)\sqcap(X_1\times Y_1)=
[X_0\times_{A_0\sqcup A_1,B_0\sqcup B_1}Y_0]\sqcap
[X_1\times_{A_0\sqcup A_1,B_0\sqcup B_1}Y_1]=
[(X_0\times_{A_0\sqcup A_1,B_0\sqcup B_1}Y_0)\sqcap
(X_1\times_{A_0\sqcup A_1,B_0\sqcup B_1}Y_1)]=
[(X_0\sqcap X_1)\times_{A_0\sqcup A_1,B_0\sqcup B_1}
(Y_0\sqcap Y_1)]=
(X_0\sqcap X_1)\times(Y_0\sqcap Y_1)$.
\end{proof}

\begin{prop}
$f\square_{A,B}=f\sqcap(A\times B)$.
\end{prop}

\begin{proof}
Take $F\in f$. Let $F'=\iota_{A\sqcup\Src F,B\sqcup\Dst F}F$.
We have $F'\in f$.
$f\square_{A,B}=[\iota_{A,B}F']=
[\mathcal{E}^{B\sqcup\Dst F,B}\circ F'\circ
\mathcal{E}^{A,A\sqcup\Src F}]=
[\id^{\mathcal{C}(B\sqcup\Dst F,B)}_{[B]}\circ F'\circ
\id^{\mathcal{C}(A,A\sqcup\Src F)}_{[A]}]=
[\id^{\mathcal{C}(B\sqcup\Dst F,B)}_{[B]}]\circ [F']\circ
[\id^{\mathcal{C}(A,A\sqcup\Src F)}_{[A]}]=
[\id^{\mathcal{C}(B\sqcup\Dst F,B\sqcup\Dst F)}_{[B]}]\circ
[F']\circ
[\id^{\mathcal{C}(A\sqcup\Src F,A\sqcup\Src F)}_{[A]}]=
[\id^{\mathcal{C}(B\sqcup\Dst F,B\sqcup\Dst F)}_{[B]}\circ
F'\circ
\id^{\mathcal{C}(A\sqcup\Src F,A\sqcup\Src F)}_{[A]}]=
[F'\sqcap(A\times_{A\sqcup\Src F,B\sqcup\Dst F}B)]=
[F']\sqcap[A\times_{A\sqcup\Src F,B\sqcup\Dst F}B]=
f\sqcap(A\times B)$.
\end{proof}

\section{Categories with embeddings}

\begin{note}
This section in not used below, it is just to feed your intuition.
\end{note}

The following generalizes the well known concept of embedding function $A
\hookrightarrow B$ for from a set $A$ to a set $B$ where $A \subseteq B$.

I will set that the unique morphism from an object $A$ to an object $B$ of a
thin category is equal to the pair $(A , B)$.

\begin{defn}
  A \emph{category with embeddings of objects} is a dagger category with a
  preorder of the set of objects together with a functor $\hookrightarrow$ (we
  will denote applying this functor to the object $(A , B)$ as $A
  \hookrightarrow B$.) such that:
  \begin{itemize}
    \item $\hookrightarrow$ is an identity on objects.
    
    \item Every $A \hookrightarrow B$ is a monomorphism.
    
    \item $(A \hookrightarrow B)^{\dagger} \circ (A \hookrightarrow B) = 1_A$.
  \end{itemize}
\end{defn}

\begin{obvious}
$A\hookrightarrow B$ is defined when $(A , B)$ is a morphism of the preorder
that is when $A \sqsubseteq B$.
\end{obvious}

\begin{obvious}
$A \hookrightarrow B : A \rightarrow B$ when $A \sqsubseteq B$.
\end{obvious}

\begin{prop}
  $A \hookrightarrow A = 1_A$.
\end{prop}

\begin{proof}
  Because $(A , A)$ is an identity morphism and $\hookrightarrow$ preserves
  identities.
\end{proof}

\begin{prop}
  $(B \hookrightarrow C) \circ (A \hookrightarrow B) = A \hookrightarrow C$
  whenever $A \sqsubseteq B \sqsubseteq C$.
\end{prop}

\begin{proof}
  $(B \hookrightarrow C) \circ (A \hookrightarrow B) = \hookrightarrow (B , C)
  \circ \hookrightarrow (A , B) = \hookrightarrow ((B , C) \circ (A , B)) =
  \hookrightarrow (A , C) = A \hookrightarrow C$.
\end{proof}

\section{\texorpdfstring{Categories under $\mathbf{Rel}$}{Categories under Rel}}

TODO: Filtrators of unfixed morphisms.

\begin{defn}
  The $\mathbf{Rel}$-morphism $\mathcal{E}^{A,B}$
  (\emph{restriction-embedding}) is defined by the formula: $\mathcal{E}^{A,B}
  = (A , B , \id_{A \cap B})$.
  
  When $A$ is clear from context, I will denote it just as $\mathcal{E}^B$.
\end{defn}

\begin{obvious}
If $A \subseteq B$ then $\mathcal{E}^{A,B}$ is an embedding $A \hookrightarrow B
= (A , B , \id_A)$.
\end{obvious}

\begin{obvious}
If $A \supseteq B$ then $\mathcal{E}^{A,B} = (A , B ,
\id_B)$.
\end{obvious}

\begin{obvious}
$\mathcal{E}^{A,A} = 1^{\mathbf{Rel}}_A$.
\end{obvious}

\begin{obvious}
$(\mathcal{E}^{A,B})^{- 1} = \mathcal{E}^{B,A}$.
\end{obvious}

\begin{defn}
\emph{Dagger functor} between two dagger categories is a functor between
these categories, which commutes with the daggers.
\fxwarning{Clearer wording.}
\end{defn}

\begin{defn}
\emph{Category under $\mathbf{Rel}$} is a pair $(C , \uparrow)$
where $C$ is a category whose objects are small sets and $\uparrow$ is an
identity-on-objects functor $\mathbf{Rel} \rightarrow C$. I call
$\uparrow$ \emph{up-arrow functor}.
\fxnote{We can use any category conforming to the above
axioms instead of~$\mathbf{Rel}$.}
\end{defn}

\begin{defn}
  \emph{Dagger category under $\mathbf{Rel}$} is a pair $(C ,
  \uparrow)$ where $C$ is a dagger category whose objects are small sets and
  $\uparrow$ is a dagger identity-on-objects functor $\mathbf{Rel}
  \rightarrow C$.
\end{defn}

\begin{defn}
  $\mathcal{E}_{\mathcal{C}}^{A,B} = \uparrow \mathcal{E}^{A,B}$. In
  other words, $\mathcal{E}_{\mathcal{C}} = \uparrow \circ \mathcal{E}$.
  
  When $A$ is clear from context, I will denote it just as $\mathcal{E}_{\mathcal{C}}^B$.
\end{defn}

\begin{prop}
  $\mathcal{E}_{\mathcal{C}}^{A,A} = 1_{\mathcal{C}}^A$.
\end{prop}

\begin{proof}
  $\mathcal{E}_{\mathcal{C}}^{A,A} = \uparrow \mathcal{E}^{A,A} =
  \uparrow 1_{\mathbf{Rel}} = 1_{\mathcal{C}}^A$.
\end{proof}

\begin{prop}
  If $f : X \rightarrow Y$ is a $\mathbf{Rel}$-morphism and
  $\im f = A \subseteq Y$ then
  \[ \mathcal{E}^{A,Y} \circ \mathcal{E}^{Y,A} \circ f = f. \]
\end{prop}

\begin{proof}
  $\mathcal{E}^{A,Y} \circ \mathcal{E}^{Y,A} \circ f = 1_{\mathcal{C}}^A
  \circ f = f$.
\end{proof}

\begin{defn}
  \emph{Partially ordered dagger category under $\mathbf{Rel}$} is
  a category which is both a partially ordered dagger category and a category
  under $\mathbf{Rel}$ such that $\uparrow \circ f^{- 1} = (\uparrow
  \circ f)^{\dagger}$ and $A \sqsubseteq B \Rightarrow \uparrow A \sqsubseteq
  \uparrow B$.
\end{defn}

\begin{prop}
  $(\mathcal{E}_{\mathcal{C}}^{A,B})^{\dagger} = \mathcal{E}_{\mathcal{C}}^{B,A}$ for a dagger category under
  $\mathbf{Rel}$.
\end{prop}

\begin{proof}
  $(\mathcal{E}_{\mathcal{C}}^{A,B})^{\dagger} = (\uparrow \mathcal{E}^{A,B})^{\dagger} = \uparrow (\mathcal{E}^{A,B})^{- 1} =
  \uparrow \mathcal{E}^{B,A} = \mathcal{E}_{\mathcal{C}}^{B,A}$.
\end{proof}

\begin{prop}
  For a partially ordered dagger category $\mathcal{C}$ under
  $\mathbf{Rel}$ we have $\mathcal{E}_{\mathcal{C}}^{A,B}$ is:
  \begin{enumerate}
    \item monovalued;
    
    \item injective;
    
    \item entirely defined if $A \subseteq B$;
    
    \item surjective if $B \subseteq A$.
  \end{enumerate}
\end{prop}

\begin{proof}
  ~
  \begin{enumerate}
    \item $\mathcal{E}^{A,B} \circ \mathcal{E}^{B,A} \sqsubseteq
    1^{\mathbf{Rel}}_B$; $\mathcal{E}^{A,B} \circ (\mathcal{E}^{A,B})^{- 1} \sqsubseteq 1^{\mathbf{Rel}}_B$;
    $\mathcal{E}_{\mathcal{C}}^{A,B} \circ (\mathcal{E}_{\mathcal{C}}^{A,B})^{\dagger} \sqsubseteq 1^{\mathcal{C}}_B$.
    
    \item $\mathcal{E}^{B,A} \circ \mathcal{E}^{A,B} \sqsubseteq
    1^{\mathbf{Rel}}_A$; $(\mathcal{E}^{A,B})^{- 1} \circ \mathcal{E}^{A,B} \sqsubseteq 1^{\mathbf{Rel}}_A$;
    $(\mathcal{E}_{\mathcal{C}}^{A,B})^{\dagger} \circ \mathcal{E}^{A,B} \sqsubseteq 1^{\mathcal{C}}_A$.
    
    \item $\mathcal{E}^{B,A} \circ \mathcal{E}^{A,B} \sqsupseteq
    1^{\mathbf{Rel}}_A$; $(\mathcal{E}^{A,B})^{- 1} \circ \mathcal{E}^{A,B} \sqsupseteq 1^{\mathbf{Rel}}_A$;
    $(\mathcal{E}_{\mathcal{C}}^{A,B})^{\dagger} \circ \mathcal{E}_{\mathcal{C}}^{A,B} \sqsupseteq 1^{\mathcal{C}}_A$.
    
    \item $\mathcal{E}^{A,B} \circ \mathcal{E}^{B,A} \sqsupseteq
    1^{\mathbf{Rel}}_A$; $\mathcal{E}^{A,B} \circ (\mathcal{E}^{A,B})^{- 1} \sqsupseteq 1^{\mathbf{Rel}}_A$;
    $\mathcal{E}_{\mathcal{C}}^{A,B} \circ (\mathcal{E}_{\mathcal{C}}^{A,B})^{\dagger} \sqsupseteq 1^{\mathcal{C}}_A$.
  \end{enumerate}
\end{proof}

??

\section{\texorpdfstring{Examples of partially ordered dagger categories under
$\mathbf{Rel}$}{Examples of partially ordered dagger categories under Rel}}

\subsection{\texorpdfstring{Category $\mathbf{Rel}$}{Category Rel}}

Category $\mathbf{Rel}$ with the identity up-arrow functor to itself
and ``reverse relation'' as the dagger is an obvious example of a partially
ordered dagger category under $\mathbf{Rel}$.

\begin{prop}
  $\iota_{A, B} f = (A , B , \GR f \cap (A \times B))$.
\end{prop}

\begin{proof}
  $\iota_{A, B} f = \mathcal{E}^{B} \circ f \circ (\mathcal{E}^{A})^{-1} = (A , B , \GR f \cap (A \times B))$.
\end{proof}

\subsection{\texorpdfstring{Category $\mathsf{FCD}$}{Category FCD}}

Category $\mathsf{FCD}$ with the up-arrow functor
$\uparrow^{\mathsf{FCD}}$ and ``reverse funcoid'' as the dagger is a
partially ordered dagger category under $\mathbf{Rel}$.

\begin{prop}
  $\mathcal{E}_{\mathsf{FCD}}^{A,B} = (A , B , \lambda \mathcal{X}
  \in \mathfrak{F} (A) : \mathcal{X} \div B , \lambda \mathcal{Y} \in
  \mathfrak{F} (B) : \mathcal{Y} \div A)$ for objects $A \subseteq B$ of
  $\mathsf{FCD}$.
\end{prop}

\begin{proof}
  $\langle \mathcal{E}_{\mathsf{FCD}}^{A,B} \rangle \mathcal{X} =
  \bigsqcap \setcond{ \langle \mathcal{E}_{\mathsf{FCD}}^{A,B}
  \rangle^{\ast} X }{ X \in \mathcal{X} } =
  \bigsqcap \setcond{ \uparrow^B  \langle \mathcal{E}^{A,B} \rangle X
  }{ X \in \mathcal{X} } = \bigsqcap \setcond{
  \uparrow^B  (X \cap A \cap B) }{ X \in \mathcal{X}
  } = \bigsqcap \setcond{ \uparrow^B  (X \cap B) }{
  X \in \mathcal{X} } = \mathcal{X} \div B$.
  
  Rest follows from symmetry.
\end{proof}

\begin{prop}
  ~
  \begin{enumerate}
    \item $\langle \mathcal{E}_{\mathsf{FCD}}^{A,B} \rangle^{\ast} X
    = \uparrow^B X$ for every $X \in \subsets A$ if $A \subseteq B$.
    
    \item $\langle \mathcal{E}_{\mathsf{FCD}}^{B,A} \rangle^{\ast}
    Y = \uparrow^A (Y \cap A)$ for every $Y \in \subsets B$ if $A \subseteq
    B$.
  \end{enumerate}
\end{prop}

\begin{proof}
  By definition of principal funcoid.
\end{proof}

\fxnote{Unfixed funcoids seem to be embedded into pointfree 
funcoids between unfixed filters.
Also unfixed reloids can be embedded into reloids
between the Grothendieck universes.}

\subsection{\texorpdfstring{Category $\mathsf{RLD}$}{Category RLD}}

Category $\mathsf{RLD}$ with the up-arrow functor
$\uparrow^{\mathsf{RLD}}$ and ``reverse reloid'' as the dagger is a
partially ordered dagger category under $\mathbf{Rel}$.

\begin{obvious}
$\mathcal{E}_{\mathsf{RLD}}^{A,B} = \uparrow^{\mathsf{RLD} (A ,
B)} \id_{A \cap B}$.
\end{obvious}

\begin{defn}
  $f \div (A \times B) = (A , B , (\GR f) \div (A \times B))$ for every
  reloid $f$.
\end{defn}

\begin{prop}
  $\iota_{A, B} f = f \div (A \times B)$.
\end{prop}

\begin{proof}
  $\iota_{A, B} f = \mathcal{E}_{\mathsf{RLD}}^{B}
\circ f \circ (\mathcal{E}_{\mathsf{RLD}}^{A})^{-1} =
\bigsqcap \setcond{ \uparrow^{\mathsf{RLD}} (\mathcal{E}^{B} \circ F \circ (\mathcal{E}^{A})^{-1}
}{ F \in \GR f } = \bigsqcap \setcond{
\uparrow^{\mathsf{RLD}} (F \cap (A \times B))}
{F \in \GR f } = f \div (A \times B)$.

\fxwarning{Filters on Cartesian products vs reloids.}
\end{proof}

\fxnote{Unfixed reloids seem to be equivalent to
endoreloids on the set of unfixed filters.}

\subsection{Some isomorphisms}

\begin{prop}
  $\setcond{ (\mathcal{A} \div A , \mathcal{A} \sqcap A) }{
  \mathcal{A} \in \mathfrak{F} (U) }$ is a function and
  moreover is an order isomorphism for a set $A \subseteq U$.
\end{prop}

\begin{proof}
  $\mathcal{A} \div A$ and $\mathcal{A} \sqcap A$ are determined by each other
  by the following formulas:
  \[ \mathcal{A} \div A = (\mathcal{A} \sqcap A) \div A \quad
     \text{and} \quad \mathcal{A} \sqcap A = (\mathcal{A} \div A) \div
     \Base (\mathcal{A}) . \]
  Prove the formulas: $(\mathcal{A} \sqcap A) \div A = \bigsqcap \setcond{
  \uparrow^A (X \cap A) }{ X \in \mathcal{A} \sqcap A
  } = \bigsqcap \setcond{ \uparrow^A (X \cap A) }{
  X \in \mathcal{A} } = \mathcal{A} \div A$.
  
  $(\mathcal{A} \div A) \div \Base (\mathcal{A}) = \bigsqcap \setcond{
  \uparrow^A (X \cap A) }{ X \in \mathcal{A} }
  \div \Base (\mathcal{A}) = \bigsqcap \setcond{ \uparrow^{\Base
  (\mathcal{A})} (Y \cap \Base (\mathcal{A})) }{
  Y \in \bigsqcap \setcond{ \uparrow^A (X \cap A) }{
  X \in \mathcal{A} } } = \text{(by properties of
  filter bases)} = \bigsqcap \setcond{ \uparrow^{\Base (\mathcal{A})} (X
  \cap A \cap \Base (\mathcal{A})) }{ X \in
  } = \bigsqcap \setcond{ \uparrow^{\Base
  (\mathcal{A})} (X \cap A) }{ X \in \mathcal{A}
  } = \mathcal{A} \sqcap A$.
  
  That this defines a bijection, follows from $\mathcal{A} \div A \sim
  \mathcal{A} \sqcap A$ what easily follows from the above formulas.
\end{proof}

\begin{prop}
  $\setcond{ (\iota_{X, Y} f , \id^{\mathbf{Rel}}_Y \circ f \circ
  \id^{\mathbf{Rel}}_X) }{ f \in
  \mathbf{Rel} (A , B) }$ is a function and moreover is an
  (order and semigroup) isomorphism, for sets $X \subseteq \Src f$, $Y
  \subseteq \Dst f$.
\end{prop}

\begin{proof}
  $\iota_{X, Y} f = (X , Y , \GR f \cap (X \times Y))$;
  $\id^{\mathbf{Rel}}_Y \circ f \circ
  \id^{\mathbf{Rel}}_X = (\Src f , \Dst f ,
  \GR f \cap (X \times Y))$. The isomorphism (both order and semigroup)
  is evident.
\end{proof}

\begin{prop}
  $\setcond{ (\iota_{X, Y} f , \id^{\mathsf{FCD}}_Y
  \circ f \circ \id^{\mathsf{FCD}}_X) }{
  f \in \mathsf{FCD} (A , B) }$ is a function and moreover is an
  (order and semigroup) isomorphism, for sets $X \subseteq \Src f$, $Y
  \subseteq \Dst f$.
\end{prop}

\begin{proof}
  From symmetry it follows that it's enough to prove that $\setcond{ \left(
  \mathcal{E}^Y \circ f , \id^{\mathsf{FCD}}_Y \circ f \right)
  }{ f \in \mathsf{FCD} (A , B) }$ is a
  function and moreover is an (order and semigroup) isomorphism, for a set $Y
  \subseteq \Dst f$.
  
  Really, $\setcond{ (\langle \mathcal{E}^Y \rangle x , \langle
  \id^{\mathsf{FCD}}_Y \rangle x) }{ x
  \in \Dst f } = \setcond{ (x \div Y , x \sqcap Y) }{
  x \in \Dst f }$ is an order isomorphism by proved
  above. This implies that $\setcond{ \left( \mathcal{E}^Y \circ f ,
  \id^{\mathsf{FCD}}_Y \circ f \right) }{
  f \in \mathsf{FCD} (A , B) }$ is an isomorphism
  (both order and semigroup).
\end{proof}

\begin{prop}
  $\setcond{ (\iota_{X, Y} f , \id^{\mathsf{RLD}}_Y \circ f \circ
  \id^{\mathsf{RLD}}_X) }{ f \in
  \mathsf{RLD} (A , B) }$ is a function and moreover is an
  (order and semigroup) isomorphism, for sets $X \subseteq \Src f$, $Y
  \subseteq \Dst f$.
\end{prop}

\begin{proof}
  $\iota_{X, Y} f = (X , Y , (\up f) \div (X \times Y))$;
  $\id^{\mathsf{RLD}}_Y \circ f \circ
  \id^{\mathsf{RLD}}_X = (\Src f , \Dst f ,
  (\up f) \sqcap (X \times Y))$. They are order isomorphic by proved
  above.
  
  $\iota_{Y, Z} g \circ \iota_{X, Y} f =\mathcal{E}^Z \circ g \circ
  (\mathcal{E}^Y)^{- 1} \circ \mathcal{E}^Y \circ f \circ (\mathcal{E}^X)^{-
  1} =\mathcal{E}^Z \circ g \circ \id^{\mathsf{RLD}}_Y \circ
  \id^{\mathsf{RLD}}_Y \circ f \circ (\mathcal{E}^X)^{- 1}$
  because $(\mathcal{E}^Y)^{- 1} \circ \mathcal{E}^Y =
  \id^{\mathbf{Rel}}_Y = \id^{\mathbf{Rel}}_Y
  \circ \id^{\mathbf{Rel}}_Y$. Thus by proved above
  \[ \setcond{ (\iota_{Y, Z} g \circ \iota_{X, Y} f ,
     \id^{\mathsf{RLD}}_Z \circ g \circ
     \id^{\mathsf{RLD}}_Y \circ \id^{\mathsf{RLD}}_Y
     \circ f \circ \id^{\mathsf{RLD}}_X) }{
     f \in \mathsf{RLD} (A , B) } \]
  is a bijection.
\end{proof}

\fxnote{Research the semigroups (Wikipedia) of funcoids and
reloids.}