diff --git a/thesis/main.tex b/thesis/main.tex index cb09468..7619561 100644 --- a/thesis/main.tex +++ b/thesis/main.tex @@ -99,6 +99,8 @@ \usepackage{noto-mono} +\usepackage{mathpazo} +\usepackage{unicode-math} \usepackage{mathrsfs} \usepackage[colorinlistoftodos,prependcaption,textsize=tiny]{todonotes} \usepackage{xargs} @@ -106,6 +108,43 @@ %\usepackage{fontspec} %\setmonofont{Noto Sans Mono} +\usepackage{pict2e} + +% \newcommand{\lbparen}{% +% \mathopen{% +% \sbox0{$()$}% +% \setlength{\unitlength}{\dimexpr\ht0+\dp0}% +% \raisebox{-\dp0}{% +% \begin{picture}(.32,1) +% \linethickness{\fontdimen8\textfont3} +% \roundcap +% \put(0,0){\raisebox{\depth}{$($}} +% \polyline(0.32,0)(0.1,0)(0.1,1)(0.32,1) +% \end{picture}% +% }% +% }% +% } + +% \newcommand{\rbparen}{% +% \mathclose{% +% \sbox0{$()$}% +% \setlength{\unitlength}{\dimexpr\ht0+\dp0}% +% \raisebox{-\dp0}{% +% \begin{picture}(.32,1) +% \linethickness{\fontdimen8\textfont3} +% \roundcap +% \put(0.02,0){\raisebox{\depth}{$)$}} +% \polyline(0.1,0)(0.32,0)(0.32,1)(0.1,1) +% \end{picture}% +% }% +% }% +% } + +\newcommand{\lbparen}{〖} +% https://unicodeplus.com/U+3016 + +\newcommand{\rbparen}{〗} + % category C \newcommand*{\C}{\ensuremath{\mathscr{C}}} \newcommand*{\D}{\ensuremath{\mathscr{D}}} @@ -142,7 +181,7 @@ } } % terminal coalgebra -\newcommand*{\coalg}[1]{\ensuremath{\llbracket #1 \rrbracket}} +\newcommand*{\coalg}[1]{\ensuremath{\lbparen#1\rbparen}} \begin{document} \pagestyle{plain} @@ -168,6 +207,7 @@ Erlangen, \today{} \rule{7cm}{1pt}\\ \newcommandx{\info}[2][1=]{\todo[inline,linecolor=OliveGreen,backgroundcolor=OliveGreen!25,bordercolor=OliveGreen,#1]{#2}} \newcommandx{\improvement}[2][1=]{\todo[inline,linecolor=Plum,backgroundcolor=Plum!25,bordercolor=Plum,#1]{#2}} + % for creating custom labels like (Fixpoint) \makeatletter \newcommand{\customlabel}[2]{% diff --git a/thesis/src/03_partiality-monads.tex b/thesis/src/03_partiality-monads.tex index d5a8f5e..bd4dbe6 100644 --- a/thesis/src/03_partiality-monads.tex +++ b/thesis/src/03_partiality-monads.tex @@ -357,11 +357,12 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ \arrow["out", from=3-1, to=3-5] \arrow["{id \times out}", from=1-1, to=1-2] \arrow["dstl", from=1-2, to=1-3] - \arrow["{\coalg{-}}", dashed, from=1-1, to=3-1] + \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1] \arrow["{f \times g + id}", from=1-3, to=1-5] - \arrow["{id + \coalg{-}}", dashed, from=1-5, to=3-5] + \arrow["{id + \coalg{\text{-}}}", dashed, from=1-5, to=3-5] \end{tikzcd}\] - We write $\coalg{-}$ to abbreviate the used coalgebra, i.e.\ in this diagram $\coalg{-} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}$ + We write $\coalg{\text{-}}$ to abbreviate the used coalgebra, i.e.\ in the previous diagram + \[\coalg{\text{-}} = \coalg{(f\times g + id) \circ dstl \circ (id \times out)}.\] Next we check the strength laws: \begin{itemize} @@ -371,8 +372,8 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ {1 \times DX} \& {1 \times X + DX} \& {1 \times X + 1 \times DX} \& {X + 1 \times DX} \\ DX \&\&\& {X + DX} \arrow["out", from=2-1, to=2-4] - \arrow["{\coalg{-}}", dashed, from=1-1, to=2-1] - \arrow["{id + \coalg{-}}", from=1-4, to=2-4] + \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1] + \arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4] \arrow["{id \times out}", from=1-1, to=1-2] \arrow["dstl", from=1-2, to=1-3] \arrow["{\pi_2 + id}", from=1-3, to=1-4] @@ -396,11 +397,11 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ {X \times DDY} \& {X \times (DY + DDY)} \& {X \times DY + X \times DDY} \\ \&\& {X \times Y + X \times DDY} \\ {D(X\times Y)} \&\& {X \times Y + D(X \times Y)} - \arrow["{\coalg{-}}", dashed, from=1-1, to=3-1] + \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1] \arrow["{id \times out}", from=1-1, to=1-2] \arrow["dstl", from=1-2, to=1-3] \arrow["out", from=3-1, to=3-3] - \arrow["{id + \coalg{-}}"', from=2-3, to=3-3] + \arrow["{id + \coalg{\text{-}}}"', from=2-3, to=3-3] \arrow["{[ (id + (id \times now)) \circ dstl \circ (id \times out) , i_2 ]}"', from=1-3, to=2-3] \end{tikzcd}\] \item[\ref{S4}] To show $D\alpha \circ \tau = \tau \circ (id \times \tau) \circ \alpha$ by coinduction we take the coalgebra: @@ -409,9 +410,9 @@ Finality of the coalgebras $(DX, out : DX \rightarrow X + DX)_{X \in \obj{\C}}$ {(X \times Y) \times DZ} \& {(X \times Y) \times (Z+ DZ)} \& {(X\times Y) \times Z + (X \times Y) \times DZ} \\ \&\& {X \times Y \times Z + (X \times Y) \times DZ} \\ {D(X \times Y \times Z)} \&\& {X \times Y \times Z + D(X \times Y \times Z)} - \arrow["{\coalg{-}}", dashed, from=1-1, to=3-1] + \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=3-1] \arrow["out", from=3-1, to=3-3] - \arrow["{id +\coalg{-}}"', from=2-3, to=3-3] + \arrow["{id +\coalg{\text{-}}}"', from=2-3, to=3-3] \arrow["{id \times out}", from=1-1, to=1-2] \arrow["dstl", from=1-2, to=1-3] \arrow["{\langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle + id}"', from=1-3, to=2-3] @@ -451,8 +452,8 @@ To prove that $\mathbf{D}$ is commutative we will use another proof principle pr \arrow["out", from=2-1, to=2-4] \arrow["out", from=1-1, to=1-2] \arrow["{[ [ i_1 , h ] , i_2 ]}", from=1-2, to=1-4] - \arrow["{id + \coalg{-}}", from=1-4, to=2-4] - \arrow["{\coalg{-}}", dashed, from=1-1, to=2-1] + \arrow["{id + \coalg{\text{-}}}", from=1-4, to=2-4] + \arrow["{\coalg{\text{-}}}", dashed, from=1-1, to=2-1] \end{tikzcd}\] \end{proof}