mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
squash warnings
This commit is contained in:
parent
2dbf69bcf6
commit
f37458fe97
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
8 changed files with 135 additions and 123 deletions
3
thesis/.vscode/ltex.dictionary.en-US.txt
vendored
3
thesis/.vscode/ltex.dictionary.en-US.txt
vendored
|
|
@ -71,3 +71,6 @@ copatterns
|
|||
epimorphisms
|
||||
monomorphisms
|
||||
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":"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[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":"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":"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,
|
||||
autogobble
|
||||
}
|
||||
% \usepackage{mathabx}
|
||||
% \usepackage{amssymb}
|
||||
\usepackage[dvipsnames]{xcolor} % Coloured text etc.
|
||||
\usepackage{amssymb}
|
||||
\usepackage{amsthm}
|
||||
\usepackage{thmtools}
|
||||
\usepackage{thmtools}
|
||||
\usepackage{fancyvrb}
|
||||
\usepackage{mathtools}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{mathabx}
|
||||
% \usepackage{mathtools}
|
||||
% \usepackage{amsmath}
|
||||
\usepackage{mathpartir}
|
||||
% packages for draft version
|
||||
\usepackage{lineno}
|
||||
\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!
|
||||
\makeatletter
|
||||
\let\atop\@@atop
|
||||
\let\atop\@@atop % chktex 1
|
||||
\makeatother
|
||||
|
||||
\usepackage{tikz}
|
||||
\usetikzlibrary{cd, babel, quotes}
|
||||
\usepackage{quiver}
|
||||
\usepackage{stmaryrd} % for \llbracket and \rrbracket
|
||||
% \usepackage{stmaryrd} % for \llbracket and \rrbracket
|
||||
\usepackage{ifthen}
|
||||
\usepackage{xspace}
|
||||
\usepackage[final]{hyperref}
|
||||
|
|
@ -108,7 +107,6 @@
|
|||
|
||||
|
||||
\usepackage[scale=.8]{noto-mono}
|
||||
\usepackage{unicode-math}
|
||||
|
||||
\usepackage{mathrsfs}
|
||||
\usepackage{xargs}
|
||||
|
|
@ -225,8 +223,6 @@
|
|||
}
|
||||
\makeatother
|
||||
|
||||
\ifdraft{\linenumbers}
|
||||
|
||||
\include{src/01_introduction}
|
||||
\include{src/02_preliminaries}
|
||||
\include{src/03_agda-categories}
|
||||
|
|
@ -241,6 +237,7 @@
|
|||
|
||||
\medskip
|
||||
|
||||
\emergencystretch=1em
|
||||
\printbibliography[heading=bibintoc]{}
|
||||
|
||||
\end{document}
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
% `tikz-cd` is necessary to draw commutative diagrams.
|
||||
\RequirePackage{tikz-cd}
|
||||
% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
|
||||
\RequirePackage{amssymb}
|
||||
% \RequirePackage{amssymb}
|
||||
% `calc` is necessary to draw curved arrows.
|
||||
\usetikzlibrary{calc}
|
||||
% `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.
|
||||
\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
|
||||
.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||
.. (\tikztotarget)\tikztonodes}},
|
||||
settings/.code={\tikzset{quiver/.cd,#1}
|
||||
\def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
|
||||
quiver/.cd,pos/.initial=0.35,height/.initial=0}
|
||||
.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
|
||||
.. (\tikztotarget)\tikztonodes}},
|
||||
settings/.code={\tikzset{quiver/.cd,#1}
|
||||
\def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
|
||||
quiver/.cd,pos/.initial=0.35,height/.initial=0}
|
||||
|
||||
% TikZ arrowhead/tail styles.
|
||||
\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
|
||||
|
|
|
|||
|
|
@ -54,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\),
|
||||
\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\),
|
||||
\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)\).
|
||||
\end{itemize}
|
||||
\end{lemma}
|
||||
|
|
@ -109,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
|
||||
First, note that
|
||||
\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*}
|
||||
by \ref{law:fixpoint} and \ref{law:uniformity}: % chktex 2
|
||||
\begin{alignat*}{1}
|
||||
|
|
@ -166,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.
|
||||
|
||||
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\).
|
||||
|
||||
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\).
|
||||
|
||||
Let us also consider the special case where \(X = 1\).
|
||||
|
|
@ -233,12 +233,12 @@ Products and exponentials of Elgot algebras can be formed in a canonical way, wh
|
|||
|
||||
Then,~\ref{law:uniformity} of \({(-)}^{\sharp_a}\) and \({(-)}^{\sharp_b}\) with the previous two equations yields:
|
||||
\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
|
||||
\end{alignat*}
|
||||
|
||||
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:
|
||||
\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}
|
||||
|
|
@ -374,13 +374,13 @@ Let us first recall the following notion that was introduced in~\cite{elgotmonad
|
|||
\\ for any \(f : X \rightarrow T(Y + X)\),
|
||||
\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\),
|
||||
\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\),
|
||||
\item \textbf{Codiagonal}: \({f^\dag}^\dag = {(T[id , i_2] \circ f)}^\dag\)
|
||||
\\ for any \(f : X \rightarrow T((Y + X) + X)\).
|
||||
\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}
|
||||
|
||||
We regard Elgot monads as minimal semantic structures for interpreting side-effecting while loops, as has been argued in~\cite{goncharov2018unguarded, goncharov2017unifying}.
|
||||
|
|
@ -726,8 +726,8 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
|||
\begin{corollary}
|
||||
\(\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}
|
||||
& \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}
|
||||
& \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}
|
||||
\end{alignat*}
|
||||
\end{corollary}
|
||||
\begin{proof}
|
||||
|
|
@ -754,7 +754,7 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
|||
\begin{itemize}
|
||||
\item[(\ref{Ktau1})]
|
||||
\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 \tau \circ (id \times Kg) \circ (f^* \times id)
|
||||
\\=\;&\tau \circ (id \times \mu) \circ (id \times Kg) \circ (f^* \times id)
|
||||
|
|
@ -764,7 +764,7 @@ As we did when proving commutativity of \(\mathbf{D}\), let us record some facts
|
|||
|
||||
\item[(\ref{Ksigma1})]
|
||||
\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 \sigma \circ (Kf \times id) \circ (id \times g^*)
|
||||
\\=\;&\sigma \circ (\mu \times id) \circ (Kf \times id) \circ (id \times g^*)
|
||||
|
|
@ -783,65 +783,65 @@ The following Lemma is central to the proof of commutativity.
|
|||
\begin{proof}
|
||||
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
|
||||
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}
|
||||
& \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 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 Kswap \circ \tau \circ \Delta \circ w^\sharp
|
||||
\\=\;&\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}}
|
||||
\\=\;&\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 {[ \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 Kswap \circ \tau \circ \Delta \circ w^\sharp
|
||||
\\=\;&\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}}
|
||||
\\=\;&\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 \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 [\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 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,
|
||||
\\=\;&{([\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
|
||||
\\=\;&{([\sigma \circ (\hat{f}^\sharp \times id) , \tau \circ (id \times \hat{g}^\sharp)])}^* \circ w^\sharp,
|
||||
\end{alignat*}
|
||||
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 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
|
||||
\[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 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,
|
||||
\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 ]^* + 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 (\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 \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 [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 , ((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 + \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 [ 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 \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 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))^\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
|
||||
\\=\;&{([ 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 ((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 , ((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 \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 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 [ 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 \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 , (\hat{f}^\sharp \circ \pi_1 + id) \circ dstl ] \circ dstr \circ (\hat{f} \times g))}^\sharp
|
||||
\end{alignat*}
|
||||
and
|
||||
\begin{alignat*}{1}
|
||||
& \hat{f}^\sharp \circ \pi_1
|
||||
\\=\;&((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 , (\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) + 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 \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,
|
||||
\\=\;&{((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 , (\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) + 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 \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,
|
||||
\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 % chktex 2
|
||||
|
|
@ -908,8 +908,8 @@ The following Lemma is central to the proof of commutativity.
|
|||
\\=\;&\psi \circ (\eta \times id) \circ (id \times h^\sharp)
|
||||
\\=\;&\tau^* \circ \eta \circ (id \times h^\sharp)
|
||||
\\=\;&\tau \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}}
|
||||
\\=\;&{((\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}}
|
||||
\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
|
||||
|
|
|
|||
|
|
@ -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}{=}\).
|
||||
|
||||
\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}
|
||||
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]
|
||||
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}
|
||||
|
||||
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}
|
||||
\item \textbf{Products}:
|
||||
\begin{minted}{agda}
|
||||
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
constructor _,_
|
||||
field
|
||||
fst : A
|
||||
snd : B
|
||||
|
||||
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → B) → (A → C) → A → (B × C)
|
||||
< f , g > x = (f x , g x)
|
||||
\end{minted}
|
||||
record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
constructor _,_
|
||||
field
|
||||
fst : A
|
||||
snd : B
|
||||
|
||||
<_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → B) → (A → C) → A → (B × C)
|
||||
< f , g > x = (f x , g x)
|
||||
\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.
|
||||
\item \textbf{Terminal Object}:
|
||||
\begin{minted}{agda}
|
||||
record ⊤ {l} : Set l where
|
||||
constructor tt
|
||||
|
||||
! : ∀ {l} {X : Set l} → X → ⊤ {l}
|
||||
! _ = tt
|
||||
\end{minted}
|
||||
record ⊤ {l} : Set l where
|
||||
constructor tt
|
||||
|
||||
! : ∀ {l} {X : Set l} → X → ⊤ {l}
|
||||
! _ = tt
|
||||
\end{minted}
|
||||
The terminal setoid is thus \((\top, \overset{\top}{=})\), where \(\top \overset{\top}{=} \top\).
|
||||
\item \textbf{Coproducts}:
|
||||
\begin{minted}{agda}
|
||||
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
i₁ : A → A + B
|
||||
i₂ : B → A + B
|
||||
|
||||
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → C) → (B → C) → (A + B) → C
|
||||
[ f , g ] (i₁ x) = f x
|
||||
[ f , g ] (i₂ x) = g x
|
||||
\end{minted}
|
||||
data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
|
||||
i₁ : A → A + B
|
||||
i₂ : B → A + B
|
||||
|
||||
[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (A → C) → (B → C) → (A + B) → C
|
||||
[ f , g ] (i₁ x) = f x
|
||||
[ f , g ] (i₂ x) = g x
|
||||
\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.
|
||||
\item \textbf{Initial Object}:
|
||||
\begin{minted}{agda}
|
||||
data ⊥ {l} : Set l where
|
||||
data ⊥ {l} : Set l where
|
||||
|
||||
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
|
||||
¡ ()
|
||||
\end{minted}
|
||||
¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
|
||||
¡ ()
|
||||
\end{minted}
|
||||
The initial setoid is then \((\bot, \emptyset)\), where the equivalence is the empty relation.
|
||||
\end{itemize}
|
||||
|
||||
|
|
@ -94,7 +94,7 @@ Setoids together with setoid functions form a category that we will call \(\seto
|
|||
\(\setoids\) is Cartesian closed.
|
||||
\end{proposition}
|
||||
\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}
|
||||
curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
|
||||
→ (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}
|
||||
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 :=
|
||||
\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\)
|
||||
\[ 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}
|
||||
\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}
|
||||
\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,
|
||||
|
|
@ -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
|
||||
\[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}
|
||||
\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
|
||||
\[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:
|
||||
|
|
@ -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\).
|
||||
|
||||
\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}
|
||||
\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.
|
||||
|
|
@ -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.
|
||||
\end{theorem}
|
||||
\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.
|
||||
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
|
||||
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 ⇝ 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 =
|
||||
\begin{cases}
|
||||
i_1(f\;a) & \text{if } x = now\;a \\
|
||||
i_2\;a & \text{if } x = later\;a
|
||||
\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.\]
|
||||
|
||||
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
|
||||
\begin{alignat*}{1}
|
||||
& 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*}
|
||||
|
||||
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}
|
||||
i_1(now\;z) & \text{if } x = now\;z \\
|
||||
i_2\;z & \text{if } x = later\;z
|
||||
\end{cases}\]
|
||||
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
|
||||
\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
|
||||
\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.
|
||||
\begin{corollary}\label{cor:delta}
|
||||
\(\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}.
|
||||
|
||||
\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}
|
||||
\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}:
|
||||
|
|
@ -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}}
|
||||
\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}
|
||||
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) \\
|
||||
|
|
@ -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_2\;q & \text{if } p = later\;q
|
||||
\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\).
|
||||
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
|
||||
\[g_3\;p := \begin{cases}
|
||||
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*}
|
||||
|
||||
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\):
|
||||
|
||||
\subcase{} \(n = 0\)\\
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@
|
|||
{% maybe \itshape?
|
||||
\Huge\bfseries
|
||||
\makeatletter
|
||||
\@title \\[1cm]
|
||||
\@title \\[1cm] % chktex 1
|
||||
\makeatother
|
||||
% \large\bfseries
|
||||
% \\ and \ldots
|
||||
|
|
|
|||
Loading…
Reference in a new issue