diff --git a/docs/roqfy.tex b/docs/roqfy.tex
index 03a8ffd..0982767 100644
--- a/docs/roqfy.tex
+++ b/docs/roqfy.tex
@@ -6,7 +6,7 @@
 \usepackage{amssymb}
 \usepackage{amsthm}
 \usepackage{unicode-math}
-\usepackage{bussproofs}
+\usepackage{ebproof}
 
 \usepackage{todonotes}
 \setuptodonotes{size=\tiny}
@@ -19,6 +19,36 @@
 \begin{document}
 \maketitle
 
+\section{Types}
 
+\[
+  \begin{prooftree}
+    \infer0{\vdash 0 : \text{Int}}
+  \end{prooftree}
+  \\
+  \begin{prooftree}
+    \hypo{Γ \vdash n : \text{Int}}
+    \hypo{Γ \vdash m : \text{Int}}
+    \infer2{Γ \vdash n \text{ + } m : \text{Int}}
+  \end{prooftree}
+  \\
+  \begin{prooftree}
+    \hypo{Γ \vdash n : \text{Int}}
+    \hypo{Γ \vdash m : \text{Int}}
+    \infer2{Γ \vdash n \text{ * } m : \text{Int}}
+  \end{prooftree}
+\]
+
+\[
+  \begin{prooftree}
+    \infer0{\vdash \text{o} : \text{\{\}}}
+  \end{prooftree}
+  \\
+  \begin{prooftree}
+    \hypo{Γ, (T_i : \text{Type})_i^* \vdash v : \{ x_i : T_i \}_i}
+    \hypo{Γ, T : \text{Type} \vdash y : T}
+    \infer2{Γ, (T_i : \text{Type})_i^*, T : \text{Type} \vdash v \text{ // } x_y = y : \{ x_i : T_i \} - x_y \cup \{ x_y : T \}}
+  \end{prooftree}
+\]
 
 \end{document}