diff --git a/info/exercises/ex-05-sol.pdf b/info/exercises/ex-05-sol.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..d263d673ab1b9625b22bbc50032c975948955f3a
Binary files /dev/null and b/info/exercises/ex-05-sol.pdf differ
diff --git a/info/exercises/ex-05.pdf b/info/exercises/ex-05.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..fd0ed338333c688e71acb42d61d99444d5217879
Binary files /dev/null and b/info/exercises/ex-05.pdf differ
diff --git a/info/exercises/src/ex-05/ex/check.tex b/info/exercises/src/ex-05/ex/check.tex
new file mode 100644
index 0000000000000000000000000000000000000000..d8cb5b11e66f3cefe9acaba07a22b50f754d045c
--- /dev/null
+++ b/info/exercises/src/ex-05/ex/check.tex
@@ -0,0 +1,61 @@
+
+% do type checking for some simple terms
+
+\pagebreak
+\begin{exercise}{}
+ For each of the following term-type pairs \((t, \tau)\), check whether the
+ term can be ascribed with the given type, i.e., whether there exists a
+ derivation of \(\Gamma \vdash t: \tau\) for some typing context \(\Gamma\) in
+ the given system. If not, briefly argue why.
+
+ \begin{enumerate}
+ \item \(\lstinline|x|, \abool\)
+ \item \(\lstinline|x| + 1, \aint\)
+ \item \(\lstinline|(x && y) == (x <= 0)|, \abool\)
+ \item \(\lstinline|f| ~\ato~ \lstinline|x| ~\ato~ \lstinline|y| ~\ato~ \lstinline|f((x, y))|\):
+
+ \lstinline|((List[Int], Bool) => Int) => List[Int] => Bool => Int|
+ \item \lstinline|Cons(x, x)| : \lstinline|List[List[Int]]|
+ \end{enumerate}
+
+ \begin{solution}
+ \begin{enumerate}
+ \item \lstinline|x, Bool|. Derivation, assume \lstinline|x| is a boolean:
+ \begin{equation*}
+ \AxiomC{\((\lstinline|x|, \abool) \in \{(\lstinline|x|, \abool)\}\)}
+ \UnaryInfC{\(\{(\lstinline|x|, \abool)\} \vdash \lstinline|x: Bool|\)}
+ \DisplayProof
+ \end{equation*}
+ Note that this would work with any type, as there are no constraints.
+ \item \(\lstinline|x| + 1, \aint\). Derivation, assume \lstinline|x| is an
+ integer:
+ \begin{equation*}
+ \AxiomC{\((\lstinline|x|, \aint) \in \{(\lstinline|x|, \aint)\}\)}
+ \UnaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|x: Int|\)}
+ \AxiomC{\(1 \in \naturals\)}
+ \UnaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|1: Int|\)}
+ \BinaryInfC{\(\{(\lstinline|x|, \aint)\} \vdash \lstinline|x + 1: Int|\)}
+ \DisplayProof
+ \end{equation*}
+ Due to addition constraining the type of \lstinline|x|, other possible
+ types would not work.
+ \item \(\lstinline|(x && y) == (x <= 0)|, \abool\). Not well-typed.
+ From the left-hand side, we would enforce that \lstinline|x: Bool|, but on
+ the right, we find \lstinline|x: Int|. Due to this conflict, there is no
+ valid derivation for this term.
+ \item \lstinline|f => x => y => f((x, y))|: this is the currying function.
+ Note that it will conform to \lstinline|((a, b) => c) => a => b => c| for any choice
+ of \lstinline|a|, \lstinline|b|, and \lstinline|c|. (check)
+ \item \lstinline|Cons(x, x)| : \lstinline|List[List[Int]]|. Not
+ well-typed. The \(cons\) rule tells us that the second argument must have
+ the same type as the result, so \lstinline|x: List[List[Int]]|, but the first
+ argument enforces the type to be \lstinline|List[Int]| (again, due to result
+ type). As \(\aint \neq \alist{\aint}\), this is not well-typed.
+
+ Note that the singular assignment of \lstinline|x| to \lstinline|Nil()|
+ can make a well typed term here, but the typing must hold for \emph{all}
+ possible values of \lstinline|x|.
+ \end{enumerate}
+ \end{solution}
+
+\end{exercise}
diff --git a/info/exercises/src/ex-05/ex/map.tex b/info/exercises/src/ex-05/ex/map.tex
new file mode 100644
index 0000000000000000000000000000000000000000..7c487fc7b7c117eea6831e637ab486a33e6c6aa2
--- /dev/null
+++ b/info/exercises/src/ex-05/ex/map.tex
@@ -0,0 +1,117 @@
+
+\begin{exercise}{}
+ Consider the following term \(t\):
+ %
+ \begin{center}
+ \(t = \) \lstinline{l => map(l, x => fst(x)(snd(x)) + snd(x))}
+ % t = \lstinline|l| ~\ato~ \lstinline|map|(\lstinline|l|, \lstinline|x| ~\ato~ \afst{\lstinline|x|}(\asnd{\lstinline|x|}) + \asnd{\lstinline|x|})
+ \end{center}
+
+ where \lstinline|map| is a function with type \(\forall \tau, \pi.\;
+ \alist{\tau} ~\ato~ (\tau ~\ato~ \pi) ~\ato~ \alist{\pi}\).
+
+ \begin{enumerate}
+ \item Label and assign type variables to each subterm of \(t\).
+ \item Generate the constraints on the type variables, assuming \(t\) is
+ well-typed, to infer the type of \(t\).
+ \item Solve the constraints via unification to deduce the type of \(t\).
+ \end{enumerate}
+
+ \begin{solution}
+ \begin{enumerate}
+ \item We can label the subterms in the following way:
+ \begin{gather}
+ t: \tau = \lstinline|l => map(l, x => fst(x)(snd(x)) + snd(x))| \\
+ t_1: \tau_1 = \lstinline|map(l, x => fst(x)(snd(x)) + snd(x))| \\
+ t_2: \tau_2 = \lstinline|x => fst(x)(snd(x)) + snd(x)| \\
+ t_3: \tau_3 = \lstinline|fst(x)(snd(x)) + snd(x)| \\
+ t_4: \tau_4 = \lstinline|fst(x)(snd(x))| \\
+ t_5: \tau_5 = \lstinline|snd(x)| \\
+ t_6: \tau_6 = \lstinline|fst(x)| \\
+ \lstinline|l|: \tau_7 = \lstinline|l| \\
+ \lstinline|x|: \tau_8 = \lstinline|x| \\
+ \lstinline|map|: \tau_9 = \lstinline|map|
+ \end{gather}
+ We can choose to separately label \lstinline|x|, \lstinline|l|, and
+ \lstinline|map|, but it does not make any difference to the result.
+
+ \item
+ Inserting the type of \lstinline|map| (thus removing \(\tau_9\)), and
+ adding constraints by looking at the top-level of each subterm, we can get
+ the set of initial constraints, labelled by the subterm equation above
+ they come from:
+ \begin{gather*}
+ \tau = \tau_7 ~\ato~ \tau_1 \tag{1} \\
+ \tau_1 = \alist{\tau_3} \tag{2, 4} \\
+ \tau_7 = \alist{\tau_8} \tag{2, 9} \\
+ \tau_2 = \tau_8 ~\ato~ \tau_3 \tag{3} \\
+ \tau_3 = \aint \tag{4} \\
+ \tau_4 = \aint \tag{4} \\
+ \tau_5 = \aint \tag{4} \\
+ \tau_6 = \tau_5 ~\ato~ \tau_4 \tag{5} \\
+ \tau_8 = (\tau_5', \tau_5) \tag{6} \\
+ \tau_8 = (\tau_6, \tau_6') \tag{7}
+ \end{gather*}
+ for fresh type variables \(\tau_5'\) and \(\tau_6'\) arising from the rule
+ for pairs.
+
+ \item
+ The constraints can be solved step-by-step (major steps shown):
+ \begin{enumerate}
+ \item Eliminating known types (\(\tau_3, \tau_4, \tau_5\)):
+ \begin{gather*}
+ \tau = \tau_7 ~\ato~ \tau_1 \\
+ \tau_1 = \alist{\aint} \\
+ \tau_7 = \alist{\tau_8} \\
+ \tau_2 = \tau_8 ~\ato~ \aint \\
+ \tau_6 = \aint ~\ato~ \aint \\
+ \tau_8 = (\tau_5', \aint) \\
+ \tau_8 = (\tau_6, \tau_6')
+ \end{gather*}
+ \item Eliminating \(\tau_1, \tau_6\):
+ \begin{gather*}
+ \tau = \tau_7 ~\ato~ \alist{\aint} \\
+ \tau_7 = \alist{\tau_8} \\
+ \tau_2 = \tau_8 ~\ato~ \aint \\
+ \tau_8 = (\tau_5', \aint) \\
+ \tau_8 = (\aint ~\ato~ \aint, \tau_6')
+ \end{gather*}
+ \item Eliminating \(\tau_8\) using either of its equations:
+ \begin{gather*}
+ \tau = \tau_7 ~\ato~ \alist{\aint} \\
+ \tau_7 = \alist{(\tau_5', \aint)} \\
+ \tau_2 = (\tau_5', \aint) ~\ato~ \aint \\
+ (\tau_5', \aint) = (\aint ~\ato~ \aint, \tau_6')
+ \end{gather*}
+ \item Performing unification of the pair type:
+ \begin{gather*}
+ \tau = \tau_7 ~\ato~ \alist{\aint} \\
+ \tau_7 = \alist{(\tau_5', \aint)} \\
+ \tau_2 = (\tau_5', \aint) ~\ato~ \aint \\
+ \tau_5' = \aint ~\ato~ \aint \\
+ \aint = \tau_6'
+ \end{gather*}
+ \item Eliminating \(\tau_5'\) and \(\tau_6'\):
+ \begin{gather*}
+ \tau = \tau_7 ~\ato~ \alist{\aint} \\
+ \tau_7 = \alist{(\aint ~\ato~ \aint, \aint)} \\
+ \tau_2 = (\aint ~\ato~ \aint, \aint) ~\ato~ \aint
+ \end{gather*}
+ \item Eliminating \(\tau_2, \tau_7\):
+ \begin{gather*}
+ \tau = \alist{(\aint ~\ato~ \aint, \aint)} ~\ato~ \alist{\aint}
+ \end{gather*}
+ \item Finally, all type variables are assigned, as we eliminate \(\tau\):
+ \begin{gather*}
+ \emptyset \text{ (no constraints left)}
+ \end{gather*}
+ \end{enumerate}
+
+ The type of \(t\) as discovered by the unification process is:
+ \begin{gather*}
+ \tau = \alist{(\aint ~\ato~ \aint, \aint)} ~\ato~ \alist{\aint}
+ \end{gather*}
+ \end{enumerate}
+ \end{solution}
+
+\end{exercise}
diff --git a/info/exercises/src/ex-05/ex/program.tex b/info/exercises/src/ex-05/ex/program.tex
new file mode 100644
index 0000000000000000000000000000000000000000..137669d10e938a4c7dec1f329cc90fe36953acc2
--- /dev/null
+++ b/info/exercises/src/ex-05/ex/program.tex
@@ -0,0 +1,73 @@
+
+\begin{exercise}{}
+
+ A \emph{program} is a top-level expression \(t\) accompanied by a set of
+ user-provided function definitions. The program is well-typed if each of the
+ function bodies conform to the type of the function, and the top-level
+ expression is well-typed in the context of the function definitions.
+
+ For each of the following function definitions, check whether the function
+ body is well-typed:
+ %
+ \begin{enumerate}
+ \item \lstinline|def f(x: Int, y: Int): Bool = x <= y|
+ \item \lstinline|def rec(x: Int): Int = rec(x)|
+ \item \lstinline|def fib(n: Int): Int = if n <= 1 then 1 else (fib(n - 1) + fib(n - 2))|
+ \end{enumerate}
+
+ \begin{solution}
+ \begin{enumerate}
+ \item Well-typed, apply rule \(Leq\).
+ \item Well-typed. We need to check if the body conforms to the output
+ type, if we know the function and its parameters have their ascribed type.
+ So, under the context \lstinline|rec: Int => Int, x: Int|, we need to
+ prove that \lstinline|rec(x): Int|. This follows from the \(app\) rule.
+
+ So, if we allow recursion and do not check for termination, we can prove
+ unexpected things using the non-terminating programs.
+ \item Well-typed. We need to produce a derivation of the following:
+ \begin{equation*}
+ \lstinline|fib: Int => Int|, \lstinline|n: Int| \vdash \lstinline|if n <= 1 then 1 else (fib(n - 1) + fib(n - 2)): Int|
+ \end{equation*}
+ i.e., given that \lstinline|fib| inductively has type \lstinline|Int => Int| and
+ the parameter \lstinline|n| has type \lstinline|Int|, we need to prove that the
+ body of the function has the ascribed type \lstinline|Int|.
+
+ The derivation can be constructed by following the structure of the term
+ on the right-hand side, the body. We set \(\Gamma =
+ %
+ \lstinline|fib: Int => Int|, \lstinline|n: Int|\) for brevity. The \lstinline|n-2|
+ branch is skipped due to space and being the same as the \lstinline|n-1| branch.
+ \begin{equation*}
+ \hspace*{-4cm}
+ \AxiomC{\((\lstinline|n|, \aint) \in \Gamma\)}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|n: Int|\)}
+ \AxiomC{\(1 \in \naturals\)}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+ \BinaryInfC{\(\Gamma \vdash \lstinline|n <= 1: Bool|\)}
+ %
+ \AxiomC{\(1 \in \naturals\)}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+ %
+ \AxiomC{\((\lstinline|fib, Int => Int|) \in \Gamma\)}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|fib: Int => Int|\)}
+ \AxiomC{\((\lstinline|n|, \aint) \in \Gamma\)}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|n: Int|\)}
+ \AxiomC{\(1 \in \naturals\)}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|1: Int|\)}
+ \BinaryInfC{\(\Gamma \vdash \lstinline|(n - 1): Int|\)}
+ \BinaryInfC{\(\Gamma \vdash \lstinline|fib(n - 1): Int|\)}
+ %
+ \AxiomC{\ldots}
+ \UnaryInfC{\(\Gamma \vdash \lstinline|fib(n - 2): Int|\)}
+ %
+ \BinaryInfC{\(\Gamma \vdash \lstinline|fib(n - 1) + fib(n - 2): Int|\)}
+ %
+ \TrinaryInfC{\(\Gamma \vdash \lstinline|if n <= 1 then 1 else (fib(n - 1) + fib(n - 2)): Int|\)}
+ \DisplayProof
+ \end{equation*}
+ \end{enumerate}
+
+ \end{solution}
+
+\end{exercise}
diff --git a/info/exercises/src/ex-05/ex/rec-inf.tex b/info/exercises/src/ex-05/ex/rec-inf.tex
new file mode 100644
index 0000000000000000000000000000000000000000..c5364bbf63032dbcf9f172761def4e9fe958fe00
--- /dev/null
+++ b/info/exercises/src/ex-05/ex/rec-inf.tex
@@ -0,0 +1,66 @@
+
+
+\pagebreak
+\begin{exercise}{}
+
+ Consider the following definition for a recursive function \(g\):
+
+ \begin{equation*}
+ \lstinline|def g(n, x) = if n <= 2 then (x, x) else (x, g(n - 1, x))|
+ \end{equation*}
+
+ \begin{enumerate}
+ \item Evaluate \(g(3, 1)\) and \(g(4, 2)\) using the definition of \(g\).
+ Suggest a type for the function \(g\) based on your observations.
+ \item Label and assign type variables to the definition parameters, body,
+ and its subterms.
+ \item Generate the constraints on the type variables, assuming the
+ definition of \(g\) is well-typed.
+ \item Attempt to solve the generated constraints via unification. Argue how
+ the result correlates to your observations from evaluating \(g\).
+ \end{enumerate}
+
+ \begin{solution}
+ \begin{enumerate}
+ \item \lstinline|g(3, 1)| evaluates to \lstinline|(1, (1, 1))| and
+ \lstinline|g(4, 2)| evaluates to \lstinline|(2, (2, (2, 2)))|. Notably,
+ these two come from disjoint types. This suggests that the function \(g\)
+ is not well-typed.
+ \item We can label the parameters, subterms, and assign a type to the
+ function:
+ \setcounter{equation}{0}
+ \begin{gather}
+ \lstinline|g|: \tau \\
+ \lstinline|n|: \tau_n \\
+ \lstinline|x|: \tau_x \\
+ body: \tau_1 = \lstinline|if n <= 2 then (x, x) else (x, g(n - 1, x))| \\
+ t_1: \tau_2 = \lstinline|n <= 2| \\
+ t_2: \tau_3 = \lstinline|(x, x)| \\
+ t_3: \tau_4 = \lstinline|(x, g(n - 1, x))| \\
+ t_4: \tau_5 = \lstinline|g(n - 1, x)| \\
+ t_5: \tau_6 = \lstinline|n - 1|
+ \end{gather}
+ \item We can generate the constraints by looking at the top-level of each
+ subterm equation:
+ \begin{gather*}
+ \tau = \tau_n ~\ato~ \tau_x ~\ato~ \tau_1 \tag{1, def} \\
+ \tau_1 = \tau_3 \tag{4} \\
+ \tau_1 = \tau_4 \tag{4} \\
+ \tau_2 = \abool \tag{4} \\
+ \tau_n = \aint \tag{5} \\
+ \tau_3 = (\tau_x, \tau_x) \tag{6} \\
+ \tau_4 = (\tau_x, \tau_5) \tag{6} \\
+ \tau_5 = \tau_1 \tag{7, def} \\
+ \tau_6 = \aint \tag{9}
+ \end{gather*}
+ \item The constraints can be solved (eliminating \(\tau_4, \tau_5\)) to
+ reach a set of constraints containing the recursive constraint \(\tau_1 =
+ (\tau_x, \tau_1)\). There is no type \(\tau_1\) (the output type of
+ \lstinline|g|!) satisfying this.
+
+ This matches our previous observation where \lstinline|g| produced two
+ different sized tuples as its output.
+ \end{enumerate}
+ \end{solution}
+
+\end{exercise}
\ No newline at end of file
diff --git a/info/exercises/src/ex-05/ex/system.tex b/info/exercises/src/ex-05/ex/system.tex
new file mode 100644
index 0000000000000000000000000000000000000000..ebe61c6cf2c431bff7f5e9f0d64ea9f12ea1fad0
--- /dev/null
+++ b/info/exercises/src/ex-05/ex/system.tex
@@ -0,0 +1,112 @@
+
+% we want lists, pairs
+% both parametric
+% we want some functions, as well as function definitions
+% we want to be able to define and typecheck recursive functions
+
+Consider a type system for a simple functional language, consisting of integers,
+booleans, parametric pairs, and lists. The rest of the exercises will revolve
+around this system.
+
+% language components
+\newcommand{\aint}{\lstinline|int|}
+\newcommand{\abool}{\lstinline|bool|}
+\newcommand{\aif}{\lstinline|if|}
+\newcommand{\athen}{\lstinline|then|}
+\newcommand{\aelse}{\lstinline|else|}
+\newcommand{\apair}[2]{(#1, #2)}
+\newcommand{\afst}[1]{\lstinline|fst|(#1)}
+\newcommand{\asnd}[1]{\lstinline|snd|(#1)}
+\newcommand{\alist}[1]{\lstinline|List[|#1\lstinline|]|}
+\newcommand{\anil}{\lstinline|Nil()|}
+\newcommand{\acons}[2]{\lstinline|Cons(|#1, #2\lstinline|)|}
+\newcommand{\ato}{\lstinline|=>|}
+
+%%% Actual type system
+\begin{gather*}
+ % variables
+ \AxiomC{\((x, \tau) \in \Gamma\)}
+ \RightLabel{(var)}
+ \UnaryInfC{\(\Gamma \vdash x : \tau\)}
+ \DisplayProof \\
+ % integers
+ \AxiomC{\(n\) is an integer value}
+ \RightLabel{(int)}
+ \UnaryInfC{\(\Gamma \vdash \num(n) : \aint\)}
+ \DisplayProof \\
+ % + -
+ \AxiomC{\(e_1 : \aint\)}
+ \AxiomC{\(e_2 : \aint\)}
+ \RightLabel{(+)}
+ \BinaryInfC{\(\Gamma \vdash e_1 + e_2 : \aint\)}
+ \DisplayProof \qquad
+ \AxiomC{\(e_1 : \aint\)}
+ \AxiomC{\(e_2 : \aint\)}
+ \RightLabel{(-)}
+ \BinaryInfC{\(\Gamma \vdash e_1 - e_2 : \aint\)}
+ \DisplayProof \\
+ % booleans
+ \AxiomC{\(b\) is a boolean value}
+ \RightLabel{(bool)}
+ \UnaryInfC{\(\Gamma \vdash \abool(b) : \abool\)}
+ \DisplayProof \\
+ % props
+ \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+ \AxiomC{\(\Gamma \vdash e_2 : \abool\)}
+ \RightLabel{(and)}
+ \BinaryInfC{\(\Gamma \vdash e_1 \land e_2 : \abool\)}
+ \DisplayProof \qquad
+ \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+ \AxiomC{\(\Gamma \vdash e_2 : \abool\)}
+ \RightLabel{(or)}
+ \BinaryInfC{\(\Gamma \vdash e_1 \lor e_2 : \abool\)}
+ \DisplayProof \\
+ \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+ \RightLabel{(not)}
+ \UnaryInfC{\(\Gamma \vdash \neg e_1 : \abool\)}
+ \DisplayProof \\
+ % ite
+ \AxiomC{\(\Gamma \vdash e_1 : \abool\)}
+ \AxiomC{\(\Gamma \vdash e_2 : \tau\)}
+ \AxiomC{\(\Gamma \vdash e_3 : \tau\)}
+ \RightLabel{(ite)}
+ \TrinaryInfC{\(\Gamma \vdash \aif \, e_1 \, \athen \, e_2 \, \aelse \, e_3 : \tau\)}
+ \DisplayProof \\
+ % pairs
+ \AxiomC{\(\Gamma \vdash e_1 : \tau_1\)}
+ \AxiomC{\(\Gamma \vdash e_2 : \tau_2\)}
+ \RightLabel{(pair)}
+ \BinaryInfC{\(\Gamma \vdash \apair{e_1}{e_2} : \apair{\tau_1}{\tau_2}\)}
+ \DisplayProof \\
+ % fst
+ \AxiomC{\(\Gamma \vdash e : \apair{\tau_1}{\tau_2}\)}
+ \RightLabel{(fst)}
+ \UnaryInfC{\(\Gamma \vdash \afst{e} : \tau_1\)}
+ \DisplayProof \qquad
+ % snd
+ \AxiomC{\(\Gamma \vdash e : \apair{\tau_1}{\tau_2}\)}
+ \RightLabel{(snd)}
+ \UnaryInfC{\(\Gamma \vdash \asnd{e} : \tau_2\)}
+ \DisplayProof \\
+ % lists
+ \AxiomC{\phantom{\(e \in \alist{\tau}\)}}
+ \RightLabel{(nil)}
+ \UnaryInfC{\(\Gamma \vdash \anil : \alist{\tau}\)}
+ \DisplayProof \qquad
+ \AxiomC{\(\Gamma \vdash e_1 : \tau\)}
+ \AxiomC{\(\Gamma \vdash e_2 : \alist{\tau}\)}
+ \RightLabel{(cons)}
+ \BinaryInfC{\(\Gamma \vdash \acons{e_1}{e_2} : \alist{\tau}\)}
+ \DisplayProof \\
+ % functions
+ \AxiomC{\(\Gamma, x : \tau_1 \vdash e : \tau_2\)}
+ \RightLabel{(fun)}
+ \UnaryInfC{\(\Gamma \vdash \lambda x : \tau_1 ~\ato~ e : \tau_1 ~\ato~ \tau_2\)}
+ \DisplayProof \qquad
+ % application
+ \AxiomC{\(\Gamma \vdash e_1 : \tau_1 ~\ato~ \tau_2\)}
+ \AxiomC{\(\Gamma \vdash e_2 : \tau_1\)}
+ \RightLabel{(app)}
+ \BinaryInfC{\(\Gamma \vdash e_1 \, e_2 : \tau_2\)}
+ \DisplayProof \\
+\end{gather*}
diff --git a/info/exercises/src/ex-05/main.tex b/info/exercises/src/ex-05/main.tex
new file mode 100644
index 0000000000000000000000000000000000000000..ae5544de28a216f881f648f6db083b36ad452c08
--- /dev/null
+++ b/info/exercises/src/ex-05/main.tex
@@ -0,0 +1,35 @@
+\documentclass[a4paper]{article}
+
+\input{../macro}
+
+\ifdefined\ANSWERS
+ \if\ANSWERS1
+ \printanswers
+ \fi
+\fi
+
+\DeclareMathOperator{\half}{half}
+\newcommand{\num}{\ensuremath{\mathbf{num}}}
+
+\title{CS 320 \\ Computer Language Processing\\Exercise Set 5}
+\author{}
+\date{April 02, 2025}
+
+\begin{document}
+\maketitle
+
+% type system
+% do some type checking
+% some unification
+% some inference
+\input{ex/system}
+
+\input{ex/check}
+
+\input{ex/program}
+
+\input{ex/map}
+
+\input{ex/rec-inf}
+
+\end{document}