CategoryTheory/algprog
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Export macros to catprog.sty, work on F-algebras section

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-27 10:35:12 +01:00
parent 64cbc50601
commit 1317daa802
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
7 changed files with 651 additions and 162 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tex/.vscode/ltex.dictionary.en-US.txt vendored
View file

@ -37,3 +37,9 @@ monoids
n-ary
Cocartesian
Yoneda
endofunctor
F-Coalgebras
Corecursion
Coinduction
Colimits
Colimit

4
tex/.vscode/settings.json vendored
View file

@ -27,6 +27,8 @@
"ltex.latex.commands": {
"\\customlabel{}": "ignore",
"\\setminted[]{}": "ignore",
"\\setmintedinline[]{}": "ignore"
"\\setmintedinline[]{}": "ignore",
"\\setmathfont[]{}": "ignore",
"\\setmathfont{}": "ignore"
}
}

221
tex/catprog.sty Normal file
View file

@ -0,0 +1,221 @@
%
% Standard macros to typeset papers on category theory and semantics
%
% Unless \catname is defined, make it bold.
% So, call \providecommand{\catname}{\mathcal}
% or \reprovidecommand{\catname}{\mathcal}
% before calling this file if you prefer calligraphic names for categories.
%
% Same applies to other commands.
%
% COPIED FROM https://gitlab.cs.fau.de/i8/TexCommon/ AND THEN ADJUSTED.
\RequirePackage{bm} % Needed for defbbname
\RequirePackage{mathtools} % Needed for coloneqq
\providecommand{\catname}{\mathsf}
%\providecommand{\mndname}{\mathbbb}
\providecommand{\clsname}{\mathscr}
\providecommand{\oname}[1]{\operatorname{\mathsf{#1}}}
%% Defining category names like \BA, \BB, etc
\def\defcatname#1{\expandafter\def\csname B#1\endcsname{\catname{#1}}}
\def\defcatnames#1{\ifx#1\defcatnames\else\defcatname#1\expandafter\defcatnames\fi}
\defcatnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defcatnames
%% Defining \CA, \CB, etc
\def\defclsname#1{\expandafter\def\csname C#1\endcsname{\clsname{#1}}}
\def\defclsnames#1{\ifx#1\defclsnames\else\defclsname#1\expandafter\defclsnames\fi}
\defclsnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defclsnames
%% Defining \BBA, \BBB, etc
\def\defbbname#1{\expandafter\def\csname BB#1\endcsname{{\bm{\mathsf{#1}}}}}
\def\defbbnames#1{\ifx#1\defbbnames\else\defbbname#1\expandafter\defbbnames\fi}
\defbbnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defbbnames
%% Defining \BMA, \BMB, etc
\def\defbbname#1{\expandafter\def\csname BM#1\endcsname{{\bm{\mathsf{#1}}}}}
\def\defbbnames#1{\ifx#1\defbbnames\else\defbbname#1\expandafter\defbbnames\fi}
\defbbnames ABCDEFGHIJKLMNOPQRSTUVWXYZ\defbbnames
%% Some standard categories
\def\Set{\ensuremath{\catname{Set}}}
\def\Par{\ensuremath{\catname{Par}}}
\def\Rel{\ensuremath{\catname{Rel}}}
\def\Cpo{\ensuremath{\catname{Cpo}}}
\def\Pos{\ensuremath{\catname{Pos}}}
\def\Mon{\ensuremath{\catname{Mon}}}
\def\Gra{\ensuremath{\catname{Gra}}}
\providecommand{\Alg}[1]{\ensuremath{\catname{Alg}(#1)}}
%% Objects of category
\providecommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
%% Dual category
\providecommand{\dual}[1]{\ensuremath{#1^{op}}}
% Misc
%% Commutation of diagrams
\providecommand{\comm}{\circlearrowleft}
%% Banana brackets for catamorphisms
\RequirePackage{stmaryrd}
\providecommand{\cata}[1]{\llparenthesis #1 \rrparenthesis}
\providecommand{\eps}{{\operatorname\epsilon}}
\providecommand{\amp}{\mathbin{\&}}
\providecommand{\argument}{\operatorname{-\!-}}
\providecommand{\altargument}{\underline{\;\;}}
\providecommand{\wave}[1]{\widetilde{#1}} % Overline wave
\providecommand{\ul}{\underline} % Underline
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\providecommand{\mplus}{{\scriptscriptstyle\bf+}} % Small '+' for indexing
\providecommand{\smin}{\smallsetminus}
\providecommand{\ass}{\mathrel{\coloneqq}}
\providecommand{\bnf}{\mathrel{\Coloneqq}}
%% Some standard functors
\providecommand{\PSet}{{\mathcal P}} % Powerset
\providecommand{\FSet}{{\mathcal P}_{\omega}} % Finite powerset
\providecommand{\CSet}{{\mathcal P}_{\omega_1}} % Countable powerset
\providecommand{\NESet}{{\mathcal P}^{\mplus}} % Non-empty powerset
\providecommand{\Id}{\operatorname{Id}}
%% General categorical notation
\providecommand{\Hom}{\mathsf{Hom}}
\providecommand{\id}{\mathsf{id}}
\providecommand{\op}{\mathsf{op}}
\providecommand{\comp}{\mathbin{\circ}}
\providecommand{\iso}{\mathbin{\cong}}
\providecommand{\tensor}{\mathbin{\otimes}}
\providecommand{\unit}{\star}
\providecommand{\bang}{\operatorname!} % Initial/final map
%% Various arrows
\providecommand{\from}{\leftarrow}
\providecommand{\ito}{\hookrightarrow} % Injection
\providecommand{\ifrom}{\hookleftarrow}
\providecommand{\pto}{\mathrel{\rightharpoonup}} % Partial function
\providecommand{\pfrom}{\mathrel{\leftarpoonup}} %
\providecommand{\tto}{\mathrel{\Rightarrow}} % Double arrow
\providecommand{\tfrom}{\mathrel{\Leftarrow}} %
\providecommand{\mto}{\mapsto}
\providecommand{\xto}[1]{\,\xrightarrow{#1}\,}
\providecommand{\xfrom}[1]{\,\xleftarrow{\;#1}\,}
\providecommand{\To}{\mathrel{\Rightarrow}} % Double arrow
\providecommand{\From}{\mathrel{\Leftarrow}}
\providecommand{\dar}{\kern-.75pt\operatorname{\downarrow}}
\providecommand{\uar}{\kern-.75pt\operatorname{\uparrow}}
\providecommand{\Dar}{\kern-.75pt\operatorname{\Downarrow}}
\providecommand{\Uar}{\kern-.75pt\operatorname{\Uparrow}}
%% Logic
\providecommand{\True}{\top}
\providecommand{\False}{\bot}
\providecommand{\bigor}{\bigvee}
\providecommand{\bigand}{\bigwedge}
\providecommand{\impl}{\Rightarrow}
\providecommand{\equ}{\Longleftrightarrow}
\providecommand{\entails}{\vdash}
%% Order
\providecommand{\appr}{\sqsubseteq}
\providecommand{\join}{\sqcup}
\providecommand{\meet}{\sqcap}
\providecommand{\bigjoin}{\bigsqcup}
\providecommand{\bigmeet}{\bigsqcap}
%% Products
\providecommand{\fst}{\oname{fst}}
\providecommand{\snd}{\oname{snd}}
\providecommand{\pr}{\oname{pr}}
\providecommand{\brks}[1]{\langle #1\rangle}
\providecommand{\Brks}[1]{\bigl\langle #1\bigr\rangle}
%% Coproducts
\providecommand{\inl}{\oname{inl}}
\providecommand{\inr}{\oname{inr}}
\providecommand{\inj}{\oname{in}}
\DeclareSymbolFont{Symbols}{OMS}{cmsy}{m}{n}
\DeclareMathSymbol{\iobj}{\mathord}{Symbols}{"3B}
%\DeclareRobustCommand{\iobj}{\emptyset}
%% CCC
\providecommand{\curry}{\oname{curry}}
\providecommand{\uncurry}{\oname{uncurry}}
\providecommand{\ev}{\oname{ev}}
% Semantic brackets
\RequirePackage{stmaryrd}
\providecommand{\lsem}{\llbracket}
\providecommand{\rsem}{\rrbracket}
\providecommand{\sem}[1]{\lsem #1 \rsem}
\providecommand{\Lsem}{\bigl\llbracket}
\providecommand{\Rsem}{\bigr\rrbracket}
\providecommand{\Sem}[1]{\Lsem #1 \Rsem}
% Typographic
\providecommand{\comma}{,\operatorname{}\linebreak[1]} % possibly line-breaking comma
\providecommand{\dash}{\nobreakdash-\hspace{0pt}} % non-line-breaking hyphen
\providecommand{\erule}{\rule{0pt}{0pt}} % Empty object whose emptiness
% is not detected by LaTeX
\providecommand{\by}[1]{\text{/\!\!/~#1}} % Comments in equations
\providecommand{\pacman}[1]{} % Hide a piece of text
\newcommand{\undefine}[1]{\let #1\relax} % Make a command undefined
\providecommand{\noqed}{\def\qed{}} % Undefine the QED symbol
% -1 superscript for the inversion operator
\providecommand{\mone}{{\text{\kern.5pt\rmfamily-}\mathsf{\kern-.5pt1}}}
\makeatletter
\@ifpackageloaded{enumitem}{}{
\RequirePackage[loadonly]{enumitem} % without [loadonly]
} % conflicts with Beamer
\makeatother
% Condensed list environments
\newlist{citemize}{itemize}{1}
\setlist[citemize]{label=\labelitemi,wide}
%leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left}
\newlist{cenumerate}{enumerate}{1}
\setlist[cenumerate,1]{label=\arabic*.~,ref={\arabic*},wide}
%leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left}
%\newenvironment{citemize}{\begin{itemize}[leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left]}{\end{itemize}}
%\newenvironment{cenumerate}{\begin{enumerate}[leftmargin=0cm,itemindent=.7cm,labelwidth=\itemindent,labelsep=-.3cm,align=left]}{\end{enumerate}}
%% A macro for defining mixfix operators
\makeatletter
\def\mfix#1{\oname{#1}\@ifnextchar\bgroup\@mfix{}} % processing odd arguments
\def\@mfix#1{#1\@ifnextchar\bgroup\mfix{}} % processing even arguments
\makeatother
% %% Instances if mfix
% \providecommand{\ift}[3]{\mfix{if}{\mathbin{}#1}{then}{\mathbin{}#2}{else}{\mathbin{}#3}}
% \providecommand{\case}[3]{\mfix{case}{\mathbin{}#1}{of}{#2}{\kern-1pt;}{\mathbin{}#3}}

BIN
tex/main.pdf
View file

Binary file not shown.

22
tex/main.tex
View file

@ -6,9 +6,15 @@
\usepackage[ngerman, english]{babel}
\babeltags{german=ngerman}
\usepackage{anyfontsize}
\usepackage{unicode-math}
\usepackage{mathtools}
\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
\setmathfont[math-style=ISO,version=normal]{Latin Modern Math}
\setmathfont[version=bold,math-style=ISO,FakeBold = 3]{Latin Modern Math}
\setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{XITS Math}
\setmathfont[range=\mathscr]{XITS Math}
\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{stmaryrd}
% \usepackage{mathrsfs}
\usepackage{booktabs}
\usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font
\usepackage[final]{hyperref}
@ -18,7 +24,7 @@
\renewcommand{\subsectionmark}[1]{\markright{\thesubsection\ #1}}
\pagestyle{scrheadings}
\newcounter{resumeenum} % for resuming enumerated lists, https://tex.stackexchange.com/a/1702
\usepackage{catprog}
%%%%
%%%% Metadata
@ -129,14 +135,8 @@
\makeatother
%%%
%%% Notation
%% Categories
\newcommand{\C}{\ensuremath{\mathscr{C}}}
\newcommand{\D}{\ensuremath{\mathscr{D}}}
%% Objects of category
\newcommand{\obj}[1]{\ensuremath{\vert #1 \vert}}
%% Dual category
\newcommand{\dual}[1]{\ensuremath{#1^{op}}}
%%% Unicode substitutions
\def\circlearrowleft{↺}
%%%
%%%%

40
tex/sections/01_introduction.tex
View file

@ -1,11 +1,11 @@
\chapter{Introduction}
\chapter{Introduction}\label{chp:introduction}
This is a summary of the course ``Algebra des Programmierens'' taught by Prof.\ Dr.\ Stefan Milius in the winter term 2023/2024 at the FAU~\footnote{Friedrich-Alexander-Universität Erlangen-Nürnberg}.
The course is based on~\cite{poll1999algebra} with~\cite{adamek1990abstract} as a reference for category theory.
Goal of the course is to develop a mathematical theory for semantics of data types and their accompanying proof principles. The chosen environment is the field of category theory.
\section{Functions}
A function $f : X \rightarrow Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$).
A function $f : X \to Y$ is a mapping from the set $X$ (the domain of $f$) to the set $Y$ (the codomain of $f$).
More concretely $f$ is a relation $f \subseteq X \times Y$ which is
\begin{itemize}
\item \emph{left-total}, i.e.\ for all $x \in X$ exists some $y \in Y$ such that $(x,y) \in f$;
@ -14,24 +14,24 @@ More concretely $f$ is a relation $f \subseteq X \times Y$ which is
Often, one is also interested in the symmetrical properties, a function is called
\begin{itemize}
\item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \rightarrow x = x'$ holds;
\item \emph{injective} or \emph{left-unique} if for every $x,x' \in X$ the implication $f(x) = f(x') \to x = x'$ holds;
\item \emph{surjective} or \emph{right-total} if for every $y \in Y$ there exists an $x \in X$ such that $f(x) = y$;
\item \emph{bijective} if it is injective and surjective.
\end{itemize}
\begin{example}
\begin{enumerate}
\item The identity function $id_A : A \rightarrow A$, $id_A(x) = x$
\item The constant function $b! : A \rightarrow B$ for $b \in B$ defined by $b!(x) = b$
\item The inclusion function $i_A : A \rightarrow B$ for $A \subseteq B$ defined by $i_A(x) = x$
\item Constants $b : 1 \rightarrow B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$.
\item Composition of function $f : A \rightarrow B, g : B \rightarrow C$ called $g \circ f : A \rightarrow C$ defined by $(g \circ f)(x) = g(f(x))$.
\item The empty function $¡ : \emptyset \rightarrow B$
\item The singleton function $! : A \rightarrow 1$
\item The identity function $id_A : A \to A$, $id_A(x) = x$
\item The constant function $b! : A \to B$ for $b \in B$ defined by $b!(x) = b$
\item The inclusion function $i_A : A \to B$ for $A \subseteq B$ defined by $i_A(x) = x$
\item Constants $b : 1 \to B$, where $1 := {*}$. The function $b$ is in bijection with the set $B$.
\item Composition of function $f : A \to B, g : B \to C$ called $g \circ f : A \to C$ defined by $(g \circ f)(x) = g(f(x))$.
\item The empty function $¡ : \emptyset \to B$
\item The singleton function $! : A \to 1$
\end{enumerate}
\end{example}
\section{Data Types}
\section{Data Types}\label{sec:datatypes}
Programs work with data that should ideally be organized in a useful manner.
A useful representation for data in functional programming is by means of \emph{algebraic data types}.
@ -54,7 +54,7 @@ Such data types (parametric or non-parametric) usually come with a principle for
Equivalently, every function defined by recursion can be defined via a \emph{fold}-function which satisfies an identity and fusion law, which replace the induction principle. Let us now consider two examples of data types and illustrate this.
\subsection{Natural Numbers}
The type of natural numbers comes with a fold function $foldn : C \rightarrow (Nat \rightarrow C) \rightarrow Nat \rightarrow C$ for every $C$, defined by
The type of natural numbers comes with a fold function $foldn : C \to (Nat \to C) \to Nat \to C$ for every $C$, defined by
\begin{alignat*}{2}
& foldn\;c\;h\;zero & & = c \\
& foldn\;c\;h\;(suc\;n) & & = h\;(foldn\;c\;h\;n)
@ -63,11 +63,11 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
\begin{example} Let us now consider some functions defined in terms of $foldn$.
\begin{itemize}
\item $iszero : Nat \rightarrow Bool$ is defined by
\item $iszero : Nat \to Bool$ is defined by
\[iszero = foldn\;true\;false!\]
\item $plus : Nat \rightarrow Nat \rightarrow Nat$ is defined by
\item $plus : Nat \to Nat \to Nat$ is defined by
\[plus = foldn\;id\;(succ \circ eval) \]
where $eval : (A \rightarrow B) \rightarrow A \rightarrow B$ is defined by
where $eval : (A \to B) \to A \to B$ is defined by
\[eval\;f\;a = f\;a\]
\end{itemize}
@ -78,7 +78,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
\begin{enumerate}
\item \customlabel{law:natident}{\textbf{Identity}}: $foldn\;zero\;succ = id_{Nat}$
\item \customlabel{law:natfusion}{\textbf{Fusion}}: for all $c : C$, $h, h' : Nat
\rightarrow C$ and $k : C \rightarrow C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically:
\to C$ and $k : C \to C'$ with $kc = c'$ and $kh = h'k$ follows $k \circ foldn\;c\;h = foldn\;c'\;h'$, or diagrammatically:
% https://q.uiver.app/#q=WzAsNSxbMiwwLCJDIl0sWzQsMCwiQyJdLFsyLDIsIkMnIl0sWzQsMiwiQyciXSxbMCwwLCIxIl0sWzQsMCwiYyJdLFswLDIsImsiXSxbNCwyLCJjJyIsMl0sWzAsMSwiaCIsMl0sWzIsMywiaCciLDJdLFsxLDMsImsiLDFdXQ==
\[
\begin{tikzcd}[ampersand replacement=\&]
@ -139,7 +139,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
\begin{example}
The identity and fusion laws can in turn be used to prove the following induction principle:
For any predicate $p : Nat \rightarrow Bool$,
For any predicate $p : Nat \to Bool$,
\begin{enumerate}
\item $p\;zero = true$ and
\item $p \circ succ = p$
@ -182,7 +182,7 @@ The type of natural numbers comes with a fold function $foldn : C \rightarrow (N
trivially commutes.
\end{example}
\subsection{Lists}\label{subsec:lists}
We will now look at the $List$ type and examine it for similar properties. Let us start with the fold function $foldr : C \rightarrow (A \rightarrow C \rightarrow C) \rightarrow List\;A \rightarrow C$, which is defined by
We will now look at the $List$ type and examine it for similar properties. Let us start with the fold function $foldr : C \to (A \to C \to C) \to List\;A \to C$, which is defined by
\begin{alignat*}{2}
& foldr\;c\;h\;nil & & = c \\
& foldr\;c\;h\;(cons\;x\;xs) & & = h\;a\;(foldr\;c\;h\;xs)
@ -191,9 +191,9 @@ We will now look at the $List$ type and examine it for similar properties. Let u
\begin{example}
Again, let us define some functions using $foldr$.
\begin{itemize}
\item $length : List\;A \rightarrow Nat$ is defined by
\item $length : List\;A \to Nat$ is defined by
\[length = foldr\;zero\;(succ !)\]
\item For $f : A \rightarrow B$ we can define $List$-mapping function $List\;f : List\;A \rightarrow List\;B$ by
\item For $f : A \to B$ we can define $List$-mapping function $List\;f : List\;A \to List\;B$ by
\[List\;f = foldr\;nil\;(cons \circ f)\]
\end{itemize}
\end{example}

520
tex/sections/02_categories.tex
View file

@ -1,29 +1,30 @@
% chktex-file 1
\chapter{Category Theory}
Categories consist of objects and morphisms between those objects, that can be composed in a coherent way.
This yields a framework for abstraction of many mathematical concepts that enables us to reason on a very abstract level.
\begin{definition}[Category] A category \C consists of
\begin{definition}[Category] A category $\CC$ consists of
\begin{itemize}
\item a class of objects denoted $\obj{\C}$,
\item for every pair of objects $A,B \in \obj{\C}$ a set of morphisms $\C(A,B)$ called the hom-set,
\item a morphism $id_A : A \rightarrow A$ for every $A \in \obj{\C}$
\item a composition operator $(-) \circ (-) : \C(B,C) \rightarrow \C(A,B) \rightarrow \C(A,C)$ for every $A,B,C \in \obj{\C}$
\item a class of objects denoted $\obj{\CC}$,
\item for every pair of objects $A,B \in \obj{\CC}$ a set of morphisms $\CC(A,B)$ called the hom-set,
\item a morphism $id_A : A \to A$ for every $A \in \obj{\CC}$
\item a composition operator $(\argument) \comp (\argument) : \CC(B,C) \to \CC(A,B) \to \CC(A,C)$ for every $A,B,C \in \obj{\CC}$
\end{itemize}
additionally the composition must be associative and $f \circ id_A = f = id_B \circ f$ for any $f : A \rightarrow B$.
additionally the composition must be associative and $f \comp id_A = f = id_B \comp f$ for any $f : A \to B$.
\end{definition}
\begin{example} Some standard examples of categories and their objects and morphisms include:
\begin{center}
\begin{tabular}{l l l}
Category & Objects & Morphisms \\\midrule
\emph{Set} & Sets & Functions \\
\emph{Par} & Sets & Partial functions \\
\emph{Rel} & Sets & Binary relations \\
\emph{Gra} & Directed Graphs & Graph homomorphisms \\
\emph{Pos} & Partially ordered sets & Monotone mappings \\
\emph{Mon} & Monoids & Monoid homomorphisms \\
Monoid $(M, \cdot, e)$ & A single object $*$ & $x : * \rightarrow *$ for every $x \in M$ \\
Poset $(X, \leq)$ & Elements of $X$ & $x \leq y \iff \exists! f : x \rightarrow y$
Category & Objects & Morphisms \\\midrule
\Set & Sets & Functions \\
\Par & Sets & Partial functions \\
\Rel & Sets & Binary relations \\
\Gra & Directed Graphs & Graph homomorphisms \\
\Pos & Partially ordered sets & Monotone mappings \\
\Mon & Monoids & Monoid homomorphisms \\
Monoid $(M, \cdot, e)$ & A single object $*$ & $x : * \to *$ for every $x \in M$ \\
Poset $(X, \leq)$ & Elements of $X$ & $x \leq y \iff \exists! f : x \to y$
\end{tabular}
\end{center}
\end{example}
@ -35,17 +36,17 @@ In this chapter we will characterize (finite) products and coproducts, as well a
\begin{definition}[Initial and Terminal Objects] The following is the categorical abstraction of ``empty set'' and ``singleton set'' respectively.
\begin{enumerate}
\item An object $0 \in \obj{\C}$ is called initial if for every $B \in \obj{C}$ there is a unique morphism $¡ : 0 \rightarrow B$.
\item An object $1 \in \obj{\C}$ is called terminal if for every $A \in \obj{C}$ there is a unique morphism $! : A \rightarrow 1$.
\item An object $0 \in \obj{\BC}$ is called initial if for every $B \in \obj{C}$ there is a unique morphism $¡ : 0 \to B$.
\item An object $1 \in \obj{\CC}$ is called terminal if for every $A \in \obj{C}$ there is a unique morphism $! : A \to 1$.
\end{enumerate}
\end{definition}
\begin{example} Oftentimes the initial object is an empty structure and the terminal object a singleton structure, some examples are:
\begin{center}
\begin{tabular}{l l l}
Category & Initial Object & Terminal Object \\\midrule
\emph{Set} & $\emptyset$ & ${*}$ \\
\emph{Pos} & $\emptyset$ & ${*}$ \\
\emph{Gra} & Empty graph & Singleton graph \\
\Set & $\emptyset$ & ${*}$ \\
\Pos & $\emptyset$ & ${*}$ \\
\Gra & Empty graph & Singleton graph \\
Poset $(X, \leq)$ & $\bot \in X$ such that $\forall x \in X. \bot \leq x$ & $\top \in X$ such that $\forall x \in X. x \leq \top$
\end{tabular}
\end{center}
@ -56,18 +57,18 @@ In this chapter we will characterize (finite) products and coproducts, as well a
Now let us characterize special morphisms.
\begin{definition}[Special Morphisms]
Let $f : A \rightarrow B$ be a morphism. $f$ is called
Let $f : A \to B$ be a morphism. $f$ is called
\begin{itemize}
\item an \emph{isomorphism} (\emph{iso}), if there exists an inverse $f^{-1} : B \rightarrow A$ such that $f \circ g = id_B$ and $g \circ f = id_A$;
\item a \emph{monomorphism} (\emph{mono}), if for all $g, h : C \rightarrow A$ the implication $f \circ g = f \circ h \Rightarrow g = h$ holds;
\item an \emph{epimorphism} (\emph{epi}), if for all $g, h : B \rightarrow C$ the implication $g \circ f = h \circ f \Rightarrow g = h$ holds.
\item an \emph{isomorphism} (\emph{iso}), if there exists an inverse $f^{-1} : B \to A$ such that $f \comp g = id_B$ and $g \comp f = id_A$;
\item a \emph{monomorphism} (\emph{mono}), if for all $g, h : C \to A$ the implication $f \comp g = f \comp h \Rightarrow g = h$ holds;
\item an \emph{epimorphism} (\emph{epi}), if for all $g, h : B \to C$ the implication $g \comp f = h \comp f \Rightarrow g = h$ holds.
\end{itemize}
\end{definition}
\begin{example} Let us consider what these notions instantiate to in concrete categories.
\begin{center}
\begin{tabular}{l l l l}
Category & Monomorphisms & Epimorphisms & Isomorphisms \\\midrule
\emph{Set} & injective functions & surjective functions & bijective functions \\
\Set & injective functions & surjective functions & bijective functions \\
\emph{Pos, Gra} & injective morphisms & surjective morphisms & bijective morphisms \\
Poset $(X, \leq)$ & all & all & all \\
Monoid $(M, \cdot, e)$ & left cancellative $a \in M$ & right cancellative $a \in M$ & invertible $a \in M$
@ -80,19 +81,19 @@ Now let us characterize special morphisms.
\begin{proof}
Let $f$ be an isomorphism.
\begin{itemize}
\item $f \circ g = f \circ h$ implies $g = f^{-1} \circ f \circ g = f^{-1} \circ f \circ h = h$, thus $f$ is a monomorphism.
\item $g \circ f = h \circ f$ implies $g = g \circ f \circ f^{-1} = h \circ f \circ f^{-1} = h$, thus $f$ is an epimorphism.
\item $f \comp g = f \comp h$ implies $g = f^{-1} \comp f \comp g = f^{-1} \comp f \comp h = h$, thus $f$ is a monomorphism.
\item $g \comp f = h \comp f$ implies $g = g \comp f \comp f^{-1} = h \comp f \comp f^{-1} = h$, thus $f$ is an epimorphism.
\end{itemize}
\end{proof}
\begin{proposition}\label{prop:monosplitting} If $f \circ m$ is a monomorphism then $m$ is also a monomorphism.
\begin{proposition}\label{prop:monosplitting} If $f \comp m$ is a monomorphism then $m$ is also a monomorphism.
\end{proposition}
\begin{proof}
Let $m \circ g = m \circ h$. To show that $g = h$ it suffices to show that $f \circ m \circ g = f \circ m \circ h$, which indeed follows by assumption.
Let $m \comp g = m \comp h$. To show that $g = h$ it suffices to show that $f \comp m \comp g = f \comp m \comp h$, which indeed follows by assumption.
\end{proof}
\begin{proposition}\label{prop:episplitting} If $e \circ f$ is an epimorphism then $e$ is also an epimorphism.
\begin{proposition}\label{prop:episplitting} If $e \comp f$ is an epimorphism then $e$ is also an epimorphism.
\end{proposition}
\begin{proof}
Let $g \circ e = h \circ e$. To show that $g = h$ it suffices to show that $g \circ e \circ f = h \circ e \circ f$, which again follows by assumption.
Let $g \comp e = h \comp e$. To show that $g = h$ it suffices to show that $g \comp e \comp f = h \comp e \comp f$, which again follows by assumption.
\end{proof}
Categorical structures like initial objects are usually not uniquely identified, there might be multiple initial objects in a category. However, all initial objects in a category are isomorphic, we call this ``unique up to isomorphism''.
@ -100,7 +101,7 @@ Categorical structures like initial objects are usually not uniquely identified,
\begin{proposition}\label{prop:init_up_to} Initial objects are unique up to isomorphism.
\end{proposition}
\begin{proof}
Let $0, 0' \in \obj{\C}$ be two initial objects of $\C$ with the unique morphisms $¡_A : 0 \rightarrow A$ and ${¡'}_A : 0' \rightarrow A$.
Let $0, 0' \in \obj{\CC}$ be two initial objects of $\CC$ with the unique morphisms $¡_A : 0 \to A$ and ${¡'}_A : 0' \to A$.
The isomorphism is:
% https://q.uiver.app/#q=WzAsMixbMCwwLCIwIl0sWzIsMCwiMCciXSxbMSwwLCJ7wqEnfV8wIiwyLHsiY3VydmUiOi0yfV0sWzAsMSwiwqFfezAnfSIsMCx7ImN1cnZlIjotMn1dXQ==
\[
@ -110,12 +111,12 @@ Categorical structures like initial objects are usually not uniquely identified,
\arrow["{¡_{0'}}", curve={height=-12pt}, from=1-1, to=1-3]
\end{tikzcd}
\]
Note that by uniqueness $¡_{0'} \circ {¡'}_0 = {¡'}_{0'} = id_{0'}$ and ${¡'}_0 \circ ¡_{0'} = ¡_0 = id_0$.
Note that by uniqueness $¡_{0'} \comp {¡'}_0 = {¡'}_{0'} = id_{0'}$ and ${¡'}_0 \comp ¡_{0'} = ¡_0 = id_0$.
\end{proof}
\begin{proposition}\label{prop:term_up_to} Terminal objects are unique up to isomorphism.
\end{proposition}
\begin{proof}
Let $1, 1' \in \obj{\C}$ be two terminal objects of $\C$ with the unique morphisms $!_A : A \rightarrow 1$ and ${!'}_A : A \rightarrow 1'$.
Let $1, 1' \in \obj{\CC}$ be two terminal objects of $\CC$ with the unique morphisms $!_A : A \to 1$ and ${!'}_A : A \to 1'$.
The isomorphism is:
% https://q.uiver.app/#q=WzAsMixbMCwwLCIxIl0sWzIsMCwiMSciXSxbMCwxLCJ7ISd9XzEiLDAseyJjdXJ2ZSI6LTJ9XSxbMSwwLCIhX3sxJ30iLDAseyJjdXJ2ZSI6LTJ9XV0=
\[
@ -125,7 +126,7 @@ Categorical structures like initial objects are usually not uniquely identified,
\arrow["{!_{1'}}", curve={height=-12pt}, from=1-3, to=1-1]
\end{tikzcd}
\]
Note that by uniqueness ${!'}_1 \circ !_{1'} = {!'}_{1'} = id_{1'}$ and $!_{1'} \circ {!'}_1 = !_1 = id_1$.
Note that by uniqueness ${!'}_1 \comp !_{1'} = {!'}_{1'} = id_{1'}$ and $!_{1'} \comp {!'}_1 = !_1 = id_1$.
\end{proof}
\section{Duality}
@ -134,17 +135,17 @@ It seems that we should somehow be able to construct one proof from the other, s
This is actually the case, we can for example say that \autoref{prop:episplitting} follows from \autoref{prop:monosplitting} by \emph{duality}.
\begin{definition}[Dual Category]
Every category $\C$ has a \emph{dual category} $\dual{\C}$ defined by
Every category $\CC$ has a \emph{dual category} $\dual{\CC}$ defined by
\begin{itemize}
\item $\obj{\dual{\C}} = \obj{\C}$
\item $\dual{\C}(A,B) = \C(B,A)$
\item $\obj{\dual{\CC}} = \obj{\CC}$
\item $\dual{\CC}(A,B) = \CC(B,A)$
\end{itemize}
\end{definition}
\begin{example} Examples are:
\begin{enumerate}
\item In a poset the order relation gets reversed.
\item \emph{\dual{Rel}} is isomorphic to \emph{Rel}, since subsets of $A \times B$ are in bijection with subsets of $B \times A$
\item $\dual{(\dual{\C})} = \C$
\item \emph{\dual{Rel}} is isomorphic to $\Rel$, since subsets of $A \times B$ are in bijection with subsets of $B \times A$
\item $\dual{(\dual{\CC})} = \CC$
\end{enumerate}
\end{example}
@ -163,7 +164,7 @@ This yields a proof principle ``by duality'', where every theorem yields another
\section{Products and Coproducts}
The categorical abstraction of Cartesian products is:
\begin{definition}[Product]
The \emph{product} of two objects $A, B \in \obj{\C}$ is an object that we call $A \times B$ together with morphisms $\pi_1 : A \times B \rightarrow A$ and $\pi_2 : A \times B \rightarrow B$ (the projections), where the following property holds:
The \emph{product} of two objects $A, B \in \obj{\CC}$ is an object that we call $A \times B$ together with morphisms $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$ (the projections), where the following property holds:
% https://q.uiver.app/#q=WzAsNCxbMiwyLCJBIFxcdGltZXMgQiJdLFs0LDIsIkIiXSxbMCwyLCJBIl0sWzIsMCwiQyJdLFswLDIsIlxccGlfMSJdLFswLDEsIlxccGlfMiIsMl0sWzMsMiwiZiIsMl0sWzMsMSwiZyJdLFszLDAsIlxcZXhpc3RzIVxcbGFuZ2xlIGYsIGcgXFxyYW5nbGUiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
\[
\begin{tikzcd}
@ -180,15 +181,15 @@ The categorical abstraction of Cartesian products is:
\end{definition}
\begin{example} Some examples include:
\begin{enumerate}
\item \emph{Set}: The product of two sets $A$ and $B$ is the Cartesian product $A \times B = \{ (a,b)\;\vert\;a \in A, b \in B\}$.
\item \emph{Gra}: The product of two graphs has as vertices the Cartesian product of the vertices of both graphs and an edge $(v_1, u_1) \rightarrow (v_2, u_2)$ iff there exists edges $v_1 \rightarrow v_2$ and $u_1 \rightarrow u_2$.
\item \emph{Pos}: Given two posets $(A, \leq), (B, \leq)$, the product is the Cartesian product of $A$ and $B$ where $(a,b) \leq (a', b') \iff a \leq a' \land b \leq b'$.
\item $\Set$: The product of two sets $A$ and $B$ is the Cartesian product $A \times B = \{ (a,b)\;\vert\;a \in A, b \in B\}$.
\item $\Gra$: The product of two graphs has as vertices the Cartesian product of the vertices of both graphs and an edge $(v_1, u_1) \to (v_2, u_2)$ iff there exists edges $v_1 \to v_2$ and $u_1 \to u_2$.
\item $\Pos$: Given two posets $(A, \leq), (B, \leq)$, the product is the Cartesian product of $A$ and $B$ where $(a,b) \leq (a', b') \iff a \leq a' \land b \leq b'$.
\item Let $(X, \leq)$ be a poset, the product of $a, b \in X$ is the greatest lower bound of $a$ and $b$.
\end{enumerate}
\end{example}
Dual to products are:
\begin{definition}[Coproduct]
The \emph{coproduct} of two objects $A, B \in \obj{\C}$ is an object that we call $A + B$ together with morphisms $i_1 : A \rightarrow A + B$ and $i_2 : B \rightarrow A + B$ (the injections), where the following property holds:
The \emph{coproduct} of two objects $A, B \in \obj{\CC}$ is an object that we call $A + B$ together with morphisms $i_1 : A \to A + B$ and $i_2 : B \to A + B$ (the injections), where the following property holds:
% https://q.uiver.app/#q=WzAsNCxbMiwwLCJBK0IiXSxbMCwwLCJBIl0sWzQsMCwiQiJdLFsyLDIsIkMiXSxbMSwwLCJpXzEiXSxbMiwwLCJpXzIiLDJdLFsxLDMsImYiLDJdLFsyLDMsImciXSxbMCwzLCJcXGV4aXN0cyFbZixnXSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==
\[
\begin{tikzcd}
@ -205,11 +206,11 @@ Dual to products are:
\end{definition}
\begin{example} Examples include:
\begin{enumerate}
\item \emph{Set}: The coproduct of two sets $A$ and $B$ is the disjoint union $A + B = \{ (a,0)\;\vert\;a \in A \} \cup \{ (b, 1) \vert b \in B \}$.
\item \emph{Pos}: The coproduct of ordered sets $(A, \leq)$ and $(B, \leq)$ is the disjoint union $A+B$ where $z \leq z'$ iff $z, z' \in A$ and $z \leq z'$ or $z, z' \in B$ and $z \leq z'$.
\item \emph{Gra}: Analogous to \emph{Pos}.
\item $\Set$: The coproduct of two sets $A$ and $B$ is the disjoint union $A + B = \{ (a,0)\;\vert\;a \in A \} \cup \{ (b, 1) \vert b \in B \}$.
\item $\Pos$: The coproduct of ordered sets $(A, \leq)$ and $(B, \leq)$ is the disjoint union $A+B$ where $z \leq z'$ iff $z, z' \in A$ and $z \leq z'$ or $z, z' \in B$ and $z \leq z'$.
\item $\Gra$: Analogous to $\Pos$.
\item Let $(X, \leq)$ be a poset, the coproduct of $a,b \in X$ is the least upper bound of $a$ and $b$.
\item \emph{Rel}: Analogous to \emph{Set} the coproduct is the disjoint union. Since $\emph{Rel} \cong \dual{\emph{Rel}}$ we know that the product is also the disjoint union.
\item $\Rel$: Analogous to $\Set$ the coproduct is the disjoint union. Since $\Rel \iso \dual{\Rel}$ we know that the product is also the disjoint union.
\end{enumerate}
\end{example}
@ -219,7 +220,7 @@ Dual to products are:
\begin{proof}
The usual proof is somewhat analogous to the proof of \autoref{prop:term_up_to}. Instead, we will prove it like this:
Consider the category $\emph{span}_{\C}(A,B)$ where objects are triples $A \overset{f}{\leftarrow} C \overset{g}{\rightarrow} B$ and morphisms $(C, f, g) \rightarrow (C', f', g')$ are morphisms $k : C \rightarrow C'$ in $\C$ such that
Consider the category $\emph{span}_{\CC}(A,B)$ where objects are triples $A \overset{f}{\leftarrow} C \overset{g}{\to} B$ and morphisms $(C, f, g) \to (C', f', g')$ are morphisms $k : C \to C'$ in $\CC$ such that
% https://q.uiver.app/#q=WzAsNCxbMiwwLCJDIl0sWzAsMiwiQSJdLFs0LDIsIkIiXSxbMiw0LCJDJyJdLFswLDEsImYiLDJdLFswLDIsImciXSxbMywxLCJmJyJdLFszLDIsImcnIiwyXSxbMCwzLCJrIl1d
\[
\begin{tikzcd}
@ -235,7 +236,7 @@ Dual to products are:
\arrow["k", from=1-3, to=5-3]
\end{tikzcd}
\]
commutes. Products of $A$ and $B$ are the final objects in $\emph{span}_{\C}(A,B)$ and are thus unique up to isomorphism.
commutes. Products of $A$ and $B$ are the final objects in $\emph{span}_{\CC}(A,B)$ and are thus unique up to isomorphism.
\end{proof}
By duality, we get:
\begin{proposition}
@ -245,41 +246,41 @@ By duality, we get:
We can now characterize products (and later dually coproducts) as a commutative monoid:
\begin{proposition}
$1$ is a unit of $\times$, i.e.\ $A \cong A \times 1$ for any $A \in \obj{\C}$.
$1$ is a unit of $\times$, i.e.\ $A \iso A \times 1$ for any $A \in \obj{\CC}$.
\end{proposition}
\begin{proof}
Take $\langle id_A , !_A \rangle : A \rightarrow A \times 1$ and $\pi_1 : A \times 1 \rightarrow A$, this indeed constitutes an isomorphism, since
\[\pi_1 \circ \langle id_A , !_A \rangle = id_A \]
Take $\langle id_A , !_A \rangle : A \to A \times 1$ and $\pi_1 : A \times 1 \to A$, this indeed constitutes an isomorphism, since
\[\pi_1 \comp \langle id_A , !_A \rangle = id_A \]
by definition and
\[\langle id_A , !_A \rangle \circ \pi_1 = \langle \pi_1 , !_A \rangle = \langle \pi_1 , \pi_2 \rangle = id_{A \times 1},\]
because $\pi_2 = !_A : A \times 1 \rightarrow 1$ by uniqueness of $!_A$.
\[\langle id_A , !_A \rangle \comp \pi_1 = \langle \pi_1 , !_A \rangle = \langle \pi_1 , \pi_2 \rangle = id_{A \times 1},\]
because $\pi_2 = !_A : A \times 1 \to 1$ by uniqueness of $!_A$.
\end{proof}
\begin{proposition}
$\times$ is associative, i.e.\ $A \times (B \times C) \cong (A \times B) \times C$ for any $A,B,C \in \obj{\C}$.
$\times$ is associative, i.e.\ $A \times (B \times C) \iso (A \times B) \times C$ for any $A,B,C \in \obj{\CC}$.
\end{proposition}
\begin{proof}
Take \[\alpha = \langle \langle \pi_1 , \pi_1 \circ \pi_2 \rangle , \pi_2 \circ \pi_2 \rangle : A \times (B \times C) \rightarrow (A \times B) \times C\]
and \[\alpha^{-1} = \langle \pi_1 \circ \pi_1 , \langle \pi_2 \circ \pi_1 , \pi_2 \rangle \rangle : (A \times B) \times C \rightarrow A \times (B \times C).\]
Take \[\alpha = \langle \langle \pi_1 , \pi_1 \comp \pi_2 \rangle , \pi_2 \comp \pi_2 \rangle : A \times (B \times C) \to (A \times B) \times C\]
and \[\alpha^{-1} = \langle \pi_1 \comp \pi_1 , \langle \pi_2 \comp \pi_1 , \pi_2 \rangle \rangle : (A \times B) \times C \to A \times (B \times C).\]
The rest of the proof then amounts to simply rewriting.
\end{proof}
\begin{proposition}
$\times$ is commutative, i.e.\ $A \times B \cong B \times A$ for any $A, B \in \obj{\C}$.
$\times$ is commutative, i.e.\ $A \times B \iso B \times A$ for any $A, B \in \obj{\CC}$.
\end{proposition}
\begin{proof}
Take \[\langle \pi_2 , \pi_1 \rangle : A \times B \rightarrow B \times A\]
and \[\langle \pi_2 , \pi_1 \rangle : B \times A \rightarrow A \times B.\]
Indeed, $\langle \pi_2 , \pi_1 \rangle \circ \langle \pi_2 , \pi_1 \rangle = \langle \pi_2 \circ \langle \pi_2 , \pi_1 \rangle , \pi_1 \circ \langle \pi_2 , \pi_1 \rangle \rangle = \langle \pi_1 , \pi_2 \rangle = id$.
Take \[\langle \pi_2 , \pi_1 \rangle : A \times B \to B \times A\]
and \[\langle \pi_2 , \pi_1 \rangle : B \times A \to A \times B.\]
Indeed, $\langle \pi_2 , \pi_1 \rangle \comp \langle \pi_2 , \pi_1 \rangle = \langle \pi_2 \comp \langle \pi_2 , \pi_1 \rangle , \pi_1 \comp \langle \pi_2 , \pi_1 \rangle \rangle = \langle \pi_1 , \pi_2 \rangle = id$.
\end{proof}
Duality instantly yields the commutative monoid structure of coproducts:
\begin{proposition}
$0$ is the unit of $+$, i.e.\ $A \cong A + 0$ for any $A \in \obj{\C}$.
$0$ is the unit of $+$, i.e.\ $A \iso A + 0$ for any $A \in \obj{\CC}$.
\end{proposition}
\begin{proposition}
$+$ is associative, i.e.\ $A + (B + C) \cong (A + B) + C$ for any $A,B,C \in \obj{\C}$.
$+$ is associative, i.e.\ $A + (B + C) \iso (A + B) + C$ for any $A,B,C \in \obj{\CC}$.
\end{proposition}
\begin{proposition}
$+$ is commutative, i.e.\ $A + B \cong B + A$ for any $A, B \in \obj{\C}$.
$+$ is commutative, i.e.\ $A + B \iso B + A$ for any $A, B \in \obj{\CC}$.
\end{proposition}
\begin{remark}
@ -289,36 +290,36 @@ Duality instantly yields the commutative monoid structure of coproducts:
\section{Functors}
Functors are morphisms between categories, concretely:
\begin{definition}[Functor]
A functor $F : \C \rightarrow \D$ consists of
A functor $F : \CC \to \CD$ consists of
\begin{itemize}
\item a mapping $F : \obj{\C} \rightarrow \obj{\D}$ on objects and
\item a mapping $F : \C(A,B) \rightarrow \C(FA,FB)$ on morphisms,
\item a mapping $F : \obj{\CC} \to \obj{\CD}$ on objects and
\item a mapping $F : \CC(A,B) \to \CC(FA,FB)$ on morphisms,
\end{itemize}
such that $F(id_A) = id_{FA}$ and $F(g \circ f) = Fg \circ Ff$.
such that $F(id_A) = id_{FA}$ and $F(g \comp f) = Fg \comp Ff$.
\end{definition}
\begin{example} Usual examples of functors include
\begin{enumerate}
\item Constant functors mapping to a single object: $D! : \C \rightarrow \D, D \in \obj{\D}$ with
\item Constant functors mapping to a single object: $D! : \CC \to \CD, D \in \obj{\CD}$ with
\[D!(C) = D, \qquad D!(f) = id_D.\]
\item Identity functor: $Id_\C : \C \rightarrow \C$ with
\[Id_\C(C) = C, \qquad Id_\C(f) = f.\]
\item Identity functor: $\Id{}_{\CC} : \CC \to \CC$ with
\[\Id{}_{\CC} (C) = C, \qquad \Id{}_{\CC} (f) = f.\]
\item Composition of functors: $(FG)(X) = F(GX), (FG)(f) = F(Gf)$
\item Square functor on $\emph{Set}$: $Q : \emph{Set} \rightarrow \emph{Set}$ with
\item Square functor on $\Set$: $Q : \Set \to \Set$ with
\[QX = X \times X, \qquad Qf = f \times f.\]
\item $list : Set \rightarrow Set$, see \autoref{subsec:lists}.
\item For $A \in \obj{\C}$ there is the hom-functor $\C(A,-) : \C \rightarrow Set$ given by
\[ \C(A,B), \qquad \C(A,f : B \rightarrow B')(h : A \rightarrow B) = f \circ h : \C(A,B').\]
\item Functors between posets are monotonous maps, which in turn are the morphisms in $\emph{Pos}$.
\item Functors between monoids are monoid homomorphisms, which in turn are the morphisms in $\emph{Mon}$.
\item The power set functor $\mathscr{P} : \emph{Set} \rightarrow \emph{Set}$ defined by
\item $list : Set \to Set$, see \autoref{subsec:lists}.
\item For $A \in \obj{\CC}$ there is the hom-functor $\CC(A,\argument) : \CC \to Set$ given by
\[ \CC(A,B), \qquad \CC(A,f : B \to B')(h : A \to B) = f \comp h : \CC(A,B').\]
\item Functors between posets are monotonous maps, which in turn are the morphisms in $\Pos$.
\item Functors between monoids are monoid homomorphisms, which in turn are the morphisms in $\Mon$.
\item The power set functor $\PSet{} : \Set \to \Set$ defined by
\begin{alignat*}{2}
& \mathscr{P}X & & = \{ Y\;\vert\; Y \subseteq X \} \\
& (\mathscr{P}f)Y & & = f[Y] \subseteq X', \text{ for } Y \subseteq X.
& \PSet{}X & & = \{ Y\;\vert\; Y \subseteq X \} \\
& (\PSet{}f)Y & & = f[Y] \subseteq X', \text{ for } Y \subseteq X.
\end{alignat*}
\item If $\C$ is a category that adds some structure to sets (like \emph{Mon} or \emph{Pos}) one usually can construct a \emph{forgetful functor} $U : \C \rightarrow \emph{Set}$, e.g.
\item If $\CC$ is a category that adds some structure to sets (like $\Mon$ or $\Pos$) one usually can construct a \emph{forgetful functor} $U : \CC \to \Set$, e.g.
\begin{alignat*}{4}
& U_{\emph{Pos}} : \emph{Pos} & & \rightarrow \emph{Set}; \qquad & & (X, \leq) & & \mapsto X \\
& U_{\emph{Mon}} : \emph{Mon} & & \rightarrow \emph{Set}; \qquad & & (M, \cdot, e) & & \mapsto M
& U_{\Pos} : \Pos & & \to \Set; \qquad & & (X, \leq) & & \mapsto X \\
& U_{\Mon} : \Mon & & \to \Set; \qquad & & (M, \cdot, e) & & \mapsto M
\end{alignat*}
\setcounter{resumeenum}{\value{enumi}}
\end{enumerate}
@ -328,34 +329,34 @@ Using functors as morphisms, one can \emph{almost} build a category $\emph{CAT}$
We can however consider structures like products and isomorphisms in the quasi-category $\emph{CAT}$:
\begin{definition}[Products of Categories]
The product of two categories $\C, \D$ consists of
The product of two categories $\CC, \CD$ consists of
\begin{itemize}
\item $\obj{\C \times \D} = \obj{\C} \times \obj{\D}$,
\item $(\C \times \D)((A_1, A_2),(B_1,B_2)) = \C(A_1, B_1) \times D(A_2, B_2)$,
\item $\obj{\CC \times \CD} = \obj{\CC} \times \obj{\CD}$,
\item $(\CC \times \CD)((A_1, A_2),(B_1,B_2)) = \CC(A_1, B_1) \times D(A_2, B_2)$,
\end{itemize}
with projection functors $\pi_1 : \C \times \D \rightarrow \C, \pi_2 : \C \times \D \rightarrow \D$.
with projection functors $\pi_1 : \CC \times \CD \to \CC, \pi_2 : \CC \times \CD \to \CD$.
\end{definition}
\begin{example} More examples of functors include:
\begin{enumerate} \setcounter{enumi}{\value{resumeenum}}
\item The Cartesian product functor: $-\times- : \emph{Set} \times \emph{Set} \rightarrow \emph{Set}$.
\item The binary hom-functor $\C(-,-) : \dual{\C} \times \C \rightarrow \emph{Set}$ with
\[\C(A,B), \qquad \C(g : X' \rightarrow X, f : Y \rightarrow Y')(h : X \rightarrow Y) = f \circ h \circ g : \C(X',Y').\]
\item The Cartesian product functor: $-\times- : \Set \times \Set \to \Set$.
\item The binary hom-functor $\CC(\argument,\argument) : \dual{\CC} \times \CC \to \Set$ with
\[\CC(A,B), \qquad \CC(g : X' \to X, f : Y \to Y')(h : X \to Y) = f \comp h \comp g : \CC(X',Y').\]
\setcounter{resumeenum}{\value{enumi}}
\end{enumerate}
\end{example}
\begin{definition}[Covariant and Contravariant Functors]
A functor $F : \dual{\C} \rightarrow \D$ is called a \emph{contravariant} functor $\C \rightarrow \D$. For differentiation, we call `normal' functors $\C \rightarrow \D$ \emph{covariant}.
A functor $F : \dual{\CC} \to \CD$ is called a \emph{contravariant} functor $\CC \to \CD$. For differentiation, we call `normal' functors $\CC \to \CD$ \emph{covariant}.
\end{definition}
\begin{example} Examples of contravariant functors include:
\begin{enumerate} \setcounter{enumi}{\value{resumeenum}}
\item For every $Y \in \obj{\C}$ there is a contravariant hom-functor $\C(-,Y) : \dual{\C} \rightarrow \emph{Set}$ given by
\[\C(X,Y), \qquad \C(f : X' \rightarrow X, Y)(h : X \rightarrow Y) = h \circ f : \C(X', Y).\]
\item $2^{(-)} : \dual{\emph{Set}} \rightarrow \emph{Set}$ where
\[2^X = \{ f : X \rightarrow 2 \} \cong \mathscr{P}X\]
\item For every $Y \in \obj{\CC}$ there is a contravariant hom-functor $\CC(\argument,Y) : \dual{\CC} \to \Set$ given by
\[\CC(X,Y), \qquad \CC(f : X' \to X, Y)(h : X \to Y) = h \comp f : \CC(X', Y).\]
\item $2^{(\argument)} : \dual{\Set} \to \Set$ where
\[2^X = \{ f : X \to 2 \} \iso \PSet{}X\]
and
\[2^{(f : X \rightarrow Y)} : 2^Y \rightarrow 2^X \cong \mathscr{P}Y \rightarrow \mathscr{P}X, \qquad Z \mapsto \{ x \;\vert\; fx \in Z \} = f^{-1}[Z] \subseteq X.\]
\item For every functor $F : \C \rightarrow \D$ the identical functor $\dual{F} : \dual{\C} \rightarrow \dual{\D}$, given by
\[2^{(f : X \to Y)} : 2^Y \to 2^X \iso \PSet{}Y \to \PSet{}X, \qquad Z \mapsto \{ x \;\vert\; fx \in Z \} = f^{-1}[Z] \subseteq X.\]
\item For every functor $F : \CC \to \CD$ the identical functor $\dual{F} : \dual{\CC} \to \dual{\CD}$, given by
\[\dual{F}C = FC, \qquad \dual{F}f = Ff.\]
\end{enumerate}
\end{example}
@ -363,26 +364,26 @@ We can however consider structures like products and isomorphisms in the quasi-c
Isomorphisms of categories are the isomorphisms in the quasi-category $\emph{CAT}$, thus a functor is an isomorphism iff he is bijective on both objects and morphisms. However, oftentimes categories are not isomorphic but instead \emph{equivalent} in the following sense:
\begin{definition}[Equivalence Functors]
A functor $F : \C \rightarrow \D$ is called
A functor $F : \CC \to \CD$ is called
\begin{itemize}
\item \emph{full} if every $F : \C(A,B) \rightarrow \D(FA,FB)$ is surjective,
\item \emph{faithful} if every $F : \C(A,B) \rightarrow \D(FA,FB)$ is injective,
\item \emph{essentially surjective (dense)} if for every $D \in \D$ there exists a $C \in \C$ such that $D \cong FC$,
\item \emph{full} if every $F : \CC(A,B) \to \CD(FA,FB)$ is surjective,
\item \emph{faithful} if every $F : \CC(A,B) \to \CD(FA,FB)$ is injective,
\item \emph{essentially surjective (dense)} if for every $D \in \CD$ there exists a $C \in \CC$ such that $D \iso FC$,
\item an \emph{equivalence} if $F$ is full, faithful and dense.
\end{itemize}
\end{definition}
\begin{example} Let us consider two examples of equivalent categories:
\begin{enumerate}
\item The category $\emph{Par}$ is equivalent to $\emph{Set}_p$, which is the category of pointed sets, where objects are tuples $(X,p), p \in X$ and morphisms are point-preserving.
\item The product category $\emph{Set} \times \emph{Set}$ is equivalent to the \emph{slice category} $\emph{Set}/2$, where objects are maps $X \rightarrow 2$ and morphisms $h : (X \overset{f}{\rightarrow} 2) \rightarrow (Y \overset{g}{\rightarrow} 2)$ are maps $h : X \rightarrow Y$ such that $g \circ h = f$.
\item The category $\Par$ is equivalent to $\Set_p$, which is the category of pointed sets, where objects are tuples $(X,p), p \in X$ and morphisms are point-preserving.
\item The product category $\Set \times \Set$ is equivalent to the \emph{slice category} $\Set/2$, where objects are maps $X \to 2$ and morphisms $h : (X \overset{f}{\to} 2) \to (Y \overset{g}{\to} 2)$ are maps $h : X \to Y$ such that $g \comp h = f$.
\end{enumerate}
\end{example}
\section{Natural Transformations}
Natural transformation are morphisms between functors. The definition of ``naturality'' was one of the original goals of category theory.
\begin{definition}[Natural Transformation]
Given two functors $F, G : \C \rightarrow \D$.
A natural transformation $\alpha : F \rightarrow G$ between these functors is a family of morphisms $(\alpha_C : FC \rightarrow GC)_{C\in\obj{\C}}$, such that for any $f : A \rightarrow B$ the diagram
Given two functors $F, G : \CC \to \CD$.
A natural transformation $\alpha : F \to G$ between these functors is a family of morphisms \[{(\alpha_C : FC \to GC)}_{C\in\obj{\CC}},\] such that for any $f : A \to B$ the diagram
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFsyLDAsIkZCIl0sWzAsMiwiR0EiXSxbMiwyLCJHQiJdLFswLDEsIkZmIl0sWzIsMywiR2YiXSxbMCwyLCJcXGFscGhhX0EiLDJdLFsxLDMsIlxcYWxwaGFfQiJdXQ==
\[
\begin{tikzcd}
@ -400,7 +401,7 @@ Natural transformation are morphisms between functors. The definition of ``natur
\begin{example} Examples of natural transformations include:
\begin{enumerate}
\item The obvious function $flatten : Tree\;A \rightarrow List\;A$:
\item The obvious function $flatten : Tree\;A \to List\;A$:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJUcmVlXFw7QSJdLFsyLDAsIlRyZWVcXDtCIl0sWzAsMiwiTGlzdFxcO0EiXSxbMiwyLCJMaXN0XFw7QiJdLFswLDIsImZsYXR0ZW5fQSIsMl0sWzEsMywiZmxhdHRlbl9CIl0sWzIsMywibGlzdFxcO2YiXSxbMCwxLCJ0cmVlXFw7ZiJdXQ==
\[
\begin{tikzcd}
@ -413,18 +414,18 @@ Natural transformation are morphisms between functors. The definition of ``natur
\arrow["{tree\;f}", from=1-1, to=1-3]
\end{tikzcd}
\]
\item For $Id, Q : Set \rightarrow Set$ we have $\delta : Id \rightarrow Q$ given by $\delta_X (x) = (x,x)$.
\item On $\mathcal{P}$ we can define natural transformations $\eta : Id \rightarrow \mathcal{P}$ and $\mu : \mathcal{P}\mathcal{P} \rightarrow \mathcal{P}$ by:
\item For $\Id{}, Q : Set \to Set$ we have $\delta : \Id{} \to Q$ given by $\delta_X (x) = (x,x)$.
\item On $\mathcal{P}$ we can define natural transformations $\eta : \Id{} \to \mathcal{P}$ and $\mu : \mathcal{P}\mathcal{P} \to \mathcal{P}$ by:
\begin{alignat*}{1}
\eta_X : X & \rightarrow \mathcal{P}X \\
\eta_X : X & \to \mathcal{P}X \\
x & \mapsto \{x\}
\end{alignat*}
and
\begin{alignat*}{1}
\mu_X : \mathcal{P}\mathcal{P}X & \rightarrow \mathcal{P}X \\
\mu_X : \mathcal{P}\mathcal{P}X & \to \mathcal{P}X \\
Z & \mapsto \bigcup Z.
\end{alignat*}
\item Between $Q$ and $\mathcal{P}$ we can consider $\alpha,\beta : Q \rightarrow \mathcal{P}$ given by
\item Between $Q$ and $\mathcal{P}$ we can consider $\alpha,\beta : Q \to \mathcal{P}$ given by
\begin{alignat*}{2}
& \alpha_X(x,y) & & = \{x,y\} \\
& \beta_X(x,y) & & = \{x\}.
@ -432,12 +433,12 @@ Natural transformation are morphisms between functors. The definition of ``natur
\end{enumerate}
\end{example}
Functors $\C \rightarrow \D$ together with natural transformations as morphisms form a quasi-category $[\C,\D]$, that is called the functor category. If $\C$ is small, then $[\C,\D]$ is a category, where identity and composition are defined component wise.
Functors $\CC \to \CD$ together with natural transformations as morphisms form a quasi-category $[\CC,\CD]$, that is called the functor category. If $\CC$ is small, then $[\CC,\CD]$ is a category, where identity and composition are defined component wise.
\begin{example} Let us examine concrete examples of functor categories:
\begin{enumerate}
\item $[2, \C] \cong \C \times \C$, where $2$ is the \emph{discrete} category with two objects, i.e.\ $2$ has no morphisms besides the identities.
\item Let $\rightarrow$ be the category with 2 objects and a single non-trivial morphism $m$. $[\rightarrow, \C$ is the \emph{category of morphisms} of $\C$, where morphisms $Fm \rightarrow Gm$ are pairs of morphisms $(f,g)$ where
\item $[2, \CC] \iso \CC \times \CC$, where $2$ is the \emph{discrete} category with two objects, i.e.\ $2$ has no morphisms besides the identities.
\item Let $\to$ be the category with 2 objects and a single non-trivial morphism $m$. $[\to, \CC]$ is the \emph{category of morphisms} of $\CC$, where morphisms $Fm \to Gm$ are pairs of morphisms $(f,g)$ where
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGMCJdLFsyLDAsIkYxIl0sWzAsMiwiRzAiXSxbMiwyLCJHMSJdLFswLDEsIkZtIl0sWzIsMywiR20iXSxbMCwyLCJmIiwyXSxbMSwzLCJnIl1d
\[
\begin{tikzcd}
@ -455,46 +456,305 @@ Functors $\C \rightarrow \D$ together with natural transformations as morphisms
\end{example}
\begin{definition}[Natural Isomorphism]
Isomorphisms in $[\C,\D]$ are called \emph{natural isomorphisms}.
Isomorphisms in $[\CC,\CD]$ are called \emph{natural isomorphisms}.
\end{definition}
\begin{proposition}
$\alpha : F \rightarrow G$ is a natural isomorphism \emph{iff} every $\alpha_C$ is an isomorphism.
$\alpha : F \to G$ is a natural isomorphism \emph{iff} every $\alpha_C$ is an isomorphism.
\end{proposition}
\begin{example} Let us consider some examples of natural isomorphisms:
\begin{enumerate}
\item In $[\emph{Set},\emph{Set}]$ is $Id \cong \emph{Set}(1,-)$, since of course $Id\;X = X \cong X^1 = \emph{Set}(1,X)$.
\item Also in $[\emph{Set},\emph{Set}]$ is $Q \cong \emph{Set}(2,-)$, similarly is $\lambda X.2\times X \cong \lambda X. X + X$.
\item The forgetful functor $U : \emph{Pos} \rightarrow \emph{Set}$ is naturally isomorphic to $\emph{Pos}(1,-)$, because the constant mapping $x : 1 \rightarrow X$ is monotonous for every element $x$ of a poset.
\item In $[\Set,\Set]$ is $\Id{} \iso \Set(1,\argument)$, since of course $\Id{}\;X = X \iso X^1 = \Set(1,X)$.
\item Also in $[\Set,\Set]$ is $Q \iso \Set(2,\argument)$, similarly is $\lambda X.2\times X \iso \lambda X. X + X$.
\item The forgetful functor $U : \Pos \to \Set$ is naturally isomorphic to $\Pos(1,\argument)$, because the constant mapping $x : 1 \to X$ is monotonous for every element $x$ of a poset.
\end{enumerate}
\end{example}
\begin{proposition}[Yoneda Lemma]
Let $A \in \obj{\C}$ and $G : \C \rightarrow \emph{Set}$. Then the natural transformations
\[\C(A,-) \rightarrow G\]
Let $A \in \obj{\CC}$ and $G : \CC \to \Set$. Then the natural transformations
\[\CC(A,\argument) \to G\]
are in bijection with the elements of the set $GA$.
In other words
\[[\CC , \Set ](\CC(A,\argument), G) \iso GA \]
\end{proposition}
\begin{proof}
The mappings are
\begin{alignat*}{1}
& Z : GA \rightarrow [\C , \emph{Set}](\C(A,-), G) \\
& Z : GA \to [\CC , \Set](\CC(A,\argument), G) \\
& Z\;x\;h = G\;h\;x
\end{alignat*}
and
\begin{alignat*}{1}
& Y : [\C , \emph{Set}](\C(A,-), G) \rightarrow GA \\
& Y\;\alpha = \alpha_A\;id_A
& Y : [\CC , \Set](\CC(A,\argument), G) \to GA \\
& Y\;\alpha = \alpha_A\;id_A.
\end{alignat*}
We are left to check naturality of $Z\;x$ and that indeed $Z$ and $Y$ are inverse to each other, all of which follows by routine rewriting.
\end{proof}
\begin{example}
Let us consider an application of the Yoneda Lemma: how many natural transformations $Id \rightarrow Q$ are there?
Recall that $Id \cong \emph{Set}(1,-)$, and by Yoneda there is exactly $\vert Q1 \vert = 1$ natural transformation $\emph{Set}(1,-) \rightarrow Q$, thus the number of natural transformations $Id \rightarrow Q$ is $1$.
Let us consider an application of the Yoneda Lemma: how many natural transformations $\Id{} \to Q$ are there?
Recall that $\Id{} \iso \Set(1,\argument)$, and by Yoneda there is exactly $\vert Q1 \vert = 1$ natural transformation $\Set(1,\argument) \to Q$, thus the number of natural transformations $\Id{} \to Q$ is $1$.
Furthermore, consider the number of natural transformations $Q \rightarrow Q$. Recall that $Q \cong \emph{Set}(2, -)$, and by Yoneda there are $\vert Q2 \vert = 4$ natural transformations $\emph{Set}(2, -) \rightarrow Q$, thus the number of natural transformations $Q \rightarrow Q$ is $4$.
Furthermore, consider the number of natural transformations $Q \to Q$. Recall that $Q \iso \Set(2, \argument)$, and by Yoneda there are $\vert Q2 \vert = 4$ natural transformations $\Set(2, \argument) \to Q$, thus the number of natural transformations $Q \to Q$ is $4$.
\end{example}
\section{Functor Algebras}
Recall the fold functions that we introduced in \autoref{chp:introduction} in the category $\Set$:
\begin{alignat*}{5}
& & foldn : \; & (1 \to C) \to (C \to C) & & \to Nat & & \to C \\
& & foldr : \; & (1 \to C) \to (A \times C \to C) & & \to List\;A & & \to C
\end{alignat*}
These are examples of special \emph{F-algebras} in $\Set$. In this section we will introduce this notion and examine what makes the fold functions special.
\begin{definition}[F-Algebras]
Let $F : \CC \to \CC$ be an endofunctor on $\CC$. An \emph{F-algebra} is a pair $(A \in \obj{\CC}, a : FA \to a)$. Homomorphisms between F-algebras $(A,a)$ and $(B,b)$ are morphisms $f : A \to B$ such that
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFswLDIsIkZCIl0sWzIsMCwiQSJdLFsyLDIsIkIiXSxbMSwzLCJiIl0sWzAsMiwiYSJdLFswLDEsIkZmIiwyXSxbMiwzLCJmIl1d
\[
\begin{tikzcd}
FA && A \\
\\
FB && B
\arrow["b", from=3-1, to=3-3]
\arrow["a", from=1-1, to=1-3]
\arrow["Ff"', from=1-1, to=3-1]
\arrow["f", from=1-3, to=3-3]
\end{tikzcd}
\]
commutes.
\end{definition}
\begin{proposition}
F-algebras together with their homomorphisms form a category that we call $\Alg{F}$.
\end{proposition}
\begin{proof}
Identities and composition are inherited by the underlying category $\CC$. We are left to show that the identities are homomorphisms:
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJGQSJdLFswLDIsIkZBIl0sWzIsMCwiQSJdLFsyLDIsIkEiXSxbMSwxLCJcXGNvbW0iXSxbMSwzLCJhIl0sWzAsMiwiYSJdLFswLDEsIkZpZCIsMl0sWzIsMywiaWQiXV0=
\[
\begin{tikzcd}
FA && A \\
& \comm \\
FA && A
\arrow["a", from=3-1, to=3-3]
\arrow["a", from=1-1, to=1-3]
\arrow["Fid"', from=1-1, to=3-1]
\arrow["id", from=1-3, to=3-3]
\end{tikzcd}
\]
and that homomorphisms are closed under composition:
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJGQSJdLFswLDIsIkZCIl0sWzIsMCwiQSJdLFsyLDIsIkIiXSxbMSwxLCJcXGNvbW0iXSxbMCw0LCJGQyJdLFsyLDQsIkMiXSxbMSwzLCJcXGNvbW0iXSxbMSwzLCJiIl0sWzAsMiwiYSJdLFswLDEsIkZmIiwyXSxbMiwzLCJmIl0sWzUsNiwiYyJdLFsxLDUsIkZnIiwyXSxbMyw2LCJnIl0sWzAsNSwiRihnIFxcY2lyYyBmKSIsMix7ImN1cnZlIjo0fV0sWzIsNiwiZyBcXGNpcmMgZiIsMCx7ImN1cnZlIjotNH1dXQ==
\[
\begin{tikzcd}
FA && A \\
& \comm \\
FB && B \\
& \comm \\
FC && C
\arrow["b", from=3-1, to=3-3]
\arrow["a", from=1-1, to=1-3]
\arrow["Ff"', from=1-1, to=3-1]
\arrow["f", from=1-3, to=3-3]
\arrow["c", from=5-1, to=5-3]
\arrow["Fg"', from=3-1, to=5-1]
\arrow["g", from=3-3, to=5-3]
\arrow["{F(g \circ f)}"', curve={height=24pt}, from=1-1, to=5-1]
\arrow["{g \circ f}", curve={height=-24pt}, from=1-3, to=5-3]
\end{tikzcd}
\]
\end{proof}
\begin{example}\label{ex:Falg} Let us now consider the structure of the data types Nat and List as F-algebras:
\begin{enumerate}
\item \textbf{Nat}: Take $\CC = \Set$ and $FX = 1 + X$, the F-algebras and their morphisms have the following form:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgQSJdLFsyLDAsIkEiXSxbMCwyLCIxICsgQiJdLFsyLDIsIkIiXSxbMCwxLCJbYyxoXSJdLFsyLDMsIltjJywgaCddIl0sWzAsMiwiXFxiYW5nICsgZiIsMl0sWzEsMywiZiJdXQ==
\[
\begin{tikzcd}
{1 + A} && A \\
\\
{1 + B} && B
\arrow["{[c,h]}", from=1-1, to=1-3]
\arrow["{[c', h']}", from=3-1, to=3-3]
\arrow["{\bang + f}"', from=1-1, to=3-1]
\arrow["f", from=1-3, to=3-3]
\end{tikzcd}
\]
Which is equivalent to:
% https://q.uiver.app/#q=WzAsNSxbMiwwLCJBIl0sWzQsMCwiQSJdLFsyLDIsIkIiXSxbNCwyLCJCIl0sWzAsMCwiMSJdLFs0LDAsImMiXSxbMCwxLCJoIl0sWzIsMywiaCciXSxbNCwyLCJjJyIsMl0sWzAsMiwiZiIsMl0sWzEsMywiZiJdXQ==
\[
\begin{tikzcd}
1 && A && A \\
\\
&& B && B
\arrow["c", from=1-1, to=1-3]
\arrow["h", from=1-3, to=1-5]
\arrow["{h'}", from=3-3, to=3-5]
\arrow["{c'}"', from=1-1, to=3-3]
\arrow["f"', from=1-3, to=3-3]
\arrow["f", from=1-5, to=3-5]
\end{tikzcd}
\]
\item \textbf{List\;A}: Take $\CC = \Set$ and $FX = 1 + A \times X$, where $A \in \obj{\Set}$. The F-algebras and their morphisms take the following form:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgQSBcXHRpbWVzIFgiXSxbMCwyLCIxICsgQSBcXHRpbWVzIFkiXSxbMiwwLCJYIl0sWzIsMiwiWSJdLFswLDIsIltjLGhdIl0sWzEsMywiW2MsaF0iXSxbMiwzLCJmIl0sWzAsMSwiXFxiYW5nICsgaWQgXFx0aW1lcyBmIiwyXV0=
\[
\begin{tikzcd}
{1 + A \times X} && X \\
\\
{1 + A \times Y} && Y
\arrow["{[c,h]}", from=1-1, to=1-3]
\arrow["{[c,h]}", from=3-1, to=3-3]
\arrow["f", from=1-3, to=3-3]
\arrow["{\bang + id \times f}"', from=1-1, to=3-1]
\end{tikzcd}
\]
Which again is equivalent to
% https://q.uiver.app/#q=WzAsNSxbMiwwLCJBIFxcdGltZXMgWCJdLFsyLDIsIkEgXFx0aW1lcyBZIl0sWzQsMCwiWCJdLFs0LDIsIlkiXSxbMCwwLCIxIl0sWzAsMiwiaCJdLFsxLDMsImgiXSxbMiwzLCJmIl0sWzAsMSwiaWQgXFx0aW1lcyBmIiwyXSxbNCwwLCJjIl0sWzQsMSwiYyciLDJdXQ==
\[
\begin{tikzcd}
1 && {A \times X} && X \\
\\
&& {A \times Y} && Y
\arrow["h", from=1-3, to=1-5]
\arrow["h", from=3-3, to=3-5]
\arrow["f", from=1-5, to=3-5]
\arrow["{id \times f}"', from=1-3, to=3-3]
\arrow["c", from=1-1, to=1-3]
\arrow["{c'}"', from=1-1, to=3-3]
\end{tikzcd}
\]
\end{enumerate}
\end{example}
\subsection{Initial F-algebras}
\emph{Initial F-algebras} (i.e.\ the initial object in $\Alg{F}$) are of special interest to us. More concretely an F-algebra $(I, i)$ is initial if for every $(A, a)$ there exists a unique $\cata{a} : I \to A$ such that
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGSSJdLFsyLDAsIkkiXSxbMCwyLCJGQSJdLFsyLDIsIkEiXSxbMCwxLCJpIl0sWzAsMiwiRlxcY2F0YXthfSIsMl0sWzEsMywiXFxleGlzdHMhXFxjYXRhe2F9IiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzIsMywiYSIsMl1d
\[
\begin{tikzcd}
FI && I \\
\\
FA && A
\arrow["i", from=1-1, to=1-3]
\arrow["{F\cata{a}}"', from=1-1, to=3-1]
\arrow["{\exists!\cata{a}}", dashed, from=1-3, to=3-3]
\arrow["a"', from=3-1, to=3-3]
\end{tikzcd}
\]
commutes.
The dual notion of \emph{terminal F-algebra} is usually not of interested, since it is just inherited from $\CC$:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGQSJdLFsyLDAsIkEiXSxbMCwyLCJGMSJdLFsyLDIsIjEiXSxbMiwzLCIhIl0sWzAsMSwiYSJdLFswLDIsIkYhIiwyXSxbMSwzLCIhIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d
\[
\begin{tikzcd}
FA && A \\
\\
F1 && 1
\arrow["{!}", from=3-1, to=3-3]
\arrow["a", from=1-1, to=1-3]
\arrow["{F!}"', from=1-1, to=3-1]
\arrow["{!}", dashed, from=1-3, to=3-3]
\end{tikzcd}
\]
\begin{example}
Important examples of initial F-algebras include:
\begin{enumerate}
\item In \autoref{ex:Falg} (1) the data type $Nat$ is the initial algebra together with the function $foldn$ that we defined in the introduction. Where the following diagram expresses the defining equations for $foldn$:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgTmF0Il0sWzAsMiwiMSArIEMiXSxbMiwwLCJOYXQiXSxbMiwyLCJDIl0sWzAsMSwiISArZm9sZG4oYyxoKSIsMl0sWzAsMiwiW3plcm8sIHN1Y2NdIl0sWzIsMywiZm9sZG4oYyxoKSJdLFsxLDMsIltjLGhdIiwyXV0=
\[
\begin{tikzcd}
{1 + Nat} && Nat \\
\\
{1 + C} && C
\arrow["{id +foldn(c,h)}"', from=1-1, to=3-1]
\arrow["{[zero, succ]}", from=1-1, to=1-3]
\arrow["{foldn(c,h)}", from=1-3, to=3-3]
\arrow["{[c,h]}"', from=3-1, to=3-3]
\end{tikzcd}
\]
\item Similarly, in \autoref{ex:Falg} (2) the data type $List\;A$ is the initial algebra:
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIxICsgQSBcXHRpbWVzIExpc3RcXDtBIl0sWzIsMCwiTGlzdFxcO0EiXSxbMCwyLCIxICsgQSBcXHRpbWVzIEMiXSxbMiwyLCJDIl0sWzAsMSwiW25pbCxjb25zXSJdLFsyLDMsIltjLGhdIl0sWzEsMywiZm9sZHIoYyxoKSJdLFswLDIsImlkICsgZm9sZHIoYyxoKSIsMl1d
\[
\begin{tikzcd}
{1 + A \times List\;A} && {List\;A} \\
\\
{1 + A \times C} && C
\arrow["{[nil,cons]}", from=1-1, to=1-3]
\arrow["{[c,h]}", from=3-1, to=3-3]
\arrow["{foldr(c,h)}", from=1-3, to=3-3]
\arrow["{id + foldr(c,h)}"', from=1-1, to=3-1]
\end{tikzcd}
\]
% TODO add other examples
\end{enumerate}
\end{example}
We can now abstract the fusion and identity laws that we defined for each data type in \autoref{sec:datatypes}:
\begin{proposition}
Let $(I,i)$ be an initial F-algebra. The following holds:
\begin{enumerate}
\item \customlabel{law:ident}{\textbf{Identity}}: $\cata{i} = id_I : I \to I$,
\item \customlabel{law:fusion}{\textbf{Fusion}}: Let $f : (A,a) \to (B,b)$ be a homomorphism between F-algebras, then
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJJIl0sWzIsMCwiQSJdLFsyLDIsIkIiXSxbMCwxLCJcXGNhdGF7YX0iXSxbMSwyLCJmIl0sWzAsMiwiXFxjYXRhe2J9IiwyXV0=
\[
\begin{tikzcd}
I && A \\
\\
&& B
\arrow["{\cata{a}}", from=1-1, to=1-3]
\arrow["f", from=1-3, to=3-3]
\arrow["{\cata{b}}"', from=1-1, to=3-3]
\end{tikzcd}
\]
commutes.
\end{enumerate}
\end{proposition}
\begin{proof} Both follow by uniqueness of homomorphisms out of the initial object:
\begin{enumerate}
\item By uniqueness of homomorphisms $(I,i) \to (I,i)$
\item By uniqueness of homomorphisms $(I,i) \to (B,b)$
\end{enumerate}
\end{proof}
\begin{proposition}[Lambeks Lemma]
Let $(I,i)$ be an initial F-algebra. The F-algebra structure $i$ is an isomorphism.
\end{proposition}
\begin{proof}
Applying $F$ on $i$ yields another F-algebra $(FI, Fi)$, which induces a homomorphism $\cata{Fi} : I \rightarrow FI$. $\cata{FI}$ is the inverse to $i$. Consider
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJGSSJdLFsyLDAsIkkiXSxbMiwyLCJGSSJdLFswLDIsIkZGSSJdLFsxLDEsIlxcY29tbSJdLFswLDQsIkZJIl0sWzIsNCwiSSJdLFsxLDMsIlxcY29tbSJdLFswLDEsImkiXSxbMywyLCJGaSJdLFswLDMsIkZcXGNhdGF7Rml9Il0sWzEsMiwiXFxjYXRhe0ZpfSIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDYsImkiXSxbMyw1LCJGaSJdLFsyLDYsImkiLDJdLFswLDUsIkYoaSBcXGNvbXAgXFxjYXRhe0ZpfSkiLDIseyJjdXJ2ZSI6M31dLFsxLDYsImkgXFxjb21wIFxcY2F0YXtGaX0iLDAseyJjdXJ2ZSI6LTN9XV0=
\[
\begin{tikzcd}
FI && I \\
& \comm \\
FFI && FI \\
& \comm \\
FI && I
\arrow["i", from=1-1, to=1-3]
\arrow["Fi", from=3-1, to=3-3]
\arrow["{F\cata{Fi}}", from=1-1, to=3-1]
\arrow["{\cata{Fi}}"', dashed, from=1-3, to=3-3]
\arrow["i", from=5-1, to=5-3]
\arrow["Fi", from=3-1, to=5-1]
\arrow["i"', from=3-3, to=5-3]
\arrow["{F(i \comp \cata{Fi})}"', curve={height=18pt}, from=1-1, to=5-1]
\arrow["{i \comp \cata{Fi}}", curve={height=-18pt}, from=1-3, to=5-3]
\end{tikzcd}
\]
from which we can follow that $i \comp \cata{Fi} = id_I : (I,i) \to (I,i)$ by uniqueness of the homomorphisms and thus also
\[\cata{Fi} \comp i = Fi \comp F\cata{Fi} = F(i \comp \cata{Fi}) = F {id}_I = {id}_{FI}.\]
\end{proof}
\subsection{Term Algebras}
% TODO
\subsection{Parametric Data Types}
% TODO
\section{Functor Coalgebras}
\section{(co)Limits} % chktex 36
% TODO coalgebras
\subsection{Terminal F-Coalgebras}
\subsection{Corecursion and Coinduction}
\section{Limits}
\section{Colimits}