diff --git a/formalization.pdf b/formalization.pdf
index 823e5ae..038119c 100644
Binary files a/formalization.pdf and b/formalization.pdf differ
diff --git a/formalization.tex b/formalization.tex
index c43510d..41e78f9 100644
--- a/formalization.tex
+++ b/formalization.tex
@@ -512,6 +512,54 @@ \subsection{Partial Taxonomy of UFO: \me{Endurant Type} by Modal Properties of T
 
 
 
+% 06_instantiation.p
+\subsection{On the Definitions of \me{Type}, \me{Individual}, Instantiation, and Specialization}
+
+This subsection introduces the UFO's definitions of \me{Type} and \me{Individual} as well as the definitions for the relations of \me{instance of}, \me{specializes}, and \me{proper specializes}.
+
+\begin{figure}[ht]
+    \centering
+    \includegraphics[width=0.6\textwidth]{diagrams/Instantiation_Diagram.png}
+    \caption{Types, individuals, instantiation, and specialization.}
+    \label{fig:06_instantiation}
+\end{figure}
+
+\begin{itemize}
+    \item[\myax{ax_dIof}] The \me{instance of} relation can only hold between $x$, $y$, and $w$, where $x$ is an instance of a type $y$ in $w$, and $w$ is the world where this relation holds.
+    
+    $\forall x,y,w(\textsf{iof}(x,y,w)\rightarrow \textsf{type\_}(y)\wedge \textsf{world}(w))$
+
+    \lstinputlisting[firstline=1, lastline=6, firstnumber=1]{src/axioms-clif/06_instantiation.p.clif}
+    
+    % TODO: review the adopted explanation style; it may be interesting to adopt a more explanatory style for the definitions in natural language rather than a simple verbalization of an axiom; e.g., "Instance of relations can only hold between instances and types in some given world."
+    \item[\myax{ax_dType}] For every $x$, $x$ is a type ifif there exists some $y$ and $w$ such that $y$ is instance of $x$ in the world $w$.
+    
+    $\forall x(\textsf{type\_}(x)\leftrightarrow \exists y,w(\textsf{iof}(y,x,w)))$
+
+    \lstinputlisting[firstline=7, lastline=14, firstnumber=7]{src/axioms-clif/06_instantiation.p.clif}
+    
+    % TODO: review the adopted explanation style; e.g., "A type is a predicative entity that collects the characteristics manifested by its instances, such that $x$ is a type ifif there exists some world $w$ where it has some instance $y$."; notice that we may risk deviating from what the axiom says.
+    \item[\myax{ax_dIndividual}] For every $x$, $x$ is an individual ifif there is no pair $y$ and $w$ such that $y$ is instance of $x$ in $w$.
+    
+    $\forall x(\textsf{individual}(x)\leftrightarrow \neg \exists y,w(\textsf{iof}(y,x,w)))$
+
+    \lstinputlisting[firstline=15, lastline=22, firstnumber=15]{src/axioms-clif/06_instantiation.p.clif}
+    
+    \item[\myax{ax_multiLevel}] The instance $x$ in an instance of relation must be either a type or an individual.
+    
+    $\forall x,y,w(\textsf{iof}(x,y,w)\rightarrow \textsf{type\_}(x)\vee \textsf{individual}(x))$
+
+    \lstinputlisting[firstline=23, lastline=28, firstnumber=23]{src/axioms-clif/06_instantiation.p.clif}
+    
+    \item[\myax{ax_twoLevelConstrained}] Chains of instance of relations are limited to a depth of two.
+    % TODO: we must verify whether the formalization is enforcing a strict stratification of ordered types, otherwise we cannot state the following;
+    % In other words, this formalization only accounts for types whose instances are individuals (i.e., first-order types), and types whose instances include first-order types (i.e., second-order types).
+    
+    $\neg \exists x,y,z,w(\textsf{type\_}(x)\wedge \textsf{iof}(x,y,w)\wedge \textsf{iof}(y,z,w))$
+
+    \lstinputlisting[firstline=29, lastline=33, firstnumber=29]{src/axioms-clif/06_instantiation.p.clif}
+\end{itemize}
+
 
 % ------------------------------ BEGIN DEPRECATED ------------------------------
 
diff --git a/src/axioms-clif/06_instantiation.p.clif b/src/axioms-clif/06_instantiation.p.clif
index 09d975b..78f30e1 100644
--- a/src/axioms-clif/06_instantiation.p.clif
+++ b/src/axioms-clif/06_instantiation.p.clif
@@ -4,7 +4,7 @@
 		(and (type_ y) (world w)))
 	)
 )
-(cl-text  ax_dType_a1
+(cl-text  ax_dType
 (forall (x)
 	(iff (type_ x)
 		(exists (y w)
@@ -12,7 +12,7 @@
 		)
 	)
 )
-(cl-text  ax_dIndividual_a2
+(cl-text  ax_dIndividual
 (forall (x)
 	(iff (individual x)
 		(not (exists (y w)
@@ -20,13 +20,13 @@
 		))
 	)
 )
-(cl-text  ax_multiLevel_a3
+(cl-text  ax_multiLevel
 (forall (x y w)
 	(if (iof x y w)
 		(or (type_ x) (individual x)))
 	)
 )
-(cl-text  ax_twoLevelConstrained_a4
+(cl-text  ax_twoLevelConstrained
 (not (exists (x y z w)
 	(and (type_ x) (iof x y w) (iof y z w)))
 )
diff --git a/src/axioms/06_instantiation.p b/src/axioms/06_instantiation.p
index 6047dc3..e338d81 100644
--- a/src/axioms/06_instantiation.p
+++ b/src/axioms/06_instantiation.p
@@ -2,18 +2,18 @@ fof(ax_dIof, axiom, (
   ![X,Y,W]: (iof(X,Y,W) => (type_(Y) & world(W)))
 )).
 
-fof(ax_dType_a1, axiom, (
+fof(ax_dType, axiom, (
   ![X]: (type_(X) <=> (?[Y,W]: iof(Y,X,W)))
 )).
 
-fof(ax_dIndividual_a2, axiom, (
+fof(ax_dIndividual, axiom, (
   ![X]: (individual(X) <=> (~?[Y,W]: iof(Y,X,W)))
 )).
 
-fof(ax_multiLevel_a3, axiom, (
+fof(ax_multiLevel, axiom, (
   ![X,Y,W]: (iof(X,Y,W) => (type_(X) | individual(X)))
 )).
 
-fof(ax_twoLevelConstrained_a4, axiom, (
+fof(ax_twoLevelConstrained, axiom, (
   ~?[X,Y,Z,W]: (type_(X) & iof(X,Y,W) & iof(Y,Z,W))
 )).
\ No newline at end of file