diff --git a/aspUnify.tex b/aspUnify.tex
index fbd05dc..ee4b63c 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -75,6 +75,21 @@ Java has adopted more and more type inference features over time.
 Currently Java only has local type inference.
 We want to bring type inference for Java to the next level.
 
+\section{Subtyping}
+\begin{mathpar}
+\inferrule[Refl]{}{
+\type{T} <: \type{T}
+}
+\and
+\inferrule[Trans]{\type{T}_1 <: \type{T}_2 \\ \type{T}_2 <: \type{T}_3}{
+\type{T}_1 <: \type{T}_3
+}
+\and
+\inferrule[Class]{\texttt{class}\ \exptype{C}{\ol{X}} \triangleleft \type{N}}{
+\exptype{C}{\ol{T}} <: [\ol{T}/\ol{X}]\type{N}
+}
+\end{mathpar}
+
 \section{Unify}
 Input: Every type placeholder must have an upper bound.
 Output: Every $\tv{a} \lessdot \type{T}$ constraint gets a