mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
3 commits
1a6f409cd1
...
75d6990bd5
| Author | SHA1 | Date | |
|---|---|---|---|
75d6990bd5
|
|||
|
f37458fe97
|
|||
|
2dbf69bcf6
|
11 changed files with 355 additions and 344 deletions
|
|
@ -125,6 +125,7 @@ private
|
||||||
where
|
where
|
||||||
f' = (η _ +₁ idC) ∘ f
|
f' = (η _ +₁ idC) ∘ f
|
||||||
g' = (η _ +₁ idC) ∘ g
|
g' = (η _ +₁ idC) ∘ g
|
||||||
|
w : X × Z ⇒ monadK.F.F₀ (X × K.₀ U + K.₀ Y × Z) + X × Z
|
||||||
w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')
|
w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')
|
||||||
w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #
|
w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w #
|
||||||
w-law₁ = sym (begin
|
w-law₁ = sym (begin
|
||||||
|
|
|
||||||
3
thesis/.vscode/ltex.dictionary.en-US.txt
vendored
3
thesis/.vscode/ltex.dictionary.en-US.txt
vendored
|
|
@ -71,3 +71,6 @@ copatterns
|
||||||
epimorphisms
|
epimorphisms
|
||||||
monomorphisms
|
monomorphisms
|
||||||
expressivity
|
expressivity
|
||||||
|
Friedrich-Alexander-Universität
|
||||||
|
Erlangen-Nürnberg
|
||||||
|
Goncharov
|
||||||
|
|
|
||||||
|
|
@ -3,3 +3,5 @@
|
||||||
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
|
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
|
||||||
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
|
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[ignoreall,show=definition]\\E$"}
|
||||||
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[1]Coalgs(#1)\\E$"}
|
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[1]Coalgs(#1)\\E$"}
|
||||||
|
{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Q[cases] mycase Case .\\E$"}
|
||||||
|
{"rule":"COMMA_PARENTHESIS_WHITESPACE","sentence":"^\\Q[cases] mycase Case .\\E$"}
|
||||||
|
|
|
||||||
|
|
@ -39,3 +39,13 @@
|
||||||
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QGiven a functor \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a (H-)guarded Elgot algebra consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a H-algebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:guardedfixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardeduniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardedcompositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QGiven a functor \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a (H-)guarded Elgot algebra consists of: An object \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, a H-algebra structure \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, and for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, satisfying the following axioms: law:guardedfixpoint Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardeduniformity Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:guardedcompositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||||
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qlaw:compositionality Compositionality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:stutter Stutter: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, law:diamond Diamond: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||||
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QAn Elgot monad consists of A monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Naturality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Codiagonal: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
{"rule":"MORFOLOGIK_RULE_EN_US","sentence":"^\\QAn Elgot monad consists of A monad \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, for every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q an iteration \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q satisfying: Fixpoint: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Uniformity: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q implies \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Naturality: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, Codiagonal: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QLet \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q be a setoid function, we define \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q point wise: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QGiven a function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, the lifted function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is defined as \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QConsider, \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is a setoid function that maps every \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q to \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QNow, consider the following function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q which tries running two computations and returns the one that finished first: \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QLastly, consider the function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which adds a number of \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q constructors in front of a value and is given by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QConsider another setoid function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QNext, let us consider functions for counting steps of computations, first regard \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q, which returns the number of steps a terminating computation has to take and is defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q and \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QConsider \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"IF_IS","sentence":"^\\QFurthermore, consider the setoid function \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q defined by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q Now, by coinduction we can easily follow that \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q for any \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+$"}
|
||||||
|
{"rule":"WHITESPACE_RULE","sentence":"^\\QFriedrich-Alexander-Universität Erlangen-Nürnberg [] Chair for Computer Science 8 Theoretical Computer Science Bachelor Thesis in Computer Science [0.5] Advisor: Sergey Goncharov Erlangen,\\E$"}
|
||||||
|
|
|
||||||
|
|
@ -12,30 +12,29 @@
|
||||||
frame=lines,
|
frame=lines,
|
||||||
autogobble
|
autogobble
|
||||||
}
|
}
|
||||||
|
% \usepackage{mathabx}
|
||||||
|
% \usepackage{amssymb}
|
||||||
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
||||||
\usepackage{amssymb}
|
|
||||||
\usepackage{amsthm}
|
\usepackage{amsthm}
|
||||||
\usepackage{thmtools}
|
\usepackage{thmtools}
|
||||||
\usepackage{thmtools}
|
|
||||||
\usepackage{fancyvrb}
|
\usepackage{fancyvrb}
|
||||||
\usepackage{mathtools}
|
% \usepackage{mathtools}
|
||||||
\usepackage{amsmath}
|
% \usepackage{amsmath}
|
||||||
\usepackage{mathabx}
|
|
||||||
\usepackage{mathpartir}
|
\usepackage{mathpartir}
|
||||||
% packages for draft version
|
% packages for draft version
|
||||||
\usepackage{lineno}
|
\usepackage{lineno}
|
||||||
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
|
\usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes}
|
||||||
\usepackage{ifdraft}
|
\usepackage{unicode-math}
|
||||||
|
|
||||||
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
|
% mathpartir uses \atop, amsmath overrides it to throw a warning tho, so we override it back to the original!
|
||||||
\makeatletter
|
\makeatletter
|
||||||
\let\atop\@@atop
|
\let\atop\@@atop % chktex 1
|
||||||
\makeatother
|
\makeatother
|
||||||
|
|
||||||
\usepackage{tikz}
|
\usepackage{tikz}
|
||||||
\usetikzlibrary{cd, babel, quotes}
|
\usetikzlibrary{cd, babel, quotes}
|
||||||
\usepackage{quiver}
|
\usepackage{quiver}
|
||||||
\usepackage{stmaryrd} % for \llbracket and \rrbracket
|
% \usepackage{stmaryrd} % for \llbracket and \rrbracket
|
||||||
\usepackage{ifthen}
|
\usepackage{ifthen}
|
||||||
\usepackage{xspace}
|
\usepackage{xspace}
|
||||||
\usepackage[final]{hyperref}
|
\usepackage[final]{hyperref}
|
||||||
|
|
@ -108,7 +107,6 @@
|
||||||
|
|
||||||
|
|
||||||
\usepackage[scale=.8]{noto-mono}
|
\usepackage[scale=.8]{noto-mono}
|
||||||
\usepackage{unicode-math}
|
|
||||||
|
|
||||||
\usepackage{mathrsfs}
|
\usepackage{mathrsfs}
|
||||||
\usepackage{xargs}
|
\usepackage{xargs}
|
||||||
|
|
@ -225,8 +223,6 @@
|
||||||
}
|
}
|
||||||
\makeatother
|
\makeatother
|
||||||
|
|
||||||
\ifdraft{\linenumbers}
|
|
||||||
|
|
||||||
\include{src/01_introduction}
|
\include{src/01_introduction}
|
||||||
\include{src/02_preliminaries}
|
\include{src/02_preliminaries}
|
||||||
\include{src/03_agda-categories}
|
\include{src/03_agda-categories}
|
||||||
|
|
@ -241,6 +237,7 @@
|
||||||
|
|
||||||
\medskip
|
\medskip
|
||||||
|
|
||||||
|
\emergencystretch=1em
|
||||||
\printbibliography[heading=bibintoc]{}
|
\printbibliography[heading=bibintoc]{}
|
||||||
|
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|
|
||||||
|
|
@ -15,7 +15,7 @@
|
||||||
% `tikz-cd` is necessary to draw commutative diagrams.
|
% `tikz-cd` is necessary to draw commutative diagrams.
|
||||||
\RequirePackage{tikz-cd}
|
\RequirePackage{tikz-cd}
|
||||||
% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
|
% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
|
||||||
\RequirePackage{amssymb}
|
% \RequirePackage{amssymb}
|
||||||
% `calc` is necessary to draw curved arrows.
|
% `calc` is necessary to draw curved arrows.
|
||||||
\usetikzlibrary{calc}
|
\usetikzlibrary{calc}
|
||||||
% `pathmorphing` is necessary to draw squiggly arrows.
|
% `pathmorphing` is necessary to draw squiggly arrows.
|
||||||
|
|
@ -23,12 +23,12 @@
|
||||||
|
|
||||||
% A TikZ style for curved arrows of a fixed height, due to AndréC.
|
% A TikZ style for curved arrows of a fixed height, due to AndréC.
|
||||||
\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
|
\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
|
||||||
.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||||
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||||
.. (\tikztotarget)\tikztonodes}},
|
.. (\tikztotarget)\tikztonodes}},
|
||||||
settings/.code={\tikzset{quiver/.cd,#1}
|
settings/.code={\tikzset{quiver/.cd,#1}
|
||||||
\def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
|
\def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
|
||||||
quiver/.cd,pos/.initial=0.35,height/.initial=0}
|
quiver/.cd,pos/.initial=0.35,height/.initial=0}
|
||||||
|
|
||||||
% TikZ arrowhead/tail styles.
|
% TikZ arrowhead/tail styles.
|
||||||
\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
|
\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
|
||||||
|
|
|
||||||
|
|
@ -177,7 +177,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
|
||||||
\]
|
\]
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{lemma}
|
\begin{proposition}
|
||||||
Every exponential object \(X^Y\) satisfies the following properties:
|
Every exponential object \(X^Y\) satisfies the following properties:
|
||||||
|
|
||||||
\begin{enumerate}
|
\begin{enumerate}
|
||||||
|
|
@ -185,7 +185,7 @@ Categories with finite products (i.e.\ binary products and a terminal object) ar
|
||||||
\item \(curry(eval \circ (f \times id)) = f\) for any \(f : X \times Y \rightarrow Z\)
|
\item \(curry(eval \circ (f \times id)) = f\) for any \(f : X \times Y \rightarrow Z\)
|
||||||
\item \(curry\;f \circ g = curry(f \circ (g \times id))\) for any \(f : X \times Y \rightarrow Z, g : A \rightarrow X\)
|
\item \(curry\;f \circ g = curry(f \circ (g \times id))\) for any \(f : X \times Y \rightarrow Z, g : A \rightarrow X\)
|
||||||
\end{enumerate}
|
\end{enumerate}
|
||||||
\end{lemma}
|
\end{proposition}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
\begin{enumerate}
|
\begin{enumerate}
|
||||||
\item Let \(f, g : X \times Y \rightarrow Z\) and \(curry\;f = curry\;g\), then indeed
|
\item Let \(f, g : X \times Y \rightarrow Z\) and \(curry\;f = curry\;g\), then indeed
|
||||||
|
|
@ -394,8 +394,8 @@ This yields the category of programs for a Kleisli triple that is called the Kle
|
||||||
The laws of categories then follow from the Kleisli triple laws.
|
The laws of categories then follow from the Kleisli triple laws.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{theorem}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
|
\begin{proposition}[\cite{manes}] The notions of Kleisli triple and monad are equivalent.
|
||||||
\end{theorem}
|
\end{proposition}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
|
The crux of this proof is defining the triples, the proofs of the corresponding laws (functoriality, naturality, monad and Kleisli triple laws) are left out.
|
||||||
|
|
||||||
|
|
@ -505,10 +505,10 @@ to establish some notation and then describe how to obtain a monad via existence
|
||||||
\]
|
\]
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{theorem}\label{thm:freemonad}
|
\begin{proposition}\label{thm:freemonad}
|
||||||
Let \(U : \C \rightarrow \D \) be a forgetful functor.
|
Let \(U : \C \rightarrow \D \) be a forgetful functor.
|
||||||
If for every \(X \in \obj{\D}\) a free object \(FX \in \obj{C}\) exists then \((X \mapsto UFX, \eta : X \rightarrow UFX, \free{(f : X \rightarrow UFY)} : UFX \rightarrow UFY)\) is a Kleisli triple on \(\D \).
|
If for every \(X \in \obj{\D}\) a free object \(FX \in \obj{C}\) exists then \((X \mapsto UFX, \eta : X \rightarrow UFX, \free{(f : X \rightarrow UFY)} : UFX \rightarrow UFY)\) is a Kleisli triple on \(\D \).
|
||||||
\end{theorem}
|
\end{proposition}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We are left to check the laws of Kleisli triples.
|
We are left to check the laws of Kleisli triples.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -21,23 +21,15 @@ To ensure that programs are partial, we recall the following notion by Cockett a
|
||||||
\begin{definition}[Restriction Structure]
|
\begin{definition}[Restriction Structure]
|
||||||
A restriction structure on a category \(\mathcal{C}\) is a mapping \(dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)\) with the following properties:
|
A restriction structure on a category \(\mathcal{C}\) is a mapping \(dom : \mathcal{C}(X, Y) \rightarrow \mathcal{C}(X , X)\) with the following properties:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
f \circ (\tdom f) & = f\tag*{(R1)}\label{R1} \\
|
f \circ (\tdom f) & = f \\
|
||||||
(\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f)\tag*{(R2)}\label{R2} \\
|
(\tdom f) \circ (\tdom g) & = (\tdom g) \circ (\tdom f) \\
|
||||||
\tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f)\tag*{(R3)}\label{R3} \\
|
\tdom(g \circ (\tdom f)) & = (\tdom g) \circ (\tdom f) \\
|
||||||
(\tdom h) \circ f & = f \circ \tdom (h \circ f)\tag*{(R4)}\label{R4}
|
(\tdom h) \circ f & = f \circ \tdom (h \circ f)
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
for any \(X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\).
|
for any \(X, Y, Z \in \vert\mathcal{C}\vert, f : X \rightarrow Y, g : X \rightarrow Z, h: Y \rightarrow Z\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{lemma}
|
The morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
|
||||||
For any \(f : X \rightarrow Y\) the restriction morphism \(\tdom f\) is idempotent.
|
|
||||||
\end{lemma}
|
|
||||||
\begin{proof}
|
|
||||||
This follows by~\ref{R3} and~\ref{R1}:
|
|
||||||
\[\tdom f \circ \tdom f = \tdom (f \circ \tdom f) = \tdom f\tag*{\qedhere}\]
|
|
||||||
\end{proof}
|
|
||||||
|
|
||||||
The idempotent morphism \(\tdom f : X \rightarrow X\) represents the domain of definiteness of \(f : X \rightarrow Y\). In the category of partial functions this takes the following form:
|
|
||||||
|
|
||||||
\[
|
\[
|
||||||
(\tdom f)(x) = \begin{cases}
|
(\tdom f)(x) = \begin{cases}
|
||||||
|
|
@ -55,7 +47,7 @@ That is, \(\tdom f\) is only defined on values where \(f\) is defined and for th
|
||||||
|
|
||||||
For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) should be a restriction category.
|
For a suitable defined partiality monad \(T\) the Kleisli category \(\C^T\) should be a restriction category.
|
||||||
|
|
||||||
Lastly we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
|
Lastly, we also recall the following notion by Bucalo et al.~\cite{eqlm} which captures what it means for a monad to have no other side effect besides some sort of non-termination:
|
||||||
|
|
||||||
\begin{definition}[Equational Lifting Monad]\label{def:eqlm}
|
\begin{definition}[Equational Lifting Monad]\label{def:eqlm}
|
||||||
A commutative monad \(T\) is called an \textit{equational lifting monad} if the following diagram commutes:
|
A commutative monad \(T\) is called an \textit{equational lifting monad} if the following diagram commutes:
|
||||||
|
|
@ -110,7 +102,7 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
|
||||||
& (id + !) \circ dstl \circ (id \times (f + id)) \\
|
& (id + !) \circ dstl \circ (id \times (f + id)) \\
|
||||||
= \; & (id + !) \circ ((id \times f) + (id \times id)) \circ dstl \\
|
= \; & (id + !) \circ ((id \times f) + (id \times id)) \circ dstl \\
|
||||||
= \; & ((id \times f) + !) \circ dstl \\
|
= \; & ((id \times f) + !) \circ dstl \\
|
||||||
= \; & ((id \times f) + id) \circ (id + !) \circ dstl
|
= \; & ((id \times f) + id) \circ (id + !) \circ dstl.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
The other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness.
|
The other strength laws and commutativity can be proven by using simple properties of distributive categories, we added these proofs to the formalization for completeness.
|
||||||
|
|
@ -131,20 +123,20 @@ The endofunctor \(MX = X + 1\) extends to a monad by taking \(\eta_X = i_1 : X \
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\]
|
\]
|
||||||
|
|
||||||
This is easily proven by pre-composing with \(i_1\) and \(i_2\):
|
This is easily proven by pre-composing with \(i_1\) and \(i_2\), indeed
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
|
& (id\;+\;!) \circ dstl \circ \langle i_1 , i_1 \rangle
|
||||||
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle
|
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_1) \circ \langle i_1 , id \rangle
|
||||||
\\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle
|
\\=\;&(id\;+\;!) \circ i_1 \circ \langle i_1 , id \rangle
|
||||||
\\=\;&i_1 \circ \langle i_1 , id \rangle
|
\\=\;&i_1 \circ \langle i_1 , id \rangle,
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
|
& (id\;+\;!) \circ dstl \circ \langle i_2 , i_2 \rangle
|
||||||
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ \langle i_2 , id \rangle
|
\\=\;&(id\;+\;!) \circ dstl \circ (id \times i_2) \circ \langle i_2 , id \rangle
|
||||||
\\=\;&(id\;+\;!) \circ i_2 \circ \langle i_2 , id \rangle
|
\\=\;&(id\;+\;!) \circ i_2 \circ \langle i_2 , id \rangle
|
||||||
\\=\;&i_2 \;\circ \; ! \circ \langle i_2 , id \rangle
|
\\=\;&i_2 \;\circ \; ! \circ \langle i_2 , id \rangle
|
||||||
\\=\;&i_2 \;\circ \; !\tag*{\qedhere}
|
\\=\;&i_2 \;\circ \; !.\tag*{\qedhere}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
@ -152,7 +144,7 @@ In the setting of classical mathematics this monad is therefore sufficient for m
|
||||||
|
|
||||||
\section{The Delay Monad}
|
\section{The Delay Monad}
|
||||||
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
|
Capretta's delay monad~\cite{delay} is a coinductive datatype whose inhabitants can be viewed as suspended computations.
|
||||||
This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow D\;X\) and \(later : D\;X \rightarrow D\;X\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} or~\cite{delay}, for a type theoretical study of this monad.
|
This datatype is usually defined by the two coinductive constructors \(now : X \rightarrow DX\) and \(later : DX \rightarrow DX\), where \(now\) is for lifting a value inside a computation and \(later\) intuitively delays a computation by one time unit. See \autoref{chp:setoids} for a type theoretical study of this monad.
|
||||||
Categorically we obtain the delay monad by the final F-coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that these final F-coalgebras indeed yield a monad that is strong and commutative.
|
Categorically we obtain the delay monad by the final F-coalgebras \(DX = \nu A. X + A\), which we assume to exist. In this section we will show that these final F-coalgebras indeed yield a monad that is strong and commutative.
|
||||||
|
|
||||||
Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} the coalgebra structure \(out : DX \rightarrow X + DX\) is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: \(out^{-1} = [ now , later ] : X + DX \rightarrow DX\).
|
Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecursion and prove theorems by coinduction. By \autoref{lem:lambek} the coalgebra structure \(out : DX \rightarrow X + DX\) is an isomorphism, whose inverse can be decomposed into the two constructors mentioned before: \(out^{-1} = [ now , later ] : X + DX \rightarrow DX\).
|
||||||
|
|
@ -225,14 +217,13 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
|
||||||
\\=\;&(id + \coalg{\alpha} \circ i_2) \circ out
|
\\=\;&(id + \coalg{\alpha} \circ i_2) \circ out
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
Let us verify that \(f^*\) indeed satisfies the requisite property:
|
Let us verify that \(f^*\) indeed satisfies the requisite property:
|
||||||
|
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ \coalg{\alpha} \circ i_1
|
& out \circ \coalg{\alpha} \circ i_1
|
||||||
\\=\;&(id + \coalg{\alpha}) \circ \alpha \circ i_1
|
\\=\;&(id + \coalg{\alpha}) \circ \alpha \circ i_1
|
||||||
\\=\;&(id + \coalg{\alpha}) \circ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out
|
\\=\;&(id + \coalg{\alpha}) \circ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out
|
||||||
\\=\;&[ [ (id + \coalg{\alpha}) \circ i_1 , (id + \coalg{\alpha}) \circ i_2 \circ i_2 ] \circ out \circ f , (id + \coalg{\alpha}) \circ i_2 \circ i_1 ] \circ out
|
\\=\;&[ [ (id + \coalg{\alpha}) \circ i_1 , (id + \coalg{\alpha}) \circ i_2 \circ i_2 ] \circ out \circ f , (id + \coalg{\alpha}) \circ i_2 \circ i_1 ] \circ out
|
||||||
\\=\;&[ [ i_1 , i_2 \circ \coalg{\alpha} \circ i_2 ] \circ out \circ f , i_2 \circ \coalg{\alpha} \circ i_1 ] \circ out
|
\\=\;&[ [ i_1 , i_2 \circ \coalg{\alpha} \circ i_2 ] \circ out \circ f , i_2 \circ \coalg{\alpha} \circ i_1 ] \circ out
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
We are left to check uniqueness of \(f^*\). Let \(g : DX \rightarrow DY\) and \(out \circ g = [ out \circ f , i_2 \circ g ] \circ out\).
|
We are left to check uniqueness of \(f^*\). Let \(g : DX \rightarrow DY\) and \(out \circ g = [ out \circ f , i_2 \circ g ] \circ out\).
|
||||||
|
|
@ -245,39 +236,39 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
|
||||||
\\=\;&[ [ [ i_1 , i_2 \circ [g , id] \circ i_2 ] \circ out \circ f , i_2 \circ [g , id] \circ i_1 ] \circ out , (id + [g , id] \circ i_2) \circ out ]
|
\\=\;&[ [ [ i_1 , i_2 \circ [g , id] \circ i_2 ] \circ out \circ f , i_2 \circ [g , id] \circ i_1 ] \circ out , (id + [g , id] \circ i_2) \circ out ]
|
||||||
\\=\;&[ [ [ (id + [g , id]) \circ i_1 , (id + [g , id]) \circ i_2 \circ i_2 ] \circ out \circ f , (id + [g , id]) \circ i_2 \circ i_1 ] \circ out
|
\\=\;&[ [ [ (id + [g , id]) \circ i_1 , (id + [g , id]) \circ i_2 \circ i_2 ] \circ out \circ f , (id + [g , id]) \circ i_2 \circ i_1 ] \circ out
|
||||||
\\ \;&, (id + [g , id]) \circ (id + i_2) \circ out ]
|
\\ \;&, (id + [g , id]) \circ (id + i_2) \circ out ]
|
||||||
\\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ]
|
\\=\;&(id + [g , id]) \circ [ [ [ i_1 , i_2 \circ i_2 ] \circ out \circ f , i_2 \circ i_1 ] \circ out , (id + i_2) \circ out ].
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Thus, \([ g , id ] = \coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
|
Thus, \([ g , id ] = \coalg{\alpha}\) by uniqueness of \(\coalg{\alpha}\).
|
||||||
It follows: \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*\]
|
It follows that indeed \[g = [ g , id ] \circ i_1 =\;\coalg{\alpha} \circ i_1 = f^*.\]
|
||||||
\item[\ref{D3}] This follows immediately since \(\tau \) is the unique coalgebra morphism from \((X \times DY, dstl \circ (id \times out))\) into the terminal coalgebra \((D(X \times Y) , out)\).
|
\item[\ref{D3}] Take \(\tau := \coalg{dstl \circ (id \times out)} : X \times DY \rightarrow D(X \times Y)\), the requisite property then follows by definition.
|
||||||
\qedhere
|
\qedhere
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{lemma}
|
\begin{lemma}
|
||||||
The following properties follow from \autoref{lem:delay}:
|
The following properties of \(\mathbf{D}\) hold:
|
||||||
\begin{enumerate}
|
\begin{enumerate}
|
||||||
\item \(out \circ Df = (f + Df) \circ out\)
|
\item \(out \circ Df = (f + Df) \circ out\)
|
||||||
\item \(f^* = [ f , {(later \circ f)}^* ] \circ out\)
|
\item \(f^* = [ f , {(later \circ f)}^* ] \circ out\)
|
||||||
\item \(later \circ f^* = {(later \circ f)}^* = f^* \circ later\)
|
\item \(later \circ f^* = {(later \circ f)}^* = f^* \circ later\)
|
||||||
\end{enumerate}
|
\end{enumerate}
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof} These identities follow by use of \autoref{lem:delay}:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item[1.] Note that definitionally: \(Df = {(now \circ f)}^*\) for any \(f : X \rightarrow TY\). The statement is then simply a consequence of~\ref{D1} and~\ref{D2}:
|
\item[1.] Note that definitionally: \(Df = {(now \circ f)}^*\) for any \(f : X \rightarrow TY\). The statement is then simply a consequence of~\ref{D1} and~\ref{D2}:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ Df
|
& out \circ Df
|
||||||
\\=\;&out \circ {(now \circ f)}^*
|
\\=\;&out \circ {(now \circ f)}^*
|
||||||
\\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
|
\\=\;&[ out \circ now \circ f , i_2 \circ {(now \circ f)}^* ] \circ out\tag*{\ref{D2}}
|
||||||
\\=\;&(f + Df) \circ out\tag*{\ref{D1}}
|
\\=\;&(f + Df) \circ out.\tag*{\ref{D1}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item[2.] By uniqueness of \(f^*\) it suffices to show:
|
\item[2.] By uniqueness of \(f^*\) it suffices to show:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ [ f , {(later \circ f)}^* ] \circ out
|
& out \circ [ f , {(later \circ f)}^* ] \circ out
|
||||||
\\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
|
\\=\;&[ out \circ f , out \circ {(later \circ f)}^* ] \circ out
|
||||||
\\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
|
\\=\;&[out \circ f , [ out \circ later \circ f , i_2 \circ {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D2}}
|
||||||
\\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out\tag*{\ref{D1}}
|
\\=\;&[out \circ f , i_2 \circ [ f , {(later \circ f)}^* ] \circ out ] \circ out.\tag*{\ref{D1}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item[3.]
|
\item[3.]
|
||||||
These equations follow by monicity of \(out\):
|
These equations follow by monicity of \(out\):
|
||||||
|
|
@ -290,7 +281,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
|
||||||
\\=\;&i_2 \circ f^*\tag*{\ref{D1}}
|
\\=\;&i_2 \circ f^*\tag*{\ref{D1}}
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_2
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ later\tag*{\ref{D1}}
|
||||||
\\=\;&out \circ f^* \circ later \tag*{\ref{D2}}
|
\\=\;&out \circ f^* \circ later. \tag*{\ref{D2}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
Thus, the postulated properties have been proven.
|
Thus, the postulated properties have been proven.
|
||||||
|
|
@ -300,7 +291,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
|
||||||
\(\mathbf{D} = (D, now, {(-)}^*)\) is a Kleisli triple.
|
\(\mathbf{D} = (D, now, {(-)}^*)\) is a Kleisli triple.
|
||||||
\end{theorem}
|
\end{theorem}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We will now use the properties proven in Corollary~\ref{lem:delay} to prove the Kleisli triple laws:
|
We will now use the properties proven in \autoref{lem:delay} to prove the Kleisli triple laws:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item[\ref{K1}]
|
\item[\ref{K1}]
|
||||||
By uniqueness of \(now^*\) it suffices to show that \(out \circ id = [ out \circ now , i_2 \circ id ] \circ out\) which instantly follows by~\ref{D1}.
|
By uniqueness of \(now^*\) it suffices to show that \(out \circ id = [ out \circ now , i_2 \circ id ] \circ out\) which instantly follows by~\ref{D1}.
|
||||||
|
|
@ -309,7 +300,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
|
||||||
& out \circ f^* \circ now
|
& out \circ f^* \circ now
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}}
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ now\tag*{\ref{D2}}
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}}
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ i_1\tag*{\ref{D1}}
|
||||||
\\=\;&out \circ f
|
\\=\;&out \circ f.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item[\ref{K3}] Let \(f : Y \rightarrow Z, g : X \rightarrow Z\) to show \(f^* \circ g^* = {(f^* \circ g)}^*\) by uniqueness of \({(f^* \circ g)}^*\) it suffices to show:
|
\item[\ref{K3}] Let \(f : Y \rightarrow Z, g : X \rightarrow Z\) to show \(f^* \circ g^* = {(f^* \circ g)}^*\) by uniqueness of \({(f^* \circ g)}^*\) it suffices to show:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
|
|
@ -317,7 +308,7 @@ Since \(DX\) is defined as a final coalgebra, we can define morphisms via corecu
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}}
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ out \circ g^*\tag*{\ref{D2}}
|
||||||
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}}
|
\\=\;&[ out \circ f , i_2 \circ f^* ] \circ [ out \circ g , i_2 \circ g^* ] \circ out\tag*{\ref{D2}}
|
||||||
\\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out
|
\\=\;&[ [ out \circ f , i_2 \circ f^* ] \circ out \circ g , i_2 \circ f^* \circ g^* ] \circ out
|
||||||
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out\tag*{\ref{D2}}
|
\\=\;&[ out \circ f^* \circ g , i_2 \circ f^* \circ g^* ] \circ out.\tag*{\ref{D2}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
This concludes the proof.
|
This concludes the proof.
|
||||||
|
|
@ -386,19 +377,18 @@ Finality of the coalgebras \({(DX, out : DX \rightarrow X + DX)}_{X \in \obj{\C}
|
||||||
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
|
\arrow["{\pi_2 + id}", from=1-3, to=1-4]
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\]
|
\]
|
||||||
\item[\ref{S2}] We don't need coinduction to show \(\tau \circ (id \times now) = now\), but we need a small helper lemma:
|
\item[\ref{S2}] We don't need coinduction to show \(\tau \circ (id \times now) = now\), but we will first need to establish
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl \tag*{(\(\ast \))}\label{helper}
|
\tau \circ (id \times out^{-1}) = out^{-1} \circ (id + \tau) \circ dstl, \tag*{(\(\ast \))}\label{helper}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
which is a direct consequence of~\ref{D3}.
|
which is a direct consequence of~\ref{D3}.
|
||||||
With this the proof is straightforward:
|
With this we are done by
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \tau \circ (id \times now) \\
|
& \tau \circ (id \times now) \\
|
||||||
=\; & \tau \circ (id \times out^{-1}) \circ (id \times i_1) \\
|
=\; & \tau \circ (id \times out^{-1}) \circ (id \times i_1) \\
|
||||||
=\; & out^{-1} \circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}} \\
|
=\; & out^{-1} \circ (id + \tau) \circ dstl \circ (id \times i_1)\tag*{\ref*{helper}} \\
|
||||||
=\; & now
|
=\; & now.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
where the last step follows by \(dstl \circ (id \times i_1) = i_1\).
|
|
||||||
\item[\ref{S3}] We need to check \(\tau^* \circ \tau = \tau \circ (id \times id^*)\), the coalgebra for coinduction is:
|
\item[\ref{S3}] We need to check \(\tau^* \circ \tau = \tau \circ (id \times id^*)\), the coalgebra for coinduction is:
|
||||||
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
|
% https://q.uiver.app/#q=WzAsNixbMCwwLCJYIFxcdGltZXMgRERZIl0sWzAsMiwiRChYXFx0aW1lcyBZKSJdLFsxLDAsIlggXFx0aW1lcyAoRFkgKyBERFkpIl0sWzIsMCwiWCBcXHRpbWVzIERZICsgWCBcXHRpbWVzIEREWSJdLFsyLDIsIlggXFx0aW1lcyBZICsgRChYIFxcdGltZXMgWSkiXSxbMiwxLCJYIFxcdGltZXMgWSArIFggXFx0aW1lcyBERFkiXSxbMCwxLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsMiwiaWQgXFx0aW1lcyBvdXQiXSxbMiwzLCJkc3RsIl0sWzEsNCwib3V0Il0sWzUsNCwiaWQgKyBcXGNvYWxney19IiwyXSxbMyw1LCJbIChpZCArIChpZCBcXHRpbWVzIG5vdykpIFxcY2lyYyBkc3RsIFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpICwgaV8yIF0iLDJdXQ==
|
||||||
\[
|
\[
|
||||||
|
|
@ -456,8 +446,8 @@ To prove that \(\mathbf{D}\) is commutative we will use another proof principle
|
||||||
\end{corollary}
|
\end{corollary}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(g : X \rightarrow D(Y + X)\) be guarded by \(h : X \rightarrow Y + D(Y+X)\) and \(f, i : X \rightarrow DY\) be solutions of g.
|
Let \(g : X \rightarrow D(Y + X)\) be guarded by \(h : X \rightarrow Y + D(Y+X)\) and \(f, i : X \rightarrow DY\) be solutions of g.
|
||||||
It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows:
|
It suffices to show \({[ now , f ]}^* = {[ now , i ]}^*\), because then follows that
|
||||||
\[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i\]
|
\[f = {[ now , f ]}^* \circ g = {[ now , i ]}^* \circ g = i.\]
|
||||||
This is proven by coinduction using
|
This is proven by coinduction using
|
||||||
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
% https://q.uiver.app/#q=WzAsNSxbMCwxLCJEWSJdLFszLDEsIlkgKyBEWSJdLFswLDAsIkQoWSArIFgpIl0sWzEsMCwiKFkgKyBYKSArIEQoWStYKSJdLFszLDAsIlkgKyBEKFkrWCkiXSxbMCwxLCJvdXQiXSxbMiwzLCJvdXQiXSxbMyw0LCJbIFsgaV8xICwgaCBdICwgaV8yIF0iXSxbNCwxLCJpZCArIFxcY29hbGd7LX0iXSxbMiwwLCJcXGNvYWxney19IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
|
||||||
\[
|
\[
|
||||||
|
|
@ -489,7 +479,7 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item[\ref{tau1}] This is just~\ref{D3} restated.
|
\item[\ref{tau1}] This is just~\ref{D3} restated.
|
||||||
\item[\ref{sigma1}]
|
\item[\ref{sigma1}] Indeed, by use of~\ref{tau1}
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ \sigma
|
& out \circ \sigma
|
||||||
\\=\;&out \circ Dswap \circ \tau \circ swap
|
\\=\;&out \circ Dswap \circ \tau \circ swap
|
||||||
|
|
@ -497,19 +487,19 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
|
||||||
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ (id \times out) \circ swap \tag*{\ref{tau1}}
|
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ (id \times out) \circ swap \tag*{\ref{tau1}}
|
||||||
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ swap \circ (out \times id)
|
\\=\;&(swap + Dswap) \circ (id + \tau) \circ dstl \circ swap \circ (out \times id)
|
||||||
\\=\;&(swap + Dswap) \circ (id + \tau) \circ (swap + swap) \circ dstr \circ (out \times id)
|
\\=\;&(swap + Dswap) \circ (id + \tau) \circ (swap + swap) \circ dstr \circ (out \times id)
|
||||||
\\=\;&(id + \sigma) \circ dstr \circ (out \times id)
|
\\=\;&(id + \sigma) \circ dstr \circ (out \times id).
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item[\ref{tau2}] By monicity of \(out\):
|
\item[\ref{tau2}] By monicity of \(out\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ \tau \circ (id \times out^{-1})
|
& out \circ \tau \circ (id \times out^{-1})
|
||||||
\\=\;&(id + \tau) \circ dstl \circ (id \times out) \circ (id \times out^{-1})\tag*{\ref{tau1}}
|
\\=\;&(id + \tau) \circ dstl \circ (id \times out) \circ (id \times out^{-1})\tag*{\ref{tau1}}
|
||||||
\\=\;&(id + \tau) \circ dstl
|
\\=\;&(id + \tau) \circ dstl.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item[\ref{sigma2}] By monicity of \(out\):
|
\item[\ref{sigma2}] Again, by monicity of \(out\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ \sigma \circ (out^{-1} \times id)
|
& out \circ \sigma \circ (out^{-1} \times id)
|
||||||
\\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
|
\\=\;&(id + \sigma) \circ dstr \circ (out \times id) \circ (out^{-1} \times id)\tag*{\ref{sigma1}}
|
||||||
\\=\;&(id + \sigma) \circ dstr\tag*{\qedhere}
|
\\=\;&(id + \sigma) \circ dstr.\tag*{\qedhere}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
@ -521,27 +511,28 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
|
||||||
Using \autoref{cor:solution} it suffices to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of some guarded morphism \(g\).
|
Using \autoref{cor:solution} it suffices to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of some guarded morphism \(g\).
|
||||||
|
|
||||||
Let \(w = (dstr + dstr) \circ dstl \circ (out \times out)\) and take
|
Let \(w = (dstr + dstr) \circ dstl \circ (out \times out)\) and take
|
||||||
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\]
|
\[g = out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w.\]
|
||||||
\(g\) is trivially guarded by \([ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\).
|
\(g\) is trivially guarded by \([ id + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\).
|
||||||
|
|
||||||
We are left to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider:
|
We are left to show that both \(\tau^* \circ \sigma \) and \(\sigma^* \circ \tau \) are solutions of \(g\). Consider
|
||||||
|
|
||||||
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g \]
|
\[\tau^* \circ \sigma = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \tau^* \circ \sigma ] ] \circ w = {[ now , \tau^* \circ \sigma]}^* \circ g, \]
|
||||||
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g \]
|
and
|
||||||
|
\[\sigma^* \circ \tau = out^{-1} \circ [ id + \sigma , i_2 \circ [ \tau , later \circ \sigma^* \circ \tau ] ] \circ w = {[ now , \sigma^* \circ \tau]}^* \circ g. \]
|
||||||
|
|
||||||
The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\):
|
The last step in both equations can be proven generally for any \(f : DX \times DY \rightarrow D(X \times Y)\) using monicity of \(out\)
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
|
& out \circ {[ now , f ]}^* \circ out^{-1} \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w
|
||||||
\\=\; & [ out \circ [ now , f ] , i_2 \circ {[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
|
\\=\; & [ out \circ [ now , f ] , i_2 \circ {[ now , f ]}^* ] \circ [ i_1 + D i_1 \circ \sigma , i_2 \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D2}}
|
||||||
\\=\; & [ id + \sigma , i_2 \circ {[ now , f]}^* \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}
|
\\=\; & [ id + \sigma , i_2 \circ {[ now , f]}^* \circ [ D i_1 \circ \tau , later \circ now \circ i_2 ] ] \circ w\tag*{\ref{D1}}
|
||||||
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ now , f]}^* \circ later \circ now \circ i_2 ] ] \circ w
|
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ now , f]}^* \circ later \circ now \circ i_2 ] ] \circ w
|
||||||
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ later \circ now , later \circ f]}^* \circ now \circ i_2 ] ] \circ w
|
\\=\; & [ id + \sigma , i_2 \circ [ \tau , {[ later \circ now , later \circ f]}^* \circ now \circ i_2 ] ] \circ w
|
||||||
\\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w
|
\\=\; & [ id + \sigma , i_2 \circ [ \tau , later \circ f ] ] \circ w.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Let us now check the first step in the equation for \(\sigma^* \circ \tau \), the same step for \(\tau^* \circ \sigma \) is then symmetric.
|
Let us now check the first step in the equation for \(\sigma^* \circ \tau \), the same step for \(\tau^* \circ \sigma \) is then symmetric.
|
||||||
|
|
||||||
Again we proceed by monicity of \(out\):
|
Again, we proceed by monicity of \(out\), which yields
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& out \circ \sigma^* \circ \tau
|
& out \circ \sigma^* \circ \tau
|
||||||
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
|
\\=\;&[ out \circ \sigma , i_2 \circ \sigma^* ] \circ out \circ \tau\tag*{\ref{D2}}
|
||||||
|
|
@ -557,18 +548,17 @@ Let us record some facts that we will use to prove commutativity of \(\mathbf{D}
|
||||||
\\=\;&[ (id + \sigma), i_2 \circ {(out^{-1} \circ (id + \sigma))}^* \circ [D i_1 \circ \tau , D i_2 \circ \tau]] \circ (dstr + dstr) \circ dstl \circ (out \times out)
|
\\=\;&[ (id + \sigma), i_2 \circ {(out^{-1} \circ (id + \sigma))}^* \circ [D i_1 \circ \tau , D i_2 \circ \tau]] \circ (dstr + dstr) \circ dstl \circ (out \times out)
|
||||||
\\=\;&[ (id + \sigma), i_2 \circ [{(out^{-1} \circ i_1)}^* \circ \tau , {(out^{-1} \circ i_2 \circ \sigma)}^* \circ \tau]] \circ w
|
\\=\;&[ (id + \sigma), i_2 \circ [{(out^{-1} \circ i_1)}^* \circ \tau , {(out^{-1} \circ i_2 \circ \sigma)}^* \circ \tau]] \circ w
|
||||||
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , {(later \circ \sigma)}^* \circ \tau]] \circ w \tag*{\ref{K1}}
|
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , {(later \circ \sigma)}^* \circ \tau]] \circ w \tag*{\ref{K1}}
|
||||||
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w
|
\\=\;&[ (id + \sigma), i_2 \circ [ \tau , later \circ \sigma^* \circ \tau]] \circ w,
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
where
|
where
|
||||||
\[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
|
\[Ddstr \circ \tau = [ Di_1 \circ \tau , Di_2 \circ \tau ] \circ dstr \tag*{(*)}\label{Dcomm-helper}\]
|
||||||
is proven using epicness of \(dstr^{-1}\):
|
indeed follows by epicness of \(dstr^{-1}\):
|
||||||
|
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& Ddstr \circ \tau \circ dstr^{-1}
|
& Ddstr \circ \tau \circ dstr^{-1}
|
||||||
\\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
|
\\=\;&[ Ddstr \circ \tau \circ (i_1 \times id) , Ddstr \circ \tau \circ (i_2 \times id) ]
|
||||||
\\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
|
\\=\;&[ Ddstr \circ D(i_1 \times id) \circ \tau , Ddstr \circ D(i_2 \times id) \circ \tau ]
|
||||||
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ]\tag*{\qedhere}
|
\\=\;&[ Di_1 \circ \tau , Di_2 \circ \tau ].\tag*{\qedhere}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -40,8 +40,11 @@ The previous intuition gives rise to the following simpler definition that has b
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
In this setting the simpler \ref{law:folding} axiom replaces the sophisticated \ref{law:guardedcompositionality} axiom. % chktex 2
|
Note that the \ref{law:uniformity} axiom requires an identity to be proven, before it can be applied. % chktex 2
|
||||||
Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent, which is illustrated by the following Lemma. % chktex 2
|
However, we will omit these proofs in most parts of the thesis, since they mostly follow by simple rewriting on (co)products, the full proofs can be looked up in the accompanying formalization. % chktex 36
|
||||||
|
|
||||||
|
Now, in this setting the simpler \ref{law:folding} axiom replaces the sophisticated \ref{law:guardedcompositionality} axiom. % chktex 2
|
||||||
|
Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the \ref{law:folding} and \ref{law:guardedcompositionality} axioms are equivalent, which is partly illustrated by the following Lemma. % chktex 2
|
||||||
|
|
||||||
\begin{lemma}
|
\begin{lemma}
|
||||||
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
|
Every Elgot algebra \((A , {(-)}^\sharp)\) satisfies the following additional axioms
|
||||||
|
|
@ -51,7 +54,7 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
|
||||||
\\ for any \(f : X \rightarrow A + X, h : Y \rightarrow X + Y\),
|
\\ for any \(f : X \rightarrow A + X, h : Y \rightarrow X + Y\),
|
||||||
\item \customlabel{law:stutter}{\textbf{Stutter}}: \({(([ h , h ] + id) \circ f)}^\sharp = {(i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )}^\sharp \circ inr\)
|
\item \customlabel{law:stutter}{\textbf{Stutter}}: \({(([ h , h ] + id) \circ f)}^\sharp = {(i_1 \circ h , [ h + i_1 , i_2 \circ i_2 ] )}^\sharp \circ inr\)
|
||||||
\\ for any \(f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A\),
|
\\ for any \(f : X \rightarrow (Y + Y) + X, h : Y \rightarrow A\),
|
||||||
\item \customlabel{law:diamond}{\textbf{Diamond}}: \({((id + \Delta) \circ f)}^\sharp = {([ i_1 , ((id + \Delta) \circ f)^\sharp + id] \circ f)}^\sharp \)
|
\item \customlabel{law:diamond}{\textbf{Diamond}}: \({((id + \Delta) \circ f)}^\sharp = {([ i_1 , {((id + \Delta) \circ f)}^\sharp + id] \circ f)}^\sharp \)
|
||||||
\\ for any \(f : X \rightarrow A + (X + X)\).
|
\\ for any \(f : X \rightarrow A + (X + X)\).
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
|
|
@ -106,7 +109,7 @@ Indeed, for \(Id\)-guarded Elgot algebras with a trivial algebra structure, the
|
||||||
\item \ref{law:diamond}: Let \(h = [ i_1 \circ i_1 , i_2 + id ] \circ f\) and \(g = (id + \Delta) \circ f\). %chktex 2
|
\item \ref{law:diamond}: Let \(h = [ i_1 \circ i_1 , i_2 + id ] \circ f\) and \(g = (id + \Delta) \circ f\). %chktex 2
|
||||||
First, note that
|
First, note that
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
[ id , g^\sharp ] = {[ i_1 , (id + i_2) \circ g ]}^\sharp, \tag{\(\Asterisk\)}\label{diamond-helper}
|
[ id , g^\sharp ] = {[ i_1 , (id + i_2) \circ g ]}^\sharp, \tag{\(∗\)}\label{diamond-helper}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
by \ref{law:fixpoint} and \ref{law:uniformity}: % chktex 2
|
by \ref{law:fixpoint} and \ref{law:uniformity}: % chktex 2
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
|
|
@ -163,11 +166,11 @@ Let us now consider morphisms that are coherent with respect to the iteration op
|
||||||
Let \((A, {(-)}^{\sharp_a}), (B, {(-)}^{\sharp_b})\) be two Elgot algebras.
|
Let \((A, {(-)}^{\sharp_a}), (B, {(-)}^{\sharp_b})\) be two Elgot algebras.
|
||||||
|
|
||||||
A morphism \(f : X \times A \rightarrow B\) is called \textit{right iteration preserving} if
|
A morphism \(f : X \times A \rightarrow B\) is called \textit{right iteration preserving} if
|
||||||
\[f \circ (id \times h^{\sharp_a}) = ((f + id) \circ dstl \circ (id \times h))^{\sharp_b}\]
|
\[f \circ (id \times h^{\sharp_a}) = {((f + id) \circ dstl \circ (id \times h))}^{\sharp_b}\]
|
||||||
for any \(h : Y \rightarrow A + Y\).
|
for any \(h : Y \rightarrow A + Y\).
|
||||||
|
|
||||||
Symmetrically a morphism \(g : A \times X \rightarrow B\) is called \textit{left iteration preserving} if
|
Symmetrically a morphism \(g : A \times X \rightarrow B\) is called \textit{left iteration preserving} if
|
||||||
\[f \circ (h^{\sharp_a} \times id) = ((f + id) \circ dstr \circ (h \times id))^{\sharp_b}\]
|
\[f \circ (h^{\sharp_a} \times id) = {((f + id) \circ dstr \circ (h \times id))}^{\sharp_b}\]
|
||||||
for any \(h : Y \rightarrow A + Y\).
|
for any \(h : Y \rightarrow A + Y\).
|
||||||
|
|
||||||
Let us also consider the special case where \(X = 1\).
|
Let us also consider the special case where \(X = 1\).
|
||||||
|
|
@ -176,46 +179,46 @@ Let us now consider morphisms that are coherent with respect to the iteration op
|
||||||
for any \(h : Y \rightarrow A + Y\).
|
for any \(h : Y \rightarrow A + Y\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
The previous definition yields the category of Elgot algebras over a category \(\C \) and iteration preserving morphisms between these algebras. We call this category \(\elgotalgs{\C}\).
|
We will now study the category of Elgot algebras and iteration preserving morphisms that we call \(\elgotalgs{\C}\). Let us introduce notation for morphisms between Elgot algebras: we denote an Elgot algebra morphism \(f : (A , {(-)}^{\sharp_a}) \rightarrow (B,{(-)}^{\sharp_b})\) as \(f : A \hookrightarrow B\), where we omit stating the iteration operator.
|
||||||
|
|
||||||
\begin{lemma}
|
\begin{lemma}\label{lem:elgotalgscat}
|
||||||
\(\elgotalgs{\C}\) is a category.
|
\(\elgotalgs{\C}\) is a category.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
It suffices to show that the identity morphism in \(\C \) is iteration preserving and the composite of two iteration preserving morphisms is also iteration preserving.
|
It suffices to show that the identity morphism in \(\C \) is iteration preserving and the composite of two iteration preserving morphisms is also iteration preserving.
|
||||||
|
|
||||||
Let \((A , {(-)}^{\sharp_a}), (B , {(-)}^{\sharp_b}), (C , {(-)}^{\sharp_c})\) be Elgot algebras.
|
Let \(A, B\) and \(C\) be Elgot algebras.
|
||||||
The identity trivially satisfies
|
The identity trivially satisfies
|
||||||
\[id \circ f^{\sharp_a} = f^{\sharp_a} = {((id + id) \circ f)}^{\sharp_a}\]
|
\[id \circ f^{\sharp_a} = f^{\sharp_a} = {((id + id) \circ f)}^{\sharp_a}\]
|
||||||
for any \(f : X \rightarrow A + X\).
|
for any \(f : X \rightarrow A + X\).
|
||||||
Given two iteration preserving morphisms \(f : B \rightarrow C, g : A \rightarrow B\), the composite is iteration preserving since
|
Given two iteration preserving morphisms \(f : B \hookrightarrow C, g : A \hookrightarrow B\), the composite is iteration preserving since
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& f \circ g \circ h^{\sharp_a}
|
& f \circ g \circ h^{\sharp_a}
|
||||||
\\=\;& f \circ {((g + id) \circ h)}^{\sharp_b}
|
\\=\;& f \circ {((g + id) \circ h)}^{\sharp_b}
|
||||||
\\=\;&{((f + id) \circ (g + id) \circ h)}^{\sharp_c}
|
\\=\;&{((f + id) \circ (g + id) \circ h)}^{\sharp_c}
|
||||||
\\=\;&{(((f \circ g) + id) \circ h)}^{\sharp_c}
|
\\=\;&{((f \circ g + id) \circ h)}^{\sharp_c}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
for any \(h : X \rightarrow A + X\).
|
for any \(h : X \rightarrow A + X\).
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
Products and exponentials of Elgot algebras can be formed in a canonical way.
|
Products and exponentials of Elgot algebras can be formed in a canonical way, which is illustrated by the following two Lemmas.
|
||||||
|
|
||||||
\begin{lemma}\label{lem:elgotalgscat}
|
\begin{lemma}\label{lem:elgotalgscart}
|
||||||
If \(\C\) is a Cartesian category, so is \(\elgotalgs{\C}\).
|
If \(\C\) is a Cartesian category, so is \(\elgotalgs{\C}\).
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(1\) be the terminal object of \(\C \). Given \(f : X \rightarrow 1 + X\) we define the iteration \(f^\sharp =\;! : X \rightarrow 1\) as the unique morphism into the terminal object. The Elgot algebra laws follow instantly by uniqueness of \(!\) and \((1 , !)\) is the terminal Elgot algebra since for every Elgot algebra \(A\) the morphism \(! : A \rightarrow 1\) extends to a morphism between Elgot algebras by uniqueness. % chktex 40
|
Let \(1\) be the terminal object of \(\C \). Given \(f : X \rightarrow 1 + X\) we define the iteration \(f^\sharp =\;! : X \rightarrow 1\) as the unique morphism into the terminal object. The Elgot algebra laws follow instantly by uniqueness of \(!\) and \((1 , !)\) is the terminal Elgot algebra since for every Elgot algebra \(A\) the morphism \(! : A \rightarrow 1\) extends to a morphism between Elgot algebras by uniqueness. % chktex 40
|
||||||
|
|
||||||
Let \((A, {(-)}^{\sharp_a}) , (B, {(-)}^{\sharp_b}) \in \vert\elgotalgs{\C}\vert \) and \(A \times B\) be the product of \(A\) and \(B\) in \(\C \). Given \(f : X \rightarrow (A \times B) + X\) we define the iteration as:
|
Let \(A, B \in \vert\elgotalgs{\C}\vert \) and \(A \times B\) be the product of \(A\) and \(B\) in \(\C \). Given \(f : X \rightarrow (A \times B) + X\) we define the iteration as:
|
||||||
\[f^\sharp = \langle ((\pi_1 + id) \circ f)^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle : X \rightarrow A \times B\]
|
\[f^\sharp = \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle : X \rightarrow A \times B\]
|
||||||
Next we show that \((A \times B, {(-)}^\sharp)\) is indeed an Elgot algebra:
|
Now, we show that \(A \times B\) indeed constitutes an Elgot algebra:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item \textbf{Fixpoint}: Let \(f : X \rightarrow (A \times B) + X\). The requisite equation follows by the fixpoint identities of \(((\pi_1 + id) \circ f)^{\sharp_a}\) and \({((\pi_2 + id) \circ f)}^{\sharp_b}\):
|
\item \textbf{Fixpoint}: Let \(f : X \rightarrow (A \times B) + X\). The requisite equation follows by the fixpoint identities of \({((\pi_1 + id) \circ f)}^{\sharp_a}\) and \({((\pi_2 + id) \circ f)}^{\sharp_b}\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle
|
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle
|
||||||
\\=\;&\langle [ id , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ (\pi_1 + id) \circ f
|
\\=\;&\langle [ id , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ (\pi_1 + id) \circ f
|
||||||
\\ &, [ id , ((\pi_2 + id) \circ f)^{\sharp_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
|
\\ &, [ id , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ (\pi_2 + id) \circ f \rangle \tag{\ref{law:fixpoint}}
|
||||||
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ f , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ f \rangle
|
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] \circ f , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \circ f \rangle
|
||||||
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \rangle \circ f
|
\\=\;&\langle [ \pi_1 , {((\pi_1 + id) \circ f)}^{\sharp_a} ] , [ \pi_2 , {((\pi_2 + id) \circ f)}^{\sharp_b} ] \rangle \circ f
|
||||||
\\=\;&[ \langle \pi_1 , \pi_2 \rangle , \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle ] \circ f
|
\\=\;&[ \langle \pi_1 , \pi_2 \rangle , \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle ] \circ f
|
||||||
|
|
@ -230,12 +233,12 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
|
||||||
|
|
||||||
Then,~\ref{law:uniformity} of \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) with the previous two equations yields:
|
Then,~\ref{law:uniformity} of \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) with the previous two equations yields:
|
||||||
\begin{alignat*}{2}
|
\begin{alignat*}{2}
|
||||||
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_1 + id) \circ f)}^{\sharp_a} \rangle & & = {((\pi_1 + id) \circ g})^{\sharp_a} \circ h
|
& \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_1 + id) \circ f)}^{\sharp_a} \rangle & & = {((\pi_1 + id) \circ g)}^{\sharp_a} \circ h
|
||||||
\\&\langle {((\pi_2 + id) \circ f)}^{\sharp_b} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle &&= {((\pi_2 + id) \circ g)}^{\sharp_b} \circ h
|
\\&\langle {((\pi_2 + id) \circ f)}^{\sharp_b} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle &&= {((\pi_2 + id) \circ g)}^{\sharp_b} \circ h
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
This concludes the proof of:
|
This concludes the proof of:
|
||||||
\[ \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , ((\pi_2 + id) \circ f)^{\sharp_b} \rangle = \langle {((\pi_1 + id) \circ g)}^{\sharp_a} , {((\pi_2 + id) \circ g)}^{\sharp_b} \rangle \circ h \]
|
\[ \langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle = \langle {((\pi_1 + id) \circ g)}^{\sharp_a} , {((\pi_2 + id) \circ g)}^{\sharp_b} \rangle \circ h \]
|
||||||
\item \textbf{Folding}: Let \(f : X \rightarrow (A \times B) + X, h : Y \rightarrow X + Y\). We need to show:
|
\item \textbf{Folding}: Let \(f : X \rightarrow (A \times B) + X, h : Y \rightarrow X + Y\). We need to show:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \langle {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_a}
|
& \langle {((\pi_1 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_a}
|
||||||
|
|
@ -253,90 +256,94 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
|
||||||
and
|
and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& {((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_b}
|
& {((\pi_2 + id) \circ (\langle {((\pi_1 + id) \circ f)}^{\sharp_a} , {((\pi_2 + id) \circ f)}^{\sharp_b} \rangle + h))}^{\sharp_b}
|
||||||
\\=\;&{(((\pi_2 + id) \circ f)^{\sharp_b} + h)}^{\sharp_b}
|
\\=\;&{({((\pi_2 + id) \circ f)}^{\sharp_b} + h)}^{\sharp_b}
|
||||||
\\=\;&{[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]}^{\sharp_b}\tag{\ref{law:folding}}
|
\\=\;&{[ (id + i_1) \circ (\pi_2 + id) \circ f , i_2 \circ h ]}^{\sharp_b}\tag{\ref{law:folding}}
|
||||||
\\=\;&(\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b}
|
\\=\;&(\pi_2 + id) \circ {[ (id + i_1) \circ f , i_2 \circ h ]}^{\sharp_b}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
which concludes the proof of the folding law.
|
which concludes the proof of the folding law.
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
|
|
||||||
The product diagram of \(A \times B\) in \(\C\) then also holds in \(\elgotalgs{\C}\), we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism \(\langle f , g \rangle\) is iteration preserving for any \(f : (Z, {(-)}^{\sharp_z}) \rightarrow (X, {(-)}^{\sharp_x}), g : (Z, {(-)}^{\sharp_z}) \rightarrow (Y, {(-)}^{\sharp_y})\):
|
The product diagram of \(A \times B\) in \(\C\) then also holds in \(\elgotalgs{\C}\), we just have to check that the projections are iteration preserving, which follows instantly, and that the unique morphism \(\langle f , g \rangle\) is iteration preserving for any \(f : C \hookrightarrow A, g : C \rightarrow B\) where \(C \in \obj{\elgotalgs{\C}}\).
|
||||||
|
|
||||||
Let \(h : X \rightarrow E + X\) where \(E \in \obj{\elgotalgs{\C}}\). We use the fact that \(f, g\) are iteration preserving to show:
|
Let \(h : X \rightarrow C + X\). We use the fact that \(f\) and \(g\) are iteration preserving to show:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \langle f , g \rangle \circ (h^{\sharp_e})
|
& \langle f , g \rangle \circ (h^{\sharp_c})
|
||||||
\\=\;&\langle f \circ (h^{\sharp_e}) , g \circ (h^{\sharp_e}) \rangle
|
\\=\;&\langle f \circ (h^{\sharp_c}) , g \circ (h^{\sharp_c}) \rangle
|
||||||
\\=\;&\langle ((f + id) \circ h)^{\sharp_a} , ((g + id) \circ h)^{\sharp_b} \rangle
|
\\=\;&\langle {((f + id) \circ h)}^{\sharp_a} , {((g + id) \circ h)}^{\sharp_b} \rangle
|
||||||
\\=\;&\langle ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\sharp_a} , ((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)^{\sharp_b} \rangle
|
\\=\;&\langle {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_a} , {((\pi_1 + id) \circ (\langle f , g \rangle + id) \circ h)}^{\sharp_b} \rangle
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, we have shown that \(A \times B\) extends to a product in \(\elgotalgs{\C}\) and therefore \(\elgotalgs{\C}\) is Cartesian, assuming that \(\C\) is Cartesian.
|
Which confirms that \(\langle f , g \rangle\) is indeed iteration preserving. Thus, it follows that \(A \times B\) extends to a product in \(\elgotalgs{\C}\) and therefore \(\elgotalgs{\C}\) is Cartesian, if \(\C\) is Cartesian.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{lemma}\label{lem:elgotexp}
|
\begin{lemma}\label{lem:elgotexp}
|
||||||
Given \(X \in \obj{\C}\) and \((A, {(-)}^{\sharp_a}) \in \vert\elgotalgs{\C}\vert \). The exponential \(X^A\) (if it exists) can be equipped with an Elgot algebra structure.
|
Given \(X \in \obj{\C}\) and \(A \in \obj{\elgotalgs{\C}} \). The exponential \(X^A\) (if it exists) can be equipped with an Elgot algebra structure.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Take \(f^\sharp = curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a})\) as the iteration of some \(f : Z \rightarrow A^X + Z\).
|
Take \(f^\sharp = curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\) as the iteration of some \(f : Z \rightarrow A^X + Z\).
|
||||||
|
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item \textbf{Fixpoint}: Let \(f : Y \rightarrow X^A + Y\) with \(Y \in \obj{C}\). By uniqueness of \(f^\sharp = curry\;(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a})\) it suffices to show:
|
\item \textbf{Fixpoint}: Let \(f : Y \rightarrow X^A + Y\). We need to show that \(f^\sharp = [ id , f^\sharp ] \circ f\), which follows by uniqueness of \[f^\sharp = curry\;({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\] and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& eval \circ ([ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \circ f] \times id)
|
& eval \circ ([ id , curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ f \times id)
|
||||||
\\=\;&eval \circ [ id , curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)\tag*{\ref{hlp:elgot_exp_fixpoint}}
|
\\=\;&eval \circ [ id , curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)\tag*{\ref{hlp:elgot_exp_fixpoint}}
|
||||||
\\=\;&[ eval , eval \circ curry (((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr \circ (f \times id)
|
\\=\;&[ eval , eval \circ (curry ({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr \circ (f \times id)
|
||||||
\\=\;&[ eval , ((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} ] \circ dstr \circ (f \times id)
|
\\=\;&[ eval , {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} ] \circ dstr \circ (f \times id)
|
||||||
\\=\;&[ id , ((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
|
\\=\;&[ id , {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} ] \circ (eval + id) \circ dstr \circ (f \times id)
|
||||||
\\=\;&((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}\tag{\ref{law:fixpoint}}
|
\\=\;&{((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a},\tag{\ref{law:fixpoint}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
Where
|
where
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \times id
|
& [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \times id
|
||||||
\\= \;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr \tag*{(*)}\label{hlp:elgot_exp_fixpoint}
|
\\= \;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr \tag*{(*)}\label{hlp:elgot_exp_fixpoint}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
follows by post-composing with \(\pi_1\) and \(\pi_2\):
|
follows by post-composing with \(\pi_1\) and \(\pi_2\), indeed:
|
||||||
|
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \pi_1 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
|
& \pi_1 \circ [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr
|
||||||
\\=\;&[ \pi_1 , \pi_1 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
|
\\=\;&[ \pi_1 , \pi_1 \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr
|
||||||
\\=\;&[ \pi_1 , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \circ \pi_1 ] \circ dstr
|
\\=\;&[ \pi_1 , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \circ \pi_1 ] \circ dstr
|
||||||
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
|
\\=\;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ (\pi_1 + \pi_1) \circ dstr
|
||||||
\\=\;&[ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) ] \circ \pi_1
|
\\=\;&[ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) ] \circ \pi_1,
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \pi_2 \circ [ id , curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
|
& \pi_2 \circ [ id , curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id ] \circ dstr
|
||||||
\\=\;&[ \pi_2 , \pi_2 \circ curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id ] \circ dstr
|
\\=\;&[ \pi_2 , \pi_2 \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) ] \circ dstr
|
||||||
\\=\;&[ \pi_2 , \pi_2 ] \circ dstr
|
\\=\;&[ \pi_2 , \pi_2 ] \circ dstr
|
||||||
\\=\;&\pi_2
|
\\=\;&\pi_2.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item \textbf{Uniformity}: Let \(Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h) \circ f = g \circ h\). By uniqueness of \(f^\sharp = curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a})\) it suffices to show:
|
\item \textbf{Uniformity}: Let \(f : Y \rightarrow X^A + Y, g : Z \rightarrow X^A + Z, h : Y \rightarrow Z\) and \((id + h) \circ f = g \circ h\). Again, by uniqueness of \(f^\sharp = curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a})\) it suffices to show:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& ((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}
|
& {((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}
|
||||||
\\=\;&((eval + id) \circ dstr \circ (g \times id))^{\sharp_a} \circ (h \times id)\tag{\ref{law:uniformity}}
|
\\=\;&{((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \circ (h \times id)\tag{\ref{law:uniformity}}
|
||||||
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\sharp_a} \times id) \circ (h \times id)
|
\\=\;&eval \circ ({((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \times id) \circ (h \times id)
|
||||||
\\=\;&eval \circ (((eval + id) \circ dstr \circ (g \times id))^{\sharp_a} \circ h \times id)
|
\\=\;&eval \circ ({((eval + id) \circ dstr \circ (g \times id))}^{\sharp_a} \circ h \times id)
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
Note that the application of \ref{law:uniformity} requires:
|
Note that the application of \ref{law:uniformity} requires: % chktex 2
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (id + (h \times id)) \circ (eval + id) \circ dstr \circ (f \times id)
|
& (id + (h \times id)) \circ (eval + id) \circ dstr \circ (f \times id)
|
||||||
\\=\;&(eval + id) \circ (id + (h \times id)) \circ dstr \circ (f \times id)
|
\\=\;&(eval + id) \circ (id + (h \times id)) \circ dstr \circ (f \times id)
|
||||||
\\=\;&(eval + id) \circ dstr \circ (id \times h) \circ (id \times id) \circ (f \times id)
|
\\=\;&(eval + id) \circ dstr \circ (id \times h) \circ (id \times id) \circ (f \times id)
|
||||||
\\=\;&(eval + id) \circ dstr \circ (g \times id) \circ (h \times id)
|
\\=\;&(eval + id) \circ dstr \circ (g \times id) \circ (h \times id)
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\item \textbf{Folding}: Let \(Y, Z \in \obj{C}, f : Y \rightarrow X^A + Y, h : Y \rightarrow Z\).
|
\item \textbf{Folding}: Let \(f : Y \rightarrow X^A + Y, h : Y \rightarrow Z\). We need to show that
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (f^\sharp + h)^\sharp
|
& {(f^\sharp + h)}^\sharp
|
||||||
\\=\;&curry(((eval + id) \circ dstr \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) + h) \times id))^{\sharp_a})
|
\\=\;&curry({((eval + id) \circ dstr \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) + h) \times id))}^{\sharp_a})
|
||||||
\\=\;&curry(((eval + id) \circ ((curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id) + (h \times id)) \circ dstr)^{\sharp_a})
|
\\=\;&curry({((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a})
|
||||||
\\=\;&curry(((eval \circ (curry(((eval + id) \circ dstr \circ (f \times id))^{\sharp_a}) \times id) + (h \times id)) \circ dstr)^{\sharp_a})
|
\\=\;&{[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp.
|
||||||
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} + (h \times id)) \circ dstr)^{\sharp_a})
|
|
||||||
\\=\;&curry(((((eval + id) \circ dstr \circ (f \times id))^{\sharp_a} + dstr \circ (h \times id)))^{\sharp_a} \circ dstr)\tag{\ref{law:uniformity}}
|
|
||||||
\\=\;&curry([ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr)\tag{\ref{law:folding}}
|
|
||||||
\\=\;&curry(((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))^{\sharp_a})\tag{\ref{law:uniformity}}
|
|
||||||
\\=\;&[ (id + i_1) \circ f , i_2 \circ h ]^\sharp
|
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\
|
Indeed, we are done by:
|
||||||
The second application of~\ref{law:uniformity} is non-trivial, using epicness of \(dstr^{-1}\):
|
\begin{alignat*}{1}
|
||||||
|
& {((eval + id) \circ dstr \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) + h) \times id))}^{\sharp_a}
|
||||||
|
\\=\;&{((eval + id) \circ ((curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) + (h \times id)) \circ dstr)}^{\sharp_a}
|
||||||
|
\\=\;&{((eval \circ (curry({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a}) \times id) + (h \times id)) \circ dstr)}^{\sharp_a}
|
||||||
|
\\=\;&{(({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} + (h \times id)) \circ dstr)}^{\sharp_a}
|
||||||
|
\\=\;&{(({((eval + id) \circ dstr \circ (f \times id))}^{\sharp_a} + dstr \circ (h \times id)))}^{\sharp_a} \circ dstr\tag{\ref{law:uniformity}}
|
||||||
|
\\=\;&[ (id + i_1) \circ (eval + id) \circ dstr \circ (f \times id) , i_2 \circ dstr \circ (h \times id) ] \circ dstr\tag{\ref{law:folding}}
|
||||||
|
\\=\;&{((eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id))}^{\sharp_a}.\tag{\ref{law:uniformity}}
|
||||||
|
\end{alignat*}
|
||||||
|
Note that the second application of~\ref{law:uniformity} is non-trivial, using epicness of \(dstr^{-1}\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ dstr^{-1}
|
& (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ dstr^{-1}
|
||||||
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_1 \times id)
|
\\=\;&[ (id + dstr) \circ (eval + id) \circ dstr \circ ([ (id + i_1) \circ f , i_2 \circ h ] \times id) \circ (i_1 \times id)
|
||||||
|
|
@ -354,7 +361,7 @@ Products and exponentials of Elgot algebras can be formed in a canonical way.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\section{The Initial (Strong) Pre-Elgot Monad}
|
\section{The Initial (Strong) Pre-Elgot Monad}
|
||||||
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial strong pre-Elgot monad.
|
In this section we will study the monad that arises from existence of all free Elgot algebras. We will show that this is an equational lifting monad and also the initial strong pre-Elgot monad. Starting in this section we will now omit indices of the iteration operator of Elgot algebras for the sake of readability.
|
||||||
|
|
||||||
Let us first recall the following notion that was introduced in~\cite{elgotmonad} and reformulated in~\cite{uniformelgot}.
|
Let us first recall the following notion that was introduced in~\cite{elgotmonad} and reformulated in~\cite{uniformelgot}.
|
||||||
\begin{definition}[Elgot Monad]
|
\begin{definition}[Elgot Monad]
|
||||||
|
|
@ -367,13 +374,13 @@ Let us first recall the following notion that was introduced in~\cite{elgotmonad
|
||||||
\\ for any \(f : X \rightarrow T(Y + X)\),
|
\\ for any \(f : X \rightarrow T(Y + X)\),
|
||||||
\item \textbf{Uniformity}: \(f \circ h = T(id + h)\) implies \(f^\dag \circ g = g^\dag\)
|
\item \textbf{Uniformity}: \(f \circ h = T(id + h)\) implies \(f^\dag \circ g = g^\dag\)
|
||||||
\\ for any \(f : X \rightarrow T(Y + X), g : Z \rightarrow T(Y + Z), h : Z \rightarrow X\),
|
\\ for any \(f : X \rightarrow T(Y + X), g : Z \rightarrow T(Y + Z), h : Z \rightarrow X\),
|
||||||
\item \textbf{Naturality}: \(g^* \circ f^\dag = {({[(Ti_1 \circ g , \eta \circ i_2 ]}^* \circ f)}^\dag\)
|
\item \textbf{Naturality}: \(g^* \circ f^\dag = {({[ Ti_1 \circ g , \eta \circ i_2 ]}^* \circ f)}^\dag\)
|
||||||
\\ for any \(f : X \rightarrow T(Y + X), g : Y \rightarrow TZ\),
|
\\ for any \(f : X \rightarrow T(Y + X), g : Y \rightarrow TZ\),
|
||||||
\item \textbf{Codiagonal}: \({f^\dag}^\dag = {(T[id , i_2] \circ f)}^\dag\)
|
\item \textbf{Codiagonal}: \({f^\dag}^\dag = {(T[id , i_2] \circ f)}^\dag\)
|
||||||
\\ for any \(f : X \rightarrow T((Y + X) + X)\).
|
\\ for any \(f : X \rightarrow T((Y + X) + X)\).
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
If the monad \(\mathbf{T}\) is strong with strength \(\tau\) and \(\tau \circ (id \times f^\dag) = {(Tdstl \circ \tau \circ (id \times f)}^\dag\) for any \(f : X \rightarrow T(Y+X)\), then \(\mathbf{T}\) is a strong Elgot monad.
|
If the monad \(\mathbf{T}\) is strong with strength \(\tau\) and \(\tau \circ (id \times f^\dag) = {(Tdstl \circ \tau \circ (id \times f))}^\dag\) for any \(f : X \rightarrow T(Y+X)\), then \(\mathbf{T}\) is a strong Elgot monad.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
We regard Elgot monads as minimal semantic structures for interpreting side-effecting while loops, as has been argued in~\cite{goncharov2018unguarded, goncharov2017unifying}.
|
We regard Elgot monads as minimal semantic structures for interpreting side-effecting while loops, as has been argued in~\cite{goncharov2018unguarded, goncharov2017unifying}.
|
||||||
|
|
@ -382,7 +389,7 @@ The following notion has been introduced in~\cite{uniformelgot} as a weaker appr
|
||||||
\begin{definition}[Pre-Elgot Monad]
|
\begin{definition}[Pre-Elgot Monad]
|
||||||
A monad \(\mathbf{T}\) is called pre-Elgot if every \(TX\) extends to an Elgot algebra such that for every \(f : X \rightarrow TY\) the Kleisli lifting \(f^* : TX \rightarrow TY\) is iteration preserving.
|
A monad \(\mathbf{T}\) is called pre-Elgot if every \(TX\) extends to an Elgot algebra such that for every \(f : X \rightarrow TY\) the Kleisli lifting \(f^* : TX \rightarrow TY\) is iteration preserving.
|
||||||
|
|
||||||
If \(\mathbf{T}\) is additionally strong and the strength \(\tau \) is right iteration preserving we call it strong pre-Elgot.
|
If the monad \(\mathbf{T}\) is additionally strong and the strength \(\tau \) is right iteration preserving we call \(\mathbf{T}\) strong pre-Elgot.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
(Strong) pre-Elgot monads form a subcategory of \(\monads{\C}\) where objects are (strong) pre-Elgot monads and morphisms between pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:monadmorphism} such that additionally each \(\alpha_X\) is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:strongmonadmorphism} such that each \(\alpha_X\) is iteration preserving. We call these categories \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) respectively.
|
(Strong) pre-Elgot monads form a subcategory of \(\monads{\C}\) where objects are (strong) pre-Elgot monads and morphisms between pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:monadmorphism} such that additionally each \(\alpha_X\) is iteration preserving. Similarly, morphisms between strong pre-Elgot monads are natural transformations \(\alpha \) as in \autoref{def:strongmonadmorphism} such that each \(\alpha_X\) is iteration preserving. We call these categories \(\preelgot{\C}\) and \(\strongpreelgot{\C}\) respectively.
|
||||||
|
|
@ -443,16 +450,16 @@ A symmetrical variant of the previous definition is sometimes useful.
|
||||||
\begin{lemma}
|
\begin{lemma}
|
||||||
Definitions~\ref{def:rightstablefreeelgot} and~\ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
|
Definitions~\ref{def:rightstablefreeelgot} and~\ref{def:leftstablefreeelgot} are equivalent in the sense that they imply each other.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof} Let \((KY, {(-)}^{\sharp_y})\) be a left stable free Elgot algebra on \(Y \in \obj{\C}\). Furthermore, let \(A \in \elgotalgs{\C}, X \in \obj{\C}, f : Y \times X \rightarrow A\).
|
\begin{proof} Let \(KY\) be a left stable free Elgot algebra on \(Y \in \obj{\C}\). Furthermore, let \(A\) be an Elgot algebra and \(X \in \obj{\C}, f : Y \times X \rightarrow A\).
|
||||||
|
|
||||||
We take \(\rs{f} := \ls{f \circ swap} \circ swap\), which is indeed right iteration preserving, since
|
We take \(\rs{f} := \ls{f \circ swap} \circ swap\), which is indeed right iteration preserving, since
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \rs{f} \circ (id \times h^{\sharp_y})
|
& \rs{f} \circ (id \times h^\sharp)
|
||||||
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times h^{\sharp_y})
|
\\=\;&\ls{f \circ swap} \circ swap \circ (id \times h^\sharp)
|
||||||
\\=\;&\ls{f \circ swap} \circ (h^{\sharp_y} \times id) \circ swap
|
\\=\;&\ls{f \circ swap} \circ (h^\sharp \times id) \circ swap
|
||||||
\\=\;&((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))^{\sharp_a} \circ swap
|
\\=\;&{((\ls{f \circ swap} + id) \circ dstr \circ (id \times h))}^\sharp \circ swap
|
||||||
\\=\;&(((\ls{f \circ swap} \circ swap) + id) \circ dstl \circ (id \times h))^{\sharp_a}\tag{\ref{law:uniformity}}
|
\\=\;&{((\ls{f \circ swap} \circ swap + id) \circ dstl \circ (id \times h))}^\sharp\tag{\ref{law:uniformity}}
|
||||||
\\=\;&(((\rs{f} + id) \circ dstl \circ (id \times h))^{\sharp_a},
|
\\=\;&{((\rs{f} + id) \circ dstl \circ (id \times h))}^\sharp,
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
|
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
|
||||||
|
|
||||||
|
|
@ -484,10 +491,10 @@ A symmetrical variant of the previous definition is sometimes useful.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
and
|
and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& g \circ swap \circ (h^{\sharp_y} \times id)
|
& g \circ swap \circ (h^\sharp \times id)
|
||||||
\\=\;&g \circ (id \times h^{\sharp_y}) \circ swap
|
\\=\;&g \circ (id \times h^\sharp) \circ swap
|
||||||
\\=\;&((g + id) \circ dstl \circ (id \times h))^{\sharp_a} \circ swap
|
\\=\;&{((g + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
|
||||||
\\=\;&(((g \circ swap) + id) \circ dstr \circ (h \times id))^{\sharp_a},\tag{\ref{law:uniformity}}
|
\\=\;&{((g \circ swap + id) \circ dstr \circ (h \times id))}^\sharp,\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
|
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\).
|
||||||
|
|
||||||
|
|
@ -499,34 +506,34 @@ A symmetrical variant of the previous definition is sometimes useful.
|
||||||
% \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
|
% \\=\;&(g + id) \circ dstl \circ (id \times h) \circ swap.
|
||||||
% \end{alignat*}
|
% \end{alignat*}
|
||||||
|
|
||||||
This concludes one direction of the proof that left stability and right stability imply each other, the other direction follows symmetrically.
|
This concludes one direction of the proof, the other direction follows symmetrically.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
In a less general setting stability would indeed follow automatically.
|
In a less general setting stability would indeed follow automatically.
|
||||||
|
|
||||||
\begin{theorem}\label{thm:stability}
|
\begin{lemma}\label{thm:stability}
|
||||||
In a Cartesian closed category every free Elgot algebra is stable.
|
In a Cartesian closed category every free Elgot algebra is stable.
|
||||||
\end{theorem}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(\C\) be Cartesian closed and let \((KX, {(-)}^\sharp, \free{(-)})\) be a free Elgot algebra on some \(X \in \obj{\C}\).
|
Let \(\C\) be Cartesian closed and let \(KX\) be a free Elgot algebra on some \(X \in \obj{\C}\).
|
||||||
|
|
||||||
To show left stability of \(KX\) we define \(\ls{f} := eval \circ (\free{curry\;f} \times id)\) for any \(X \in \obj{\C}, A \in \vert\elgotalgs{\C}\vert\), and \(f : Y \times X \rightarrow A\).
|
To show left stability of \(KX\) we define \(\ls{f} := eval \circ (\free{curry\;f} \times id)\) for any \(X \in \obj{\C}\), \(A \in \vert\elgotalgs{\C}\vert\), and \(f : Y \times X \rightarrow A\).
|
||||||
We will now verify that this does indeed satisfy the requisite properties, i.e.
|
We will now verify that this does indeed satisfy the requisite properties, i.e.
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& eval \circ (\free{curry\;f} \times id) \circ (\eta \times id)
|
& eval \circ (\free{curry\;f} \times id) \circ (\eta \times id)
|
||||||
\\=\;&eval \circ ((\free{curry\;f} \circ \eta) \times id)
|
\\=\;&eval \circ (\free{curry\;f} \circ \eta \times id)
|
||||||
\\=\;&eval \circ (curry\;f) \times id)
|
\\=\;&eval \circ (curry\;f \times id)
|
||||||
\\=\;&f
|
\\=\;&f
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
and for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\):
|
and for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& eval \circ (\free{curry\;f} \times id) \circ (h^{\sharp_a} \times id)
|
& eval \circ (\free{curry\;f} \times id) \circ (h^\sharp \times id)
|
||||||
\\=\;&eval \circ ((\free{curry\;f} \circ h^{\sharp_a}) \times id)
|
\\=\;&eval \circ (\free{curry\;f} \circ h^\sharp \times id)
|
||||||
\\=\;&eval \circ (curry(((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\sharp_b})) \times id)
|
\\=\;&eval \circ (curry({((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))}^\sharp) \times id)
|
||||||
\\=\;&((eval + id) \circ dstr \circ (((\free{curry\;f} + id) \circ h) \times id))^{\sharp_b}
|
\\=\;&{((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \circ h \times id))}^\sharp
|
||||||
\\=\;&((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))^{\sharp_b}
|
\\=\;&{((eval + id) \circ dstr \circ ((\free{curry\;f} + id) \times id) \circ (h \times id))}^\sharp
|
||||||
\\=\;&((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))^{\sharp_b}
|
\\=\;&{((eval + id) \circ ((\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))}^\sharp
|
||||||
\\=\;&(((eval \circ (\free{curry\;f} \times id)) + id) \circ dstr \circ (h \times id))^{\sharp_b}.
|
\\=\;&{((eval \circ (\free{curry\;f} \times id) + id) \circ dstr \circ (h \times id))}^\sharp.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Lastly, we need to check uniqueness of \(\ls{f}\). Let us consider a left iteration preserving morphism \(g : KY \times X \rightarrow A\) that satisfies \(g \circ (\eta \times id) = f\). Since \(curry\) is an injective mapping it suffices to show that
|
Lastly, we need to check uniqueness of \(\ls{f}\). Let us consider a left iteration preserving morphism \(g : KY \times X \rightarrow A\) that satisfies \(g \circ (\eta \times id) = f\). Since \(curry\) is an injective mapping it suffices to show that
|
||||||
|
|
@ -540,13 +547,13 @@ In a less general setting stability would indeed follow automatically.
|
||||||
|
|
||||||
Indeed,
|
Indeed,
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& curry\;g \circ h^{\sharp}
|
& curry\;g \circ h^\sharp
|
||||||
\\=\;&curry\;(g \circ (h^{\sharp} \times id))
|
\\=\;&curry\;(g \circ (h^\sharp \times id))
|
||||||
\\=\;&curry\;(((g + id) \circ dstr \circ (h \times id))^{\sharp_a})
|
\\=\;&curry\;({((g + id) \circ dstr \circ (h \times id))}^\sharp)
|
||||||
\\=\;&curry\;((((eval \circ (curry\; g \times id)) + id) \circ dstr \circ (h \times id))^{\sharp_a})
|
\\=\;&curry\;({((eval \circ (curry\; g \times id) + id) \circ dstr \circ (h \times id))}^\sharp)
|
||||||
\\=\;&curry\;(((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))^{\sharp_a})
|
\\=\;&curry\;({((eval + id) \circ ((curry\; g \times id) + id) \circ dstr \circ (h \times id))}^\sharp)
|
||||||
\\=\;&curry\;(((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))^{\sharp_a})
|
\\=\;&curry\;({((eval + id) \circ dstr \circ ((curry\;g + id) \times id) \circ (h \times id))}^\sharp)
|
||||||
\\=\;&curry\;(((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))^{\sharp_a})
|
\\=\;&curry\;({((eval + id) \circ dstr \circ (((curry\;g + id) \circ h) \times id))}^\sharp)
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\), and
|
for any \(Z \in \obj{\C}, h : Z \rightarrow KY + Z\), and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
|
|
@ -555,7 +562,7 @@ In a less general setting stability would indeed follow automatically.
|
||||||
\\=\;&curry\;f
|
\\=\;&curry\;f
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
This completes the proof.
|
Which completes the proof.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
For the rest of this chapter we will assume every \(KX\) to exist and be stable. Under these assumptions we show that \(\mathbf{K}\) is an equational lifting monad and in fact the initial strong pre-Elgot monad.
|
For the rest of this chapter we will assume every \(KX\) to exist and be stable. Under these assumptions we show that \(\mathbf{K}\) is an equational lifting monad and in fact the initial strong pre-Elgot monad.
|
||||||
|
|
@ -599,9 +606,9 @@ Of course there is also a symmetric version of this.
|
||||||
\(\mathbf{K}\) is a strong monad.
|
\(\mathbf{K}\) is a strong monad.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We define strength as \(\tau = \rs{(\eta : X \times Y \rightarrow K(X \times Y))} : X \times KY \rightarrow K(X \times Y)\). Note that \(\tau\) is right iteration preserving by definition and \(\tau \circ (id \times \eta) = \eta\).
|
We define strength as \(\tau = \rs{(\eta : X \times Y \rightarrow K(X \times Y))} : X \times KY \rightarrow K(X \times Y)\). Note that by definition \(\tau\) is right iteration preserving and \(\tau \circ (id \times \eta) = \eta\).
|
||||||
|
|
||||||
Most of the requisite proofs will be done by right-stability, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
|
Most of the requisite proofs will be done by right-stability using \autoref{rem:proofbystability}, i.e.\ to prove an identity we need to give a unifying morphism such that the requisite diagram commutes, and we need to show that both sides of the identity are right iteration preserving. The proofs of commutativity follow by easy rewriting and are thus deferred to the formalization. The proofs of right iteration preservation follow in most cases instantly since the morphisms are composed of (right) iteration preserving morphisms but in non-trivial cases we will give the full proof.
|
||||||
|
|
||||||
Naturality of \(\tau \) follows by:
|
Naturality of \(\tau \) follows by:
|
||||||
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJBIFxcdGltZXMgS0IiXSxbMCwzLCJBIFxcdGltZXMgQiJdLFsxLDIsIksoQSBcXHRpbWVzIEIpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMywwLCJYIFxcdGltZXMgS1kiXSxbMSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzAsMiwiXFx0YXUiLDJdLFsyLDMsIksoZlxcdGltZXMgZykiLDJdLFswLDQsImYgXFx0aW1lcyBLZyJdLFs0LDMsIlxcdGF1Il0sWzEsMywiXFxldGEgXFxjaXJjIChmIFxcdGltZXMgZykiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
||||||
|
|
@ -623,9 +630,9 @@ Of course there is also a symmetric version of this.
|
||||||
Notably, \(\tau \circ (f \times Kg)\) is right iteration preserving, since for any \(Z : \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
|
Notably, \(\tau \circ (f \times Kg)\) is right iteration preserving, since for any \(Z : \obj{\C}\) and \(h : Z \rightarrow KY + Z\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \tau \circ (f \times Kg) \circ (id \times h^\sharp)
|
& \tau \circ (f \times Kg) \circ (id \times h^\sharp)
|
||||||
\\=\;&\tau \circ (f \times ((Kg + id) \circ h)^\sharp)
|
\\=\;&\tau \circ (f \times {((Kg + id) \circ h)}^\sharp)
|
||||||
\\=\;&((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))^\sharp \circ (f \times id)
|
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((Kg + id) \circ h)))}^\sharp \circ (f \times id)
|
||||||
\\=\;&(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))^\sharp.\tag{\ref{law:uniformity}}
|
\\=\;&{(((\tau \circ (f \times Kg)) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
% where uniformity is justified by
|
% where uniformity is justified by
|
||||||
|
|
@ -650,7 +657,7 @@ Of course there is also a symmetric version of this.
|
||||||
Let us now check the strength laws.
|
Let us now check the strength laws.
|
||||||
|
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item[\ref{S1}] Note that for \(K\pi_2 \circ \tau = \pi_2\) holds more generally for any \(X, Y \in \obj{\C}\), instead of just for \(X = 1\):
|
\item[\ref{S1}] Note that for \(\mathbf{K}\), the identity \(K\pi_2 \circ \tau = \pi_2\) holds more generally for any \(X, Y \in \obj{\C}\), instead of just for \(X = 1\), proven by right-stability, using:
|
||||||
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgS1kiXSxbMiwwLCJLKFhcXHRpbWVzIFkpIl0sWzIsMiwiS1kiXSxbMCwyLCJYIFxcdGltZXMgWSJdLFswLDEsIlxcdGF1Il0sWzEsMiwiS1xccGlfMiJdLFswLDIsIlxccGlfMiIsMl0sWzMsMCwiaWQgXFx0aW1lcyBcXGV0YSIsMl0sWzMsMiwiXFxldGEgXFxjaXJjIFxccGlfMiIsMl1d
|
||||||
\[
|
\[
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
|
|
@ -666,7 +673,7 @@ Of course there is also a symmetric version of this.
|
||||||
\]
|
\]
|
||||||
|
|
||||||
\item[\ref{S2}] As already mentioned, \(\tau \circ (id \times \eta) = \eta\) follows by definition of \(\tau\).
|
\item[\ref{S2}] As already mentioned, \(\tau \circ (id \times \eta) = \eta\) follows by definition of \(\tau\).
|
||||||
\item[\ref{S3}] To show that \(\tau \circ (id \times \mu) = \tau^* \circ \tau\), consider:
|
\item[\ref{S3}] To show that \(\tau \circ (id \times \mu) = \tau^* \circ \tau\), we will proceed by right-stability using:
|
||||||
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS0tZIl0sWzMsMCwiWCBcXHRpbWVzIEtZIl0sWzMsMiwiSyhYXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFswLDMsIlggXFx0aW1lcyBLWSJdLFswLDEsImlkIFxcdGltZXMgXFxtdSIsMl0sWzEsMiwiXFx0YXUiLDJdLFswLDMsIlxcdGF1Il0sWzMsMiwiXFx0YXVeKiJdLFs0LDAsImlkIFxcdGltZXMgXFxldGEiLDAseyJjdXJ2ZSI6LTJ9XSxbNCwyLCJcXHRhdSIsMCx7ImN1cnZlIjoyfV1d
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS0tZIl0sWzMsMCwiWCBcXHRpbWVzIEtZIl0sWzMsMiwiSyhYXFx0aW1lcyBZKSJdLFsxLDIsIksoWCBcXHRpbWVzIEtZKSJdLFswLDMsIlggXFx0aW1lcyBLWSJdLFswLDEsImlkIFxcdGltZXMgXFxtdSIsMl0sWzEsMiwiXFx0YXUiLDJdLFswLDMsIlxcdGF1Il0sWzMsMiwiXFx0YXVeKiJdLFs0LDAsImlkIFxcdGltZXMgXFxldGEiLDAseyJjdXJ2ZSI6LTJ9XSxbNCwyLCJcXHRhdSIsMCx7ImN1cnZlIjoyfV1d
|
||||||
\[
|
\[
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
|
|
@ -682,7 +689,7 @@ Of course there is also a symmetric version of this.
|
||||||
\arrow["\tau", curve={height=12pt}, from=4-1, to=3-4]
|
\arrow["\tau", curve={height=12pt}, from=4-1, to=3-4]
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\]
|
\]
|
||||||
\item[\ref{S4}] Lastly, consider the following diagram:
|
\item[\ref{S4}] Lastly, consider the following diagram for the proof by right-stability:
|
||||||
% https://q.uiver.app/#q=WzAsNixbMSwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgS1oiXSxbMSwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIEtZIl0sWzMsMCwiSygoWCBcXHRpbWVzIFkpIFxcdGltZXMgWikiXSxbMywyLCJLKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgSyhZIFxcdGltZXMgWikiXSxbMCwzLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDEsIlxcYWxwaGEiXSxbMiwzLCJLXFxhbHBoYSJdLFswLDIsIlxcdGF1Il0sWzEsNCwiaWQgXFx0aW1lc1xcdGF1Il0sWzQsMywiXFx0YXUiXSxbNSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzUsMywiXFxldGEgXFxjaXJjIFxcYWxwaGEiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
% https://q.uiver.app/#q=WzAsNixbMSwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgS1oiXSxbMSwyLCJYIFxcdGltZXMgWSBcXHRpbWVzIEtZIl0sWzMsMCwiSygoWCBcXHRpbWVzIFkpIFxcdGltZXMgWikiXSxbMywyLCJLKFggXFx0aW1lcyBZIFxcdGltZXMgWikiXSxbMiwyLCJYIFxcdGltZXMgSyhZIFxcdGltZXMgWikiXSxbMCwzLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDEsIlxcYWxwaGEiXSxbMiwzLCJLXFxhbHBoYSJdLFswLDIsIlxcdGF1Il0sWzEsNCwiaWQgXFx0aW1lc1xcdGF1Il0sWzQsMywiXFx0YXUiXSxbNSwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzUsMywiXFxldGEgXFxjaXJjIFxcYWxwaGEiLDIseyJjdXJ2ZSI6Mn1dXQ==
|
||||||
\[
|
\[
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
|
|
@ -699,17 +706,16 @@ Of course there is also a symmetric version of this.
|
||||||
\arrow["{\eta \circ \alpha}"', curve={height=12pt}, from=4-1, to=3-4]
|
\arrow["{\eta \circ \alpha}"', curve={height=12pt}, from=4-1, to=3-4]
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\]
|
\]
|
||||||
|
|
||||||
where \(\tau \circ (id \times \tau) \circ \alpha \) is right iteration preserving, since for any \(Z : \obj{\C}\) and \(h : Z \rightarrow KX + Z\):
|
where \(\tau \circ (id \times \tau) \circ \alpha \) is right iteration preserving, since for any \(Z : \obj{\C}\) and \(h : Z \rightarrow KX + Z\):
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \tau \circ (id \times \tau) \circ \alpha \circ (id \times h^\sharp)
|
& \tau \circ (id \times \tau) \circ \alpha \circ (id \times h^\sharp)
|
||||||
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle \circ (id \times h^\sharp)
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle \circ (id \times h^\sharp)
|
||||||
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , h^\sharp \circ \pi_2 \rangle \rangle
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ \langle \pi_2 \circ \pi_1 , h^\sharp \circ \pi_2 \rangle \rangle
|
||||||
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ (id \times h^\sharp) \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , \tau \circ (id \times h^\sharp) \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
|
||||||
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , ((\tau + id) \circ dstl \circ (id \times h))^\sharp \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
|
\\=\;&\tau \circ \langle \pi_1 \circ \pi_1 , {((\tau + id) \circ dstl \circ (id \times h))}^\sharp \circ \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle
|
||||||
\\=\;&\tau \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))^\sharp) \circ \alpha
|
\\=\;&\tau \circ (id \times {((\tau + id) \circ dstl \circ (id \times h))}^\sharp) \circ \alpha
|
||||||
\\=\;&((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))^\sharp \circ \alpha
|
\\=\;&{((\tau + id) \circ dstl \circ (id \times ((\tau + id) \circ dstl \circ (id \times h))))}^\sharp \circ \alpha
|
||||||
\\=\;&(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))^\sharp.\tag{\ref{law:uniformity}}
|
\\=\;&{(((\tau \circ (id \times \tau) \circ \alpha) + id) \circ dstl \circ (id \times h))}^\sharp.\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
Thus, strength of \(\mathbf{K}\) has been proven.
|
Thus, strength of \(\mathbf{K}\) has been proven.
|
||||||
|
|
@ -720,8 +726,8 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
||||||
\begin{corollary}
|
\begin{corollary}
|
||||||
\(\sigma \) is left iteration preserving and satisfies \(\sigma \circ (\eta \times id) = \eta \) and the following properties of \(\tau \) and \(\sigma \) hold.
|
\(\sigma \) is left iteration preserving and satisfies \(\sigma \circ (\eta \times id) = \eta \) and the following properties of \(\tau \) and \(\sigma \) hold.
|
||||||
\begin{alignat*}{2}
|
\begin{alignat*}{2}
|
||||||
& \tau \circ (f^* \times g^*) & & = (\tau \circ {(id \times g))}^* \circ \tau \circ (f^* \times id)\tag{\(\tau_1\)}\label{Ktau1}
|
& \tau \circ (f^* \times g^*) & & = {(\tau \circ (id \times g))}^* \circ \tau \circ (f^* \times id)\tag{\(\tau_1\)}\label{Ktau1}
|
||||||
\\&\sigma \circ (f^* \times g^*) &&= (\sigma \circ {(f \times id))}^* \circ \sigma \circ (id \times g^*)\tag{\(\sigma_1\)}\label{Ksigma1}
|
\\&\sigma \circ (f^* \times g^*) &&= {(\sigma \circ (f \times id))}^* \circ \sigma \circ (id \times g^*)\tag{\(\sigma_1\)}\label{Ksigma1}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{corollary}
|
\end{corollary}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
@ -739,16 +745,16 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
||||||
& \sigma \circ (h^\sharp \times id)
|
& \sigma \circ (h^\sharp \times id)
|
||||||
\\=\;&Kswap \circ \tau \circ swap \circ (h^\sharp \times id)
|
\\=\;&Kswap \circ \tau \circ swap \circ (h^\sharp \times id)
|
||||||
\\=\;&Kswap \circ \tau \circ (id \times h^\sharp) \circ swap
|
\\=\;&Kswap \circ \tau \circ (id \times h^\sharp) \circ swap
|
||||||
\\=\;&Kswap \circ ((\tau + id) \circ dstl \circ (id \times h))^\sharp \circ swap
|
\\=\;&Kswap \circ {((\tau + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
|
||||||
\\=\;&(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))^\sharp \circ swap
|
\\=\;&{(((Kswap \circ \tau) + id) \circ dstl \circ (id \times h))}^\sharp \circ swap
|
||||||
\\=\;&((\sigma + id) \circ dstr \circ (h \times id))^\sharp.\tag{\ref{law:uniformity}}
|
\\=\;&{((\sigma + id) \circ dstr \circ (h \times id))}^\sharp.\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Let us now proceed with the properties of \(\tau \) and \(\sigma \).
|
Let us now proceed with the properties of \(\tau \) and \(\sigma \).
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item[(\ref{Ktau1})]
|
\item[(\ref{Ktau1})]
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (\tau \circ {(id \times g))}^* \circ \tau \circ (f^* \times id)
|
& {(\tau \circ (id \times g))}^* \circ \tau \circ (f^* \times id)
|
||||||
\\=\;&\tau^* \circ K(id \times g) \circ \tau \circ (f^* \times id)
|
\\=\;&\tau^* \circ K(id \times g) \circ \tau \circ (f^* \times id)
|
||||||
\\=\;&\tau^* \circ \tau \circ (id \times Kg) \circ (f^* \times id)
|
\\=\;&\tau^* \circ \tau \circ (id \times Kg) \circ (f^* \times id)
|
||||||
\\=\;&\tau \circ (id \times \mu) \circ (id \times Kg) \circ (f^* \times id)
|
\\=\;&\tau \circ (id \times \mu) \circ (id \times Kg) \circ (f^* \times id)
|
||||||
|
|
@ -758,7 +764,7 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
||||||
|
|
||||||
\item[(\ref{Ksigma1})]
|
\item[(\ref{Ksigma1})]
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (\sigma \circ {(f \times id))}^* \circ \sigma \circ (id \times g^*)
|
& {(\sigma \circ (f \times id))}^* \circ \sigma \circ (id \times g^*)
|
||||||
\\=\;&\sigma^* \circ K(f \times id) \circ \sigma \circ (id \times g^*)
|
\\=\;&\sigma^* \circ K(f \times id) \circ \sigma \circ (id \times g^*)
|
||||||
\\=\;&\sigma^* \circ \sigma \circ (Kf \times id) \circ (id \times g^*)
|
\\=\;&\sigma^* \circ \sigma \circ (Kf \times id) \circ (id \times g^*)
|
||||||
\\=\;&\sigma \circ (\mu \times id) \circ (Kf \times id) \circ (id \times g^*)
|
\\=\;&\sigma \circ (\mu \times id) \circ (Kf \times id) \circ (id \times g^*)
|
||||||
|
|
@ -766,77 +772,79 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
||||||
\\=\;&\sigma \circ (f^* \times g^*)
|
\\=\;&\sigma \circ (f^* \times g^*)
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
This concludes the proof.
|
Thus, the proof has been concluded.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
The following Lemma is central to the proof of commutativity.
|
The following Lemma is central to the proof of commutativity.
|
||||||
|
|
||||||
\begin{lemma}\label{lem:KCommKey} Given \(f : X \rightarrow KY + Z, g : Z \rightarrow KA + Z\),
|
\begin{lemma}\label{lem:KCommKey} Given \(f : X \rightarrow KY + X, g : Z \rightarrow KA + Z\),
|
||||||
\[\tau^* \circ \sigma \circ (((\eta + id) \circ f)^\sharp \times ((\eta + id) \circ g)^\sharp) = \sigma^* \circ \tau \circ (((\eta + id) \circ f)^\sharp \times ((\eta + id) \circ g)^\sharp).\]
|
\[\tau^* \circ \sigma \circ ({((\eta + id) \circ f)}^\sharp \times {((\eta + id) \circ g)}^\sharp) = \sigma^* \circ \tau \circ ({((\eta + id) \circ f)}^\sharp \times {((\eta + id) \circ g)}^\sharp).\]
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let us abbreviate \(\hat{f} := (\eta + id) \circ f\) and \(\hat{g} := (\eta + id) \circ g\). It suffices to find a \(w : ?\) such that \(\hat{f}^\sharp \circ \pi_1 = [ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp\) and \(\hat{g}^\sharp \circ \pi_2 = [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^* \circ w^\sharp \), then
|
Let us abbreviate \(\hat{f} := (\eta + id) \circ f\) and \(\hat{g} := (\eta + id) \circ g\). It suffices to find a
|
||||||
|
\[w : X \times Z \rightarrow K(X \times KA + KY \times Z) + X \times Z\]
|
||||||
|
such that \(\hat{f}^\sharp \circ \pi_1 = {[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \circ w^\sharp\) and \(\hat{g}^\sharp \circ \pi_2 = {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^* \circ w^\sharp \), because then
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \tau^* \circ \sigma \circ (\hat{f}^\sharp \times \hat{g}^\sharp)
|
& \tau^* \circ \sigma \circ (\hat{f}^\sharp \times \hat{g}^\sharp)
|
||||||
\\=\;&\tau^* \circ \sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\sharp \times w^\sharp)
|
\\=\;&\tau^* \circ \sigma \circ ({[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ (w^\sharp \times w^\sharp)
|
||||||
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ \sigma \circ (id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ (w^\sharp \times w^\sharp)
|
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ \sigma \circ (id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ (w^\sharp \times w^\sharp)
|
||||||
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ \sigma \circ (w^\sharp \times w^\sharp)
|
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ \sigma \circ (w^\sharp \times w^\sharp)
|
||||||
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ \tau \circ \Delta \circ w^\sharp
|
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ Kswap \circ \tau \circ \Delta \circ w^\sharp
|
||||||
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^*
|
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^*
|
||||||
\\&\hphantom{\tau^* }\circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ Kswap \circ K\langle \eta , id \rangle \circ w^\sharp\tag{\autoref{thm:Klifting}}
|
\\&\hphantom{\tau^* }\circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ Kswap \circ K\langle \eta , id \rangle \circ w^\sharp\tag{\autoref{thm:Klifting}}
|
||||||
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]^*) \circ K\langle id , \eta \rangle \circ w^\sharp
|
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K(id \times {[ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]}^*) \circ K\langle id , \eta \rangle \circ w^\sharp
|
||||||
\\=\;&\tau^* \circ (\sigma \circ {([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K\langle id , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle \circ w^\sharp
|
\\=\;&\tau^* \circ {(\sigma \circ ([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] \times id))}^* \circ K\langle id , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle \circ w^\sharp
|
||||||
\\=\;&\tau^* \circ {(\sigma \circ \langle[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\sharp
|
\\=\;&\tau^* \circ {(\sigma \circ \langle[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ] , [ \hat{g}^\sharp \circ \pi_2 , \eta \circ \pi_2 ]\rangle)}^* \circ w^\sharp
|
||||||
\\=\;&\tau^* \circ {(\sigma \circ [\langle \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_2 \rangle , \langle \eta \circ \pi_1 , \hat{g}^\sharp \circ \pi_2 \rangle])}^* \circ w^\sharp
|
\\=\;&\tau^* \circ {(\sigma \circ [\langle \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_2 \rangle , \langle \eta \circ \pi_1 , \hat{g}^\sharp \circ \pi_2 \rangle])}^* \circ w^\sharp
|
||||||
\\=\;&{(\tau^* \circ \sigma \circ [\hat{f}^\sharp \times \eta , \eta \times \hat{g}^\sharp])}^* \circ w^\sharp
|
\\=\;&{(\tau^* \circ \sigma \circ [\hat{f}^\sharp \times \eta , \eta \times \hat{g}^\sharp])}^* \circ w^\sharp
|
||||||
\\=\;&([\tau^* \circ \sigma \circ (\hat{f}^\sharp \times \eta) , \tau^* \circ \sigma \circ {(\eta \times \hat{g}^\sharp)])}^* \circ w^\sharp
|
\\=\;&{([\tau^* \circ \sigma \circ (\hat{f}^\sharp \times \eta) , \tau^* \circ \sigma \circ (\eta \times \hat{g}^\sharp)])}^* \circ w^\sharp
|
||||||
\\=\;&([\tau^* \circ K(id \times \eta) \circ \sigma \circ (\hat{f}^\sharp \times id) , \tau^* \circ \eta \circ {(id \times \hat{g}^\sharp)])}^* \circ w^\sharp
|
\\=\;&{([\tau^* \circ K(id \times \eta) \circ \sigma \circ (\hat{f}^\sharp \times id) , \tau^* \circ \eta \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp
|
||||||
\\=\;&([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ {(id \times \hat{g}^\sharp)])}^* \circ w^\sharp,
|
\\=\;&{([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp,
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
and by a symmetric argument also
|
and by a symmetric argument also
|
||||||
\[\sigma^* \circ \tau \circ (\hat{f}^\sharp \times \hat{g}^\sharp) = ([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ {(id \times \hat{g}^\sharp)])}^* \circ w^\sharp.\]
|
\[\sigma^* \circ \tau \circ (\hat{f}^\sharp \times \hat{g}^\sharp) = {([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp.\]
|
||||||
|
|
||||||
Note that we are referencing \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity.
|
Note that we are referencing the equational lifting law established in \autoref{thm:Klifting} even though for a monad to be an equational lifting monad it has to be commutative first. However, since we are merely referencing the equational law, which can (and does in this case) hold without depending on commutativity, this does not pose a problem.
|
||||||
|
|
||||||
We are thus left to find such a \(w\), consider
|
We are thus left to find such a \(w\), consider
|
||||||
\[w := [ i_1 \circ K i_1 \circ \tau , ((K i_2 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}). \]
|
\[w := [ i_1 \circ K i_1 \circ \tau , ((K i_2 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}). \]
|
||||||
\(w\) indeed satisfies the requisite properties, let us check the first property, the second one follows by a symmetric argument. We will show that
|
\(w\) indeed satisfies the requisite properties, let us check the first property, the second one follows by a symmetric argument. We need to show that
|
||||||
\[[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp = ([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\sharp = \hat{f}^\sharp \circ \pi_1. \]
|
\[{[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \circ w^\sharp = {([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp = \hat{f}^\sharp \circ \pi_1. \]
|
||||||
Indeed,
|
Indeed,
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& [ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* \circ w^\sharp
|
& {[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* \circ w^\sharp
|
||||||
\\=\;&(([ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]^* + id) \circ w)^\sharp
|
\\=\;&{(({[ \hat{f}^\sharp \circ \pi_1 , \eta \circ \pi_1 ]}^* + id) \circ w)}^\sharp
|
||||||
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}))^\sharp
|
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times \hat{g}))}^\sharp
|
||||||
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times (\eta + id)) \circ (id \times g))^\sharp
|
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times (\eta + id)) \circ (id \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ ((id \times \eta) + id) \circ dstl \circ (id \times g))^\sharp
|
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ ((id \times \eta) + id) \circ dstl \circ (id \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau \circ (id \times \eta) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp
|
\\=\;&{([ i_1 \circ {(\hat{f}^\sharp \circ \pi_1)}^* \circ \tau \circ (id \times \eta) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ \hat{f}^\sharp \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp
|
\\=\;&{([ i_1 \circ \hat{f}^\sharp \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \hat{f} \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp\tag{\ref{law:fixpoint}}
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \hat{f} \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp\tag{\ref{law:fixpoint}}
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 \circ (\hat{f} \times id) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))^\sharp
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 \circ (\hat{f} \times id) , ((K\pi_1 \circ \sigma) + id) \circ dstr \circ (\hat{f} \times id) ] \circ dstl \circ (id \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ ((\hat{f} \times id) + (\hat{f} \times id)) \circ dstl \circ (id \times g))^\sharp
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ ((\hat{f} \times id) + (\hat{f} \times id)) \circ dstl \circ (id \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ \pi_1 , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) \circ dstr , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) \circ dstr , ((K\pi_1 \circ \sigma) + id) \circ dstr ] \circ dstl \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ (dstr + dstr) \circ dstl \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ (dstr + dstr) \circ dstl \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ [ i_1 + i_1 , i_2 + i_2 ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ i_1 \circ [id , \hat{f}^\sharp] \circ (\pi_1 + \pi_1) , ((K\pi_1 \circ \sigma) + id) ] \circ [ i_1 + i_1 , i_2 + i_2 ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ [ i_1 \circ [id , \hat{f}^\sharp] \circ i_1 \circ \pi_1 , i_1 \circ K\pi_1 \circ \sigma ] , [ i_1 \circ [id , \hat{f}^\sharp] \circ i_2 \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ [ i_1 \circ [id , \hat{f}^\sharp] \circ i_1 \circ \pi_1 , i_1 \circ K\pi_1 \circ \sigma ] , [ i_1 \circ [id , \hat{f}^\sharp] \circ i_2 \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ [ i_1 \circ \pi_1 , i_1 \circ \pi_1 ] , [ i_1 \circ \hat{f}^\sharp \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ [ i_1 \circ \pi_1 , i_1 \circ \pi_1 ] , [ i_1 \circ \hat{f}^\sharp \circ \pi_1 , i_2 ] ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ [ \pi_1 , \pi_1 ] , (\hat{f}^\sharp \circ \pi_1 + id) ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ i_1 \circ [ \pi_1 , \pi_1 ] , (\hat{f}^\sharp \circ \pi_1 + id) ] \circ (dstl + dstl) \circ dstr \circ (\hat{f} \times g))}^\sharp
|
||||||
\\=\;&([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\sharp
|
\\=\;&{([ i_1 \circ \pi_1 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
and
|
and
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \hat{f}^\sharp \circ \pi_1
|
& \hat{f}^\sharp \circ \pi_1
|
||||||
\\=\;&((id + \Delta) \circ h)^\sharp \tag{\ref{law:uniformity}}
|
\\=\;&{((id + \Delta) \circ h)}^\sharp \tag{\ref{law:uniformity}}
|
||||||
\\=\;&([ i_1 , ((id + \Delta) \circ h)^\sharp + id] \circ h)^\sharp \tag{\ref{law:diamond}}
|
\\=\;&{([ i_1 , {((id + \Delta) \circ h)}^\sharp + id] \circ h)}^\sharp \tag{\ref{law:diamond}}
|
||||||
\\=\;&([ i_1 , (\hat{f}^\sharp \circ \pi_1) + id ] \circ h)^\sharp \tag{\ref{law:uniformity}}
|
\\=\;&{([ i_1 , (\hat{f}^\sharp \circ \pi_1) + id ] \circ h)}^\sharp \tag{\ref{law:uniformity}}
|
||||||
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1 \circ \pi_1) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1 \circ \pi_1) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))}^\sharp
|
||||||
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ ((\pi_1 \times id) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ ((\pi_1 \times id) + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))}^\sharp
|
||||||
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ \langle \pi_1 , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ \langle \pi_1 , g \circ \pi_2 \rangle ] \circ dstr \circ (\hat{f} \times id))}^\sharp
|
||||||
\\=\;&([ i_1 \circ \pi_1 \circ (id \times g) , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ (id \times g) ] \circ dstr \circ (\hat{f} \times id))^\sharp
|
\\=\;&{([ i_1 \circ \pi_1 \circ (id \times g) , ((\hat{f} \circ \pi_1) + id) \circ dstl \circ (id \times g) ] \circ dstr \circ (\hat{f} \times id))}^\sharp
|
||||||
\\=\;&([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\sharp,
|
\\=\;&{([ i_1 \circ \pi_1 , ((\hat{f} \circ \pi_1) + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp,
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
where \(h = (\pi_1 + ((\pi_1 + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)\) and the application of \ref{law:uniformity} is justified, since
|
where \(h = (\pi_1 + (\pi_1 + (\pi_1 \times id)) \circ dstl \circ \langle id , g \circ \pi_2 \rangle) \circ dstr \circ (\hat{f} \times id)\) and the application of \ref{law:uniformity} is justified, since % chktex 2
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& (id + \pi_1) \circ (id + \Delta) \circ h
|
& (id + \pi_1) \circ (id + \Delta) \circ h
|
||||||
\\=\;&(\pi_1 + ((\pi_1 \circ [ \pi_1 , \pi_1 \times id ]) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
|
\\=\;&(\pi_1 + ((\pi_1 \circ [ \pi_1 , \pi_1 \times id ]) \circ dstl \circ \langle id , g \circ \pi_2 \rangle)) \circ dstr \circ (\hat{f} \times id)
|
||||||
|
|
@ -850,9 +858,9 @@ The following Lemma is central to the proof of commutativity.
|
||||||
This concludes the proof.
|
This concludes the proof.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{theorem}
|
\begin{lemma}
|
||||||
\(\mathbf{K}\) is a commutative monad.
|
\(\mathbf{K}\) is a commutative monad.
|
||||||
\end{theorem}
|
\end{lemma}
|
||||||
\begin{proof} We need to show that \(\tau^* \circ \sigma = \sigma^* \circ \tau : KX \times KY \rightarrow K(X \times Y)\).
|
\begin{proof} We need to show that \(\tau^* \circ \sigma = \sigma^* \circ \tau : KX \times KY \rightarrow K(X \times Y)\).
|
||||||
Let us proceed by right stability, consider the following diagram.
|
Let us proceed by right stability, consider the following diagram.
|
||||||
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0=
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJLWCBcXHRpbWVzIEtZIl0sWzMsMCwiSyhLWCBcXHRpbWVzIFkpIl0sWzEsMiwiSyhYIFxcdGltZXMgS1kpIl0sWzMsMiwiSyhYIFxcdGltZXMgWSkiXSxbMCwzLCJLWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdSJdLFswLDIsIlxcaGF0e1xcdGF1fSIsMl0sWzEsMywiXFxoYXR7XFx0YXV9XioiXSxbMiwzLCJcXHRhdV4qIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMywiXFxoYXR7XFx0YXV9IiwyLHsiY3VydmUiOjJ9XV0=
|
||||||
|
|
@ -874,10 +882,10 @@ The following Lemma is central to the proof of commutativity.
|
||||||
The diagram commutes since
|
The diagram commutes since
|
||||||
\[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma \]
|
\[\sigma^* \circ \tau \circ (id \times \eta) = \sigma^* \circ \eta = \sigma \]
|
||||||
and
|
and
|
||||||
\[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = (\tau \circ {(id \times \eta))}^* \circ \sigma = \sigma.\]
|
\[\tau^* \circ \sigma \circ (id \times \eta) = \tau^* \circ K(id \times \eta) \circ \sigma = {(\tau \circ (id \times \eta))}^* \circ \sigma = \sigma.\]
|
||||||
|
|
||||||
We are left to show that both \(\sigma^* \circ \tau \) and \(\tau^* \circ \sigma \) are right iteration preserving. Let \(h : Z \rightarrow KY + Z\), indeed
|
We are left to show that both \(\sigma^* \circ \tau \) and \(\tau^* \circ \sigma \) are right iteration preserving. Let \(h : Z \rightarrow KY + Z\), indeed
|
||||||
\[\sigma^* \circ \tau \circ (id \times h^\sharp) = \sigma^* ((\tau + id) \circ dstl \circ (id \times h))^\sharp = (((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))^\sharp. \]
|
\[\sigma^* \circ \tau \circ (id \times h^\sharp) = \sigma^* {((\tau + id) \circ dstl \circ (id \times h))}^\sharp = {(((\sigma^* \circ \tau) + id) \circ dstl \circ (id \times h))}^\sharp. \]
|
||||||
|
|
||||||
Let \(\psi := \tau^* \circ \sigma \) and let us proceed by left stability to show that \(\psi \) is right iteration preserving, consider the following diagram
|
Let \(\psi := \tau^* \circ \sigma \) and let us proceed by left stability to show that \(\psi \) is right iteration preserving, consider the following diagram
|
||||||
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
|
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJLWCBcXHRpbWVzIEtZIl0sWzQsMSwiSyhYIFxcdGltZXMgWSkiXSxbMCwxLCJLWCBcXHRpbWVzIFoiXSxbMCwzLCJYIFxcdGltZXMgWiJdLFswLDEsIlxccHNpIl0sWzIsMCwiaWQgXFx0aW1lcyBoXlxcIyJdLFsyLDEsIigoXFxwc2kgKyBpZCkgXFxjaXJjIGRzdGwgXFxjaXJjIChpZCBcXHRpbWVzIGgpKV5cXCMiLDJdLFszLDIsIlxcZXRhIFxcdGltZXMgaWQiXSxbMywxLCJcXHRhdSBcXGNpcmMgKGlkIFxcdGltZXMgaF5cXCMpIiwyXV0=
|
||||||
|
|
@ -900,54 +908,54 @@ The following Lemma is central to the proof of commutativity.
|
||||||
\\=\;&\psi \circ (\eta \times id) \circ (id \times h^\sharp)
|
\\=\;&\psi \circ (\eta \times id) \circ (id \times h^\sharp)
|
||||||
\\=\;&\tau^* \circ \eta \circ (id \times h^\sharp)
|
\\=\;&\tau^* \circ \eta \circ (id \times h^\sharp)
|
||||||
\\=\;&\tau \circ (id \times h^\sharp)
|
\\=\;&\tau \circ (id \times h^\sharp)
|
||||||
\\=\;&((\tau + id) \circ dstl \circ (id \times h))^\sharp
|
\\=\;&{((\tau + id) \circ dstl \circ (id \times h))}^\sharp
|
||||||
\\=\;&((\psi + id) \circ dstl \circ (id \times h))^\sharp \circ (\eta \times id).\tag{\ref{law:uniformity}}
|
\\=\;&{((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (\eta \times id).\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
We are left to show that both \(\psi \circ (id \times h^\sharp)\) and \(((\psi + id) \circ dstl \circ (id \times h))^\sharp \) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi \circ (id \times h^\sharp)\) is left iteration preserving, since
|
We are left to show that both \(\psi \circ (id \times h^\sharp)\) and \({((\psi + id) \circ dstl \circ (id \times h))}^\sharp \) are left iteration preserving. Let \(g : A \rightarrow KX + A\), then \(\psi \circ (id \times h^\sharp)\) is left iteration preserving, since
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \psi \circ (id \times h^\sharp) \circ (g^\sharp \times id)
|
& \psi \circ (id \times h^\sharp) \circ (g^\sharp \times id)
|
||||||
\\=\;&\psi \circ (g^\sharp \times id) \circ (id \times h^\sharp)
|
\\=\;&\psi \circ (g^\sharp \times id) \circ (id \times h^\sharp)
|
||||||
\\=\;&\tau^* \circ ((\sigma + id) \circ dstr \circ (g \times id))^\sharp \circ (id \times h^\sharp)
|
\\=\;&\tau^* \circ {((\sigma + id) \circ dstr \circ (g \times id))}^\sharp \circ (id \times h^\sharp)
|
||||||
\\=\;&((\psi + id) \circ dstr \circ (g \times id))^\sharp \circ (id \times h^\sharp)
|
\\=\;&{((\psi + id) \circ dstr \circ (g \times id))}^\sharp \circ (id \times h^\sharp)
|
||||||
\\=\;&(((\psi \circ (id \times h^\sharp)) + id) \circ dstr \circ (g \times id))^\sharp.\tag{\ref{law:uniformity}}
|
\\=\;&{(((\psi \circ (id \times h^\sharp)) + id) \circ dstr \circ (g \times id))}^\sharp.\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Lastly, we need to show that
|
Lastly, we need to show that
|
||||||
\[((\psi + id) \circ dstl \circ (id \times h))^\sharp \circ (g^\sharp \times id) = ((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp.\]
|
\[{((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (g^\sharp \times id) = {(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp.\]
|
||||||
Note that by~\ref{law:uniformity} the left-hand side can be rewritten as
|
Note that by~\ref{law:uniformity} the left-hand side can be rewritten as
|
||||||
\[((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp.\]
|
\[{(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp.\]
|
||||||
|
|
||||||
Consider now, that
|
Consider now, that
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& ((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp
|
& {(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp
|
||||||
\\=\;&(((((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))^\sharp
|
\\=\;&{(({({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* + id) \circ (\eta + id) \circ dstr \circ (g \times id))}^\sharp
|
||||||
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ ((\eta + id) \circ dstr \circ (g \times id))^\sharp
|
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ {((\eta + id) \circ dstr \circ (g \times id))}^\sharp
|
||||||
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ (((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))^\sharp
|
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ {(((\sigma \circ (\eta \times id)) + id) \circ dstr \circ (g \times id))}^\sharp
|
||||||
\\=\;&(((\psi + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&{({((\psi + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&(((\psi^* + id) \circ (\eta + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&{({((\psi^* + id) \circ (\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ {({((\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ (((\eta + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ {({((\eta + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ ((((\tau \circ (id \times \eta)) + id) \circ dstl \circ {(id \times h))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ {({(((\tau \circ (id \times \eta)) + id) \circ dstl \circ (id \times h))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ (((\tau + id) \circ dstl \circ (id \times ({(\eta + id) \circ h)))^\sharp)}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ {({((\tau + id) \circ dstl \circ (id \times ((\eta + id) \circ h)))}^\sharp)}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ (\tau \circ (id \times ({(\eta + id) \circ h)^\sharp))}^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ {(\tau \circ (id \times {((\eta + id) \circ h)}^\sharp))}^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ \tau^* \circ K(id \times ((\eta + id) \circ h)^\sharp) \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ \tau^* \circ K(id \times {((\eta + id) \circ h)}^\sharp) \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times ((\eta + id) \circ h)^\sharp) \circ (((\eta + id) \circ g)^\sharp \times id)
|
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (id \times {((\eta + id) \circ h)}^\sharp) \circ ({((\eta + id) \circ g)}^\sharp \times id)
|
||||||
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp),
|
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp),
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
and by a symmetric argument
|
and by a symmetric argument
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& ((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp
|
& {(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp
|
||||||
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp).
|
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp).
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
We are thus done by
|
We are thus done by
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& ((\psi + id) \circ dstl \circ (id \times h))^\sharp \circ (g^\sharp \times id)
|
& {((\psi + id) \circ dstl \circ (id \times h))}^\sharp \circ (g^\sharp \times id)
|
||||||
\\=\;&((((\psi + id) \circ dstr \circ (g \times id))^\sharp + id) \circ dstl \circ (id \times h))^\sharp\tag{\ref{law:uniformity}}
|
\\=\;&{(({((\psi + id) \circ dstr \circ (g \times id))}^\sharp + id) \circ dstl \circ (id \times h))}^\sharp\tag{\ref{law:uniformity}}
|
||||||
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp)
|
\\=\;&\psi^* \circ \sigma^* \circ \tau \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp)
|
||||||
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ (((\eta + id) \circ g)^\sharp \times ((\eta + id) \circ h)^\sharp)\tag{\autoref{lem:KCommKey}}
|
\\=\;&\psi^* \circ \tau^* \circ \sigma \circ ({((\eta + id) \circ g)}^\sharp \times {((\eta + id) \circ h)}^\sharp)\tag{\autoref{lem:KCommKey}}
|
||||||
\\=\;&((((\psi + id) \circ dstl \circ (id \times h))^\sharp + id) \circ dstr \circ (g \times id))^\sharp.\tag*{\qedhere}
|
\\=\;&{(({((\psi + id) \circ dstl \circ (id \times h))}^\sharp + id) \circ dstr \circ (g \times id))}^\sharp.\tag*{\qedhere}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
@ -958,7 +966,7 @@ The following Lemma is central to the proof of commutativity.
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Since we have already shown commutativity, we are left to show that \(\tau \circ \Delta = K \langle \eta , id \rangle \). Note that \(K \langle \eta , id \rangle = \free{\eta \circ \langle \eta , id \rangle}\), which is the unique Elgot algebra morphism satisfying \(K \langle \eta , id \rangle \circ \eta = \eta \circ \langle \eta , id \rangle \). It thus suffices to show that \(\tau \circ \Delta \) satisfies the same identity and is iteration preserving.
|
Since we have already shown commutativity, we are left to show that \(\tau \circ \Delta = K \langle \eta , id \rangle \). Note that \(K \langle \eta , id \rangle = \free{\eta \circ \langle \eta , id \rangle}\), which is the unique Elgot algebra morphism satisfying \(K \langle \eta , id \rangle \circ \eta = \eta \circ \langle \eta , id \rangle \). It thus suffices to show that \(\tau \circ \Delta \) satisfies the same identity and is iteration preserving.
|
||||||
|
|
||||||
The identity follows easily
|
The identity follows easily:
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& \tau \circ \Delta \circ \eta
|
& \tau \circ \Delta \circ \eta
|
||||||
\\=\;&\tau \circ \langle \eta , \eta \rangle
|
\\=\;&\tau \circ \langle \eta , \eta \rangle
|
||||||
|
|
@ -971,8 +979,8 @@ The following Lemma is central to the proof of commutativity.
|
||||||
& \tau \circ \Delta \circ h^{\sharp}
|
& \tau \circ \Delta \circ h^{\sharp}
|
||||||
\\=\;&\tau \circ \langle h^{\sharp} , h^{\sharp} \rangle
|
\\=\;&\tau \circ \langle h^{\sharp} , h^{\sharp} \rangle
|
||||||
\\=\;&\tau \circ (id \times h^{\sharp}) \circ \langle h^{\sharp} , id \rangle
|
\\=\;&\tau \circ (id \times h^{\sharp}) \circ \langle h^{\sharp} , id \rangle
|
||||||
\\=\;&((\tau + id) \circ dstl \circ (id \times f))^\sharp \circ \langle h^{\sharp} , id \rangle
|
\\=\;&{((\tau + id) \circ dstl \circ (id \times f))}^\sharp \circ \langle h^{\sharp} , id \rangle
|
||||||
\\=\;&(((\tau \circ \Delta) + id) \circ f)^\sharp.\tag{\ref{law:uniformity}}
|
\\=\;&{(((\tau \circ \Delta) + id) \circ f)}^\sharp.\tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
|
Note that by monicity of \(dstl^{-1}\) and by~\ref{law:fixpoint}
|
||||||
|
|
@ -994,11 +1002,11 @@ The following Lemma is central to the proof of commutativity.
|
||||||
Note that \(\mathbf{K}\) is a pre-Elgot monad by definition and strong pre-Elgot by \autoref{lem:Kstrong}. Let us first show that \(\mathbf{K}\) is the initial pre-Elgot monad.
|
Note that \(\mathbf{K}\) is a pre-Elgot monad by definition and strong pre-Elgot by \autoref{lem:Kstrong}. Let us first show that \(\mathbf{K}\) is the initial pre-Elgot monad.
|
||||||
|
|
||||||
Given any pre-Elgot monad \(\mathbf{T}\), let us introduce alternative names for the monad operations of \(\mathbf{T}\) and \(\mathbf{K}\) to avoid confusion:
|
Given any pre-Elgot monad \(\mathbf{T}\), let us introduce alternative names for the monad operations of \(\mathbf{T}\) and \(\mathbf{K}\) to avoid confusion:
|
||||||
\[\mathbf{T} = (T , \eta^T, \mu^T, {(-)}^{\sharp_T})\]
|
\[\mathbf{T} = (T , \eta^T, \mu^T)\]
|
||||||
and
|
and
|
||||||
\[\mathbf{K} = (K , \eta^K, \mu^T, {(-)}^{\sharp_K}).\]
|
\[\mathbf{K} = (K , \eta^K, \mu^T).\]
|
||||||
|
|
||||||
For every \(X \in \obj{\C} \) we define \(¡ = \free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is the unique iteration preserving morphism that satisfies \(¡ \circ \eta^K = \eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
|
For every \(X \in \obj{\C} \) we define \(¡ = \free{(\eta^T : X \rightarrow TX)} : KX \rightarrow TX \). Note that \(¡\) is per definition the unique iteration preserving morphism that satisfies \(¡ \circ \eta^K = \eta^T\). We are done after showing that \(¡\) is natural and respects the monad multiplication.
|
||||||
|
|
||||||
Let \(f : X \rightarrow Y\). For naturality of \(¡\) it suffices to show
|
Let \(f : X \rightarrow Y\). For naturality of \(¡\) it suffices to show
|
||||||
\[¡ \circ Kf = \free{Tf \circ \eta^T} = Tf \circ ¡,\]
|
\[¡ \circ Kf = \free{Tf \circ \eta^T} = Tf \circ ¡,\]
|
||||||
|
|
@ -1008,7 +1016,7 @@ The following Lemma is central to the proof of commutativity.
|
||||||
& ¡ \circ Kf \circ \eta^K
|
& ¡ \circ Kf \circ \eta^K
|
||||||
\\=\;&¡ \circ \eta^K \circ f
|
\\=\;&¡ \circ \eta^K \circ f
|
||||||
\\=\;&\eta^T \circ f
|
\\=\;&\eta^T \circ f
|
||||||
\\=\;&Tf \circ \eta^T
|
\\=\;&Tf \circ \eta^T.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Let us proceed similarly for showing that \(¡\) respects the monad multiplication, i.e.\ consider
|
Let us proceed similarly for showing that \(¡\) respects the monad multiplication, i.e.\ consider
|
||||||
|
|
@ -1022,7 +1030,7 @@ The following Lemma is central to the proof of commutativity.
|
||||||
\\=\;&¡.
|
\\=\;&¡.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Thus, \(\mathbf{K}\) is an initial pre-Elgot monad. To show that \(\mathbf{K}\) is also initial strong pre-Elgot, assume that \(\mathbf{T}\) is strong with strength \(\tau^T\) and let us call the strength of \(\mathbf{K}\) \(\tau^K\). We are left to show that \(¡\) respects strength, i.e.\ \( ¡ \circ \tau^K = \tau^T \circ (id \times ¡) : X \times KY \rightarrow T(X \times Y) \). Note that
|
Thus, \(\mathbf{K}\) is an initial pre-Elgot monad. To show that \(\mathbf{K}\) is also initial strong pre-Elgot, assume that \(\mathbf{T}\) is strong with strength \(\tau^T\) and let us call the strength of \(\mathbf{K}\) \(\tau^K\). We are left to show that \(¡\) respects strength, i.e.\ \( ¡ \circ \tau^K = \tau^T \circ (id \times ¡) : X \times KY \rightarrow T(X \times Y) \). We proceed by right-stability, using:
|
||||||
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS1kiXSxbMywwLCJLKFggXFx0aW1lcyBZKSJdLFszLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzEsMiwiWCBcXHRpbWVzIFRZIl0sWzAsMywiWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdV5LIl0sWzEsMiwiwqEiXSxbMCwzLCJpZCBcXHRpbWVzIMKhIiwyXSxbMywyLCJcXHRhdV5UIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMiwiXFxldGFeVCIsMix7ImN1cnZlIjoyfV1d
|
% https://q.uiver.app/#q=WzAsNSxbMSwwLCJYIFxcdGltZXMgS1kiXSxbMywwLCJLKFggXFx0aW1lcyBZKSJdLFszLDIsIlQoWCBcXHRpbWVzIFkpIl0sWzEsMiwiWCBcXHRpbWVzIFRZIl0sWzAsMywiWCBcXHRpbWVzIFkiXSxbMCwxLCJcXHRhdV5LIl0sWzEsMiwiwqEiXSxbMCwzLCJpZCBcXHRpbWVzIMKhIiwyXSxbMywyLCJcXHRhdV5UIiwyXSxbNCwwLCJpZCBcXHRpbWVzIFxcZXRhIiwwLHsiY3VydmUiOi0yfV0sWzQsMiwiXFxldGFeVCIsMix7ImN1cnZlIjoyfV1d
|
||||||
\[
|
\[
|
||||||
\begin{tikzcd}[ampersand replacement=\&]
|
\begin{tikzcd}[ampersand replacement=\&]
|
||||||
|
|
@ -1038,5 +1046,5 @@ The following Lemma is central to the proof of commutativity.
|
||||||
\arrow["{\eta^T}"', curve={height=12pt}, from=4-1, to=3-4]
|
\arrow["{\eta^T}"', curve={height=12pt}, from=4-1, to=3-4]
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\]
|
\]
|
||||||
commutes, since \( ¡ \circ \tau^K = \eta^T = \tau^T \circ (id \times \eta^T) = \tau^T \circ (id \times ¡) \circ (id \times \eta^T) \). Using \autoref{rem:proofbystability} we are done, since \(¡ \circ \tau^K\) and \(\tau^T \circ (id \times ¡)\) are both right iteration preserving for the reason that both are composed of (right) iteration preserving morphisms.
|
The diagram commutes, since \( ¡ \circ \tau^K = \eta^T = \tau^T \circ (id \times \eta^T) = \tau^T \circ (id \times ¡) \circ (id \times \eta^T) \). Now we are done, since \(¡ \circ \tau^K\) and \(\tau^T \circ (id \times ¡)\) are both right iteration preserving because both are composed of (right) iteration preserving morphisms.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
@ -12,11 +12,11 @@ We will now introduce the category that the rest of the chapter will take place
|
||||||
For brevity, we will not use the tuple notation most of the time, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
|
For brevity, we will not use the tuple notation most of the time, instead we will just say `Let \(A\) be a setoid' and implicitly call the equivalence relation \(\overset{A}{=}\).
|
||||||
|
|
||||||
\begin{definition}[Setoid Function]
|
\begin{definition}[Setoid Function]
|
||||||
A function on setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid functions as \(A \leadsto B\).
|
A function on setoids \(A\) and \(B\) is a function \(f : A \rightarrow B\) between the carriers, such that \(f\) respects the equivalences, i.e.\ for any \(x,y : A\), \(x \overset{A}{=} y\) implies \(f\;x \overset{B}{=} f\;y\). We will denote setoid functions as \(A ⇝ B\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
Let us now consider the function space setoid, which is of special interest, since it defines a notion of equality between functions.
|
Let us now consider the function space setoid, which is of special interest, since it defines a notion of equality between functions.
|
||||||
\begin{definition}[Function Space Setoid]
|
\begin{definition}[Function Space Setoid]
|
||||||
Given two setoids \(A\) and \(B\). The function space setoid on these setoids is defined as \((A \leadsto B, \doteq)\) or just \(A \leadsto B\), where \(\doteq\) is point wise equality on setoid functions.
|
Given two setoids \(A\) and \(B\). The function space setoid on these setoids is defined as \((A ⇝ B, \doteq)\) or just \(A ⇝ B\), where \(\doteq\) is point wise equality on setoid functions.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
Setoids together with setoid functions form a category that we will call \(\setoids\). Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
|
Setoids together with setoid functions form a category that we will call \(\setoids\). Properties of \(\setoids\) have already been examined in~\cite{setoids}, however we will reiterate some of these properties now to introduce notation that will be used for the rest of the chapter.
|
||||||
|
|
@ -31,45 +31,45 @@ Setoids together with setoid functions form a category that we will call \(\seto
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item \textbf{Products}:
|
\item \textbf{Products}:
|
||||||
\begin{minted}{agda}
|
\begin{minted}{agda}
|
||||||
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||||
constructor _,_
|
constructor _,_
|
||||||
field
|
field
|
||||||
fst : A
|
fst : A
|
||||||
snd : B
|
snd : B
|
||||||
|
|
||||||
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||||
→ (A → B) → (A → C) → A → (B × C)
|
→ (A → B) → (A → C) → A → (B × C)
|
||||||
< f , g > x = (f x , g x)
|
< f , g > x = (f x , g x)
|
||||||
\end{minted}
|
\end{minted}
|
||||||
The product setoid is denoted \((A \times B, \overset{\times}{=})\) or just \(A \times B\). Equality of products is defined in the canonical way.
|
The product setoid is denoted \((A \times B, \overset{\times}{=})\) or just \(A \times B\). Equality of products is defined in the canonical way.
|
||||||
\item \textbf{Terminal Object}:
|
\item \textbf{Terminal Object}:
|
||||||
\begin{minted}{agda}
|
\begin{minted}{agda}
|
||||||
record ⊤ {l} : Set l where
|
record ⊤ {l} : Set l where
|
||||||
constructor tt
|
constructor tt
|
||||||
|
|
||||||
! : ∀ {l} {X : Set l} → X → ⊤ {l}
|
! : ∀ {l} {X : Set l} → X → ⊤ {l}
|
||||||
! _ = tt
|
! _ = tt
|
||||||
\end{minted}
|
\end{minted}
|
||||||
The terminal setoid is thus \((\top, \overset{\top}{=})\), where \(\top \overset{\top}{=} \top\).
|
The terminal setoid is thus \((\top, \overset{\top}{=})\), where \(\top \overset{\top}{=} \top\).
|
||||||
\item \textbf{Coproducts}:
|
\item \textbf{Coproducts}:
|
||||||
\begin{minted}{agda}
|
\begin{minted}{agda}
|
||||||
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||||
i₁ : A → A + B
|
i₁ : A → A + B
|
||||||
i₂ : B → A + B
|
i₂ : B → A + B
|
||||||
|
|
||||||
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||||
→ (A → C) → (B → C) → (A + B) → C
|
→ (A → C) → (B → C) → (A + B) → C
|
||||||
[ f , g ] (i₁ x) = f x
|
[ f , g ] (i₁ x) = f x
|
||||||
[ f , g ] (i₂ x) = g x
|
[ f , g ] (i₂ x) = g x
|
||||||
\end{minted}
|
\end{minted}
|
||||||
Similarly to products, the coproduct setoid is denoted \((A + B, \overset{+}{=})\) or just \(A + B\), where equality of coproducts is defined in the canonical way.
|
Similarly to products, the coproduct setoid is denoted \((A + B, \overset{+}{=})\) or just \(A + B\), where equality of coproducts is defined in the canonical way.
|
||||||
\item \textbf{Initial Object}:
|
\item \textbf{Initial Object}:
|
||||||
\begin{minted}{agda}
|
\begin{minted}{agda}
|
||||||
data ⊥ {l} : Set l where
|
data ⊥ {l} : Set l where
|
||||||
|
|
||||||
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
|
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
|
||||||
¡ ()
|
¡ ()
|
||||||
\end{minted}
|
\end{minted}
|
||||||
The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
|
The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
|
|
||||||
|
|
@ -94,7 +94,7 @@ Setoids together with setoid functions form a category that we will call \(\seto
|
||||||
\(\setoids\) is Cartesian closed.
|
\(\setoids\) is Cartesian closed.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(A\) and \(B\) be two setoids. The function space setoid \(A \leadsto B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
|
Let \(A\) and \(B\) be two setoids. The function space setoid \(A ⇝ B\) is an exponential object of \(A\) and \(B\), together with the functions \(curry\) and \(eval\) defined in the following listing.
|
||||||
\begin{minted}{agda}
|
\begin{minted}{agda}
|
||||||
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||||
→ (C × A → B) → C → A → B
|
→ (C × A → B) → C → A → B
|
||||||
|
|
@ -168,7 +168,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We need to show that for every setoid \(A\) the resulting setoid \(\dbtilde{D}\;A\) can be extended to an Elgot algebra.
|
We need to show that for every setoid \(A\) the resulting setoid \(\dbtilde{D}\;A\) can be extended to an Elgot algebra.
|
||||||
|
|
||||||
Let \(X\) be a setoid and \(f : X \leadsto \dbtilde{D}\;A + X\) be a setoid function, we define \(f^\sharp : X \leadsto \dbtilde{D}\;A\) point wise:
|
Let \(X\) be a setoid and \(f : X ⇝ \dbtilde{D}\;A + X\) be a setoid function, we define \(f^\sharp : X ⇝ \dbtilde{D}\;A\) point wise:
|
||||||
\[
|
\[
|
||||||
f^\sharp\;x :=
|
f^\sharp\;x :=
|
||||||
\begin{cases}
|
\begin{cases}
|
||||||
|
|
@ -189,7 +189,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
|
||||||
\case{} \(f\;x = i_2\;a\)
|
\case{} \(f\;x = i_2\;a\)
|
||||||
\[ f^\sharp\;x \approx later (f^{\sharp}\;a) \approx f^\sharp\;a \approx [ id , f^\sharp ] (i_2 \;a) \approx [ id , f^\sharp ] (f\;x)\]
|
\[ f^\sharp\;x \approx later (f^{\sharp}\;a) \approx f^\sharp\;a \approx [ id , f^\sharp ] (i_2 \;a) \approx [ id , f^\sharp ] (f\;x)\]
|
||||||
\end{mycase}
|
\end{mycase}
|
||||||
\item \ref{law:uniformity}: Let \(Y\) be a setoid and \(g : Y \leadsto \dbtilde{D}\;A + Y, h : X \leadsto Y\) be setoid functions, such that \((id + h) \circ f \doteq g \circ h\). We need to show that \(f^\sharp\;x \approx g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h) \circ f \doteq g \circ h\), we only need to consider two cases: % chktex 2
|
\item \ref{law:uniformity}: Let \(Y\) be a setoid and \(g : Y ⇝ \dbtilde{D}\;A + Y, h : X ⇝ Y\) be setoid functions, such that \((id + h) \circ f \doteq g \circ h\). We need to show that \(f^\sharp\;x \approx g^\sharp(h\;x)\), for any \(x : X\). Let us proceed by case distinction over \(f\;x\) and \(g (h\;x)\), note that by the requisite equation \((id + h) \circ f \doteq g \circ h\), we only need to consider two cases: % chktex 2
|
||||||
\begin{mycase}
|
\begin{mycase}
|
||||||
\case{} \(f\;x = i_1\;a\) and \(g (h\;x) = i_1\;b\)\\
|
\case{} \(f\;x = i_1\;a\) and \(g (h\;x) = i_1\;b\)\\
|
||||||
Consider that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_1 \; a \overset{+}{=} i_1 \; b\) and thus \(a \approx b\). Then indeed,
|
Consider that \((id + h) \circ f \doteq g \circ h\) on \(x\) yields \(i_1 \; a \overset{+}{=} i_1 \; b\) and thus \(a \approx b\). Then indeed,
|
||||||
|
|
@ -199,7 +199,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
|
||||||
We are done by coinduction, which yields
|
We are done by coinduction, which yields
|
||||||
\[f^\sharp\;x \approx later(f^\sharp\;a) \approx later(g^\sharp(h\;a)) \approx later(g^\sharp\;b) \approx g^\sharp (h\;x).\]
|
\[f^\sharp\;x \approx later(f^\sharp\;a) \approx later(g^\sharp(h\;a)) \approx later(g^\sharp\;b) \approx g^\sharp (h\;x).\]
|
||||||
\end{mycase}
|
\end{mycase}
|
||||||
\item \ref{law:folding}: Let \(Y\) be a setoid and \(h : Y \leadsto X + Y\) a setoid function, we need to show that \({(f^\sharp + h)}^\sharp\;z \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp\;z\) for any \(z : X + Y\). % chktex 2
|
\item \ref{law:folding}: Let \(Y\) be a setoid and \(h : Y ⇝ X + Y\) a setoid function, we need to show that \({(f^\sharp + h)}^\sharp\;z \approx {[ (id + i_1) \circ f , i_2 \circ h ]}^\sharp\;z\) for any \(z : X + Y\). % chktex 2
|
||||||
Let us first establish the following fact
|
Let us first establish the following fact
|
||||||
\[f^\sharp\;c \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c) \qquad \text{for any } c : X, \tag{*}\label{folding-helper}\]
|
\[f^\sharp\;c \approx {[(id + i_1) \circ f , i_2 \circ h ]}^\sharp(i_1\;c) \qquad \text{for any } c : X, \tag{*}\label{folding-helper}\]
|
||||||
which follows by case distinction on \(f\;c\) and coinduction:
|
which follows by case distinction on \(f\;c\) and coinduction:
|
||||||
|
|
@ -249,7 +249,7 @@ For the rest of this chapter we will abbreviate \(\tilde{D}\;A = (D_A , \sim)\)
|
||||||
In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a setoid \(Z\), we can discretize \(Z\) by replacing the equivalence relation with propositional equality, yielding \(\disc{Z} := (Z, \equiv)\). Now, the following corollary describes how to transform an iteration on \(\dbtilde{D}\;A\) into an iteration on \(\tilde{D}\;A\).
|
In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a setoid \(Z\), we can discretize \(Z\) by replacing the equivalence relation with propositional equality, yielding \(\disc{Z} := (Z, \equiv)\). Now, the following corollary describes how to transform an iteration on \(\dbtilde{D}\;A\) into an iteration on \(\tilde{D}\;A\).
|
||||||
|
|
||||||
\begin{corollary}\label{cor:discretize}
|
\begin{corollary}\label{cor:discretize}
|
||||||
Given a setoid function \(g : X \leadsto \dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X} \leadsto \tilde{D}\;A + \disc{X}\) such that \(g^\sharp\;x \sim \bar{g}^{\tilde{\sharp}}\;x\) for any \(x : X\).
|
Given a setoid function \(g : X ⇝ \dbtilde{D}\;A + X\). There exists a setoid function \(\bar{g} : \disc{X} ⇝ \tilde{D}\;A + \disc{X}\) such that \(g^\sharp\;x \sim \bar{g}^{\tilde{\sharp}}\;x\) for any \(x : X\).
|
||||||
\end{corollary}
|
\end{corollary}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
It is clear that propositional equality implies strong bisimilarity and thus \(\bar{g}\) is a setoid function that behaves as \(g\) does but with a different type profile.
|
It is clear that propositional equality implies strong bisimilarity and thus \(\bar{g}\) is a setoid function that behaves as \(g\) does but with a different type profile.
|
||||||
|
|
@ -267,20 +267,20 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
|
||||||
Every \(\dbtilde{D}\;A\) can be equipped with a free Elgot algebra structure.
|
Every \(\dbtilde{D}\;A\) can be equipped with a free Elgot algebra structure.
|
||||||
\end{theorem}
|
\end{theorem}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid function \(now : A \leadsto \dbtilde{D}\;A\) is a free such algebra.
|
We build on \autoref{lem:Delgot}, it thus suffices to show that for any setoid \(A\), the Elgot algebra \((\dbtilde{D}\;A, {(-)}^\sharp)\) together with the setoid function \(now : A ⇝ \dbtilde{D}\;A\) is a free such algebra.
|
||||||
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid function \(f : A \leadsto B\). We need to define an Elgot algebra function \(\free{f} : \dbtilde{D}\;A \leadsto B\). Consider \(g : \tilde{D}\;A \leadsto B + \tilde{D}\;A\) defined by
|
Given an Elgot algebra \((B, {(-)}^{\sharp_b})\) and a setoid function \(f : A ⇝ B\). We need to define an Elgot algebra function \(\free{f} : \dbtilde{D}\;A ⇝ B\). Consider \(g : \tilde{D}\;A ⇝ B + \tilde{D}\;A\) defined by
|
||||||
\[g\;x =
|
\[g\;x =
|
||||||
\begin{cases}
|
\begin{cases}
|
||||||
i_1(f\;a) & \text{if } x = now\;a \\
|
i_1(f\;a) & \text{if } x = now\;a \\
|
||||||
i_2\;a & \text{if } x = later\;a
|
i_2\;a & \text{if } x = later\;a
|
||||||
\end{cases}\]
|
\end{cases}\]
|
||||||
|
|
||||||
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}.
|
\(g\) trivially respects strong bisimilarity, thus consider \(g^{\sharp_b} : \tilde{D}\;A ⇝ B\). We need to show that \(g^{\sharp_b}\) also respects weak bisimilarity, thus yielding the requisite function \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A ⇝ B\). However, the proof turns out to be rather complex, let us postpone it to~\autoref{cor:respects}.
|
||||||
|
|
||||||
Instead, we will continue with the proof. Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X \leadsto \dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\). Using \autoref{cor:discretize} we will proceed to show
|
Instead, we will continue with the proof. Let us now show that \(g^{\sharp_b}\) is iteration preserving. Given a setoid function \(h : X ⇝ \dbtilde{D}\;A + X\), we need to show that \(g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x\) for any \(x : X\). Using \autoref{cor:discretize} we will proceed to show
|
||||||
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\]
|
\[g^{\sharp_b} (h^\sharp\;x) \overset{B}{=} {((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}\;x.\]
|
||||||
|
|
||||||
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X} \leadsto X\), and thus the second step can be reduced to \({((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}(id\;x)\). % chktex 2
|
The second step instantly follows by \ref{law:uniformity}, considering that the identity function easily extends to a setoid function \(id : \disc{X} ⇝ X\), and thus the second step can be reduced to \({((g^{\sharp_b} + id) \circ \bar{h})}^{\sharp_b}\;x \overset{B}{=} {((g^{\sharp_b} + id) \circ h)}^{\sharp_b}(id\;x)\). % chktex 2
|
||||||
For the first step consider
|
For the first step consider
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
& g^{\sharp_b} (h^\sharp\;x)
|
& g^{\sharp_b} (h^\sharp\;x)
|
||||||
|
|
@ -291,15 +291,15 @@ In the next proof a notion of \emph{discretized} setoid is needed, i.e.\ given a
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Thus, \(g^{\sharp_b}\) is an Elgot algebra function. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b} \circ now \doteq [ id , g^\sharp_b ] \circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
|
Thus, \(g^{\sharp_b}\) is an Elgot algebra function. We are left to check that \(g^{\sharp_b}\) satisfies the requisite properties of free objects. First, note that \(g^{\sharp_b} \circ now \doteq [ id , g^\sharp_b ] \circ g \circ now \doteq f\) by \ref{law:fixpoint} and the definition of \(g\). % chktex 2
|
||||||
Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra functions \(e, h : \dbtilde{D}\;A \leadsto B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
|
Next, we need to check uniqueness of \(g^{\sharp_b}\). It suffices to show that any two Elgot algebra functions \(e, h : \dbtilde{D}\;A ⇝ B\) satisfying \(e \circ now \doteq f\) and \(h \circ now \doteq f\) are equal.
|
||||||
|
|
||||||
First, note that the identity function can be extended to the following conversion setoid function \(conv : \tilde{D}\;A \leadsto \dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid function \(o : \tilde{D}\;A \leadsto \tilde{D}\;A + \tilde{D}\;A\) defined by
|
First, note that the identity function can be extended to the following conversion setoid function \(conv : \tilde{D}\;A ⇝ \dbtilde{D}\;A\), since strong bisimilarity implies weak bisimilarity. Furthermore, consider the setoid function \(o : \tilde{D}\;A ⇝ \tilde{D}\;A + \tilde{D}\;A\) defined by
|
||||||
\[o\;x := \begin{cases}
|
\[o\;x := \begin{cases}
|
||||||
i_1(now\;z) & \text{if } x = now\;z \\
|
i_1(now\;z) & \text{if } x = now\;z \\
|
||||||
i_2\;z & \text{if } x = later\;z
|
i_2\;z & \text{if } x = later\;z
|
||||||
\end{cases}\]
|
\end{cases}\]
|
||||||
Now, by coinduction we can easily follow that
|
Now, by coinduction we can easily follow that
|
||||||
\[x \approx {((conv + id) \circ o)}^\sharp\;x \qquad \text{for any } x : D\;A.\tag{\(\Asterisk\)}\label{uniq-helper}\]
|
\[x \approx {((conv + id) \circ o)}^\sharp\;x \qquad \text{for any } x : D\;A.\tag{\(∗\)}\label{uniq-helper}\]
|
||||||
|
|
||||||
Let us now return to the proof of uniqueness. We proceed by
|
Let us now return to the proof of uniqueness. We proceed by
|
||||||
\begin{alignat*}{1}
|
\begin{alignat*}{1}
|
||||||
|
|
@ -380,7 +380,7 @@ Lastly, consider the function \(\iota : A \times \mathbb{N} \rightarrow D\;A\),
|
||||||
later(\iota\;(a, m)) & \text{if } n = m + 1
|
later(\iota\;(a, m)) & \text{if } n = m + 1
|
||||||
\end{cases}\]
|
\end{cases}\]
|
||||||
|
|
||||||
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times \mathbb{N} \leadsto \tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality.
|
Trivially, \(\iota\) can be extended to a setoid function \(\iota : A \times \mathbb{N} ⇝ \tilde{D}\;A\), where the equivalence on \(\mathbb{N}\) is propositional equality.
|
||||||
Let us state two facts about \(\Delta\), the proofs can again be found in the formalization.
|
Let us state two facts about \(\Delta\), the proofs can again be found in the formalization.
|
||||||
\begin{corollary}\label{cor:delta}
|
\begin{corollary}\label{cor:delta}
|
||||||
\(\Delta\) satisfies the following properties:
|
\(\Delta\) satisfies the following properties:
|
||||||
|
|
@ -393,7 +393,7 @@ Let us state two facts about \(\Delta\), the proofs can again be found in the fo
|
||||||
Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
|
Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
|
||||||
|
|
||||||
\begin{corollary}\label{cor:respects}
|
\begin{corollary}\label{cor:respects}
|
||||||
The setoid function \(g^{\sharp_b} : \tilde{D}\;A \leadsto B\) defined in \autoref{thm:Dfreeelgot} respects weak bisimilarity, thus yielding \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A \leadsto B\).
|
The setoid function \(g^{\sharp_b} : \tilde{D}\;A ⇝ B\) defined in \autoref{thm:Dfreeelgot} respects weak bisimilarity, thus yielding \(\free{f} = g^{\sharp_b} : \dbtilde{D}\;A ⇝ B\).
|
||||||
\end{corollary}
|
\end{corollary}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(x, y : D\;A\) such that \(x \approx y\). Recall that by \autoref{cor:race} \(x \approx y\) implies \(p: race\;x\;y \lesssim y\) and symmetrically \(q: race\;y\;x \lesssim x\), now, using Corollaries~\ref{cor:race} and~\ref{cor:delta}:
|
Let \(x, y : D\;A\) such that \(x \approx y\). Recall that by \autoref{cor:race} \(x \approx y\) implies \(p: race\;x\;y \lesssim y\) and symmetrically \(q: race\;y\;x \lesssim x\), now, using Corollaries~\ref{cor:race} and~\ref{cor:delta}:
|
||||||
|
|
@ -419,7 +419,7 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
|
||||||
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
|
\\\overset{B}{=}\;&g^{\sharp_b}(\iota^*\;z). \tag{\ref{law:uniformity}}
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Which leaves us to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) \leadsto B + \tilde{D} (A \times \mathbb{N})\). Consider,
|
Which leaves us to find suitable \(g_1, g_2 : \tilde{D}(A \times \mathbb{N}) ⇝ B + \tilde{D} (A \times \mathbb{N})\). Consider,
|
||||||
\[g_1\;p := \begin{cases}
|
\[g_1\;p := \begin{cases}
|
||||||
i_1(f\;x) & \text{if } p = now\;(x, zero) \\
|
i_1(f\;x) & \text{if } p = now\;(x, zero) \\
|
||||||
i_2(\tilde{D}o (\iota\;(x,n))) & \text{if } p = now\;(x, n + 1) \\
|
i_2(\tilde{D}o (\iota\;(x,n))) & \text{if } p = now\;(x, n + 1) \\
|
||||||
|
|
@ -430,11 +430,11 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
|
||||||
i_1(f\;x) & \text{if } p = now\;(x , n) \\
|
i_1(f\;x) & \text{if } p = now\;(x , n) \\
|
||||||
i_2\;q & \text{if } p = later\;q
|
i_2\;q & \text{if } p = later\;q
|
||||||
\end{cases}\]
|
\end{cases}\]
|
||||||
where \(o : A \leadsto A \times \mathbb{N}\) is a setoid function that maps every \(z : A\) to \((z , 0) : A \times \mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota \circ o \doteq now\). % chktex 2
|
where \(o : A ⇝ A \times \mathbb{N}\) is a setoid function that maps every \(z : A\) to \((z , 0) : A \times \mathbb{N}\). The applications of \ref{law:uniformity} are then justified by the definitions of \(g_1\) and \(g_2\) as well as the fact that \(\iota \circ o \doteq now\). % chktex 2
|
||||||
|
|
||||||
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\).
|
We are thus done after showing that \(g_1^{\sharp_b}\;z \overset{B}{=} g_2^{\sharp_b}\;z\).
|
||||||
Consider another setoid function
|
Consider another setoid function
|
||||||
\[g_3 : \tilde{D}(A \times \mathbb{N}) \leadsto B + \tilde{D}(A \times \mathbb{N}) + \tilde{D}(A \times \mathbb{N}),\]
|
\[g_3 : \tilde{D}(A \times \mathbb{N}) ⇝ B + \tilde{D}(A \times \mathbb{N}) + \tilde{D}(A \times \mathbb{N}),\]
|
||||||
defined by
|
defined by
|
||||||
\[g_3\;p := \begin{cases}
|
\[g_3\;p := \begin{cases}
|
||||||
i_1(f\;x) & \text{if } p = now\;(x, 0) \\
|
i_1(f\;x) & \text{if } p = now\;(x, 0) \\
|
||||||
|
|
@ -474,7 +474,7 @@ Let us now return to the missing Corollary of \autoref{thm:Dfreeelgot}.
|
||||||
\end{alignat*}
|
\end{alignat*}
|
||||||
|
|
||||||
Where
|
Where
|
||||||
\[{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n))) \overset{B}{=} f\;y \tag{\(\Asterisk\)}\label{finalhelper}\]
|
\[{((id + [ id , id]) \circ g_3)}^{\sharp_b}(\tilde{D}o(\iota\;(y,n))) \overset{B}{=} f\;y \tag{\(∗\)}\label{finalhelper}\]
|
||||||
follows by induction on \(n\):
|
follows by induction on \(n\):
|
||||||
|
|
||||||
\subcase{} \(n = 0\)\\
|
\subcase{} \(n = 0\)\\
|
||||||
|
|
|
||||||
|
|
@ -18,7 +18,7 @@
|
||||||
{% maybe \itshape?
|
{% maybe \itshape?
|
||||||
\Huge\bfseries
|
\Huge\bfseries
|
||||||
\makeatletter
|
\makeatletter
|
||||||
\@title \\[1cm]
|
\@title \\[1cm] % chktex 1
|
||||||
\makeatother
|
\makeatother
|
||||||
% \large\bfseries
|
% \large\bfseries
|
||||||
% \\ and \ldots
|
% \\ and \ldots
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue