+\subsection{What is done, what is missing}
+
+Sadly the author ran out of time while implementing observational
+equality, and while the constructs and typing rules are present, the
+machinery to make it happen (equality reduction, coercions, quotation,
+etc.) is not present yet. Everything else presented is implemented and
+working reasonably well.
+
+\subsection{Syntax}
+
+\begin{figure}[p]
+ $
+ \begin{array}{@{\ \ }l@{\ }c@{\ }l}
+ \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\
+ \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\
+ \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind.}} \\
+ \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\
+ \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\
+ \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\
+ \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
+ \multicolumn{3}{@{}l}{
+ \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
+ \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
+ & | & \mytermi{*} & \text{\mytyc{Type}.} \\
+ & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
+ & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
+ & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
+ & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
+ & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
+ & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
+ & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
+ & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
+ & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
+ \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
+ & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
+ & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
+ & | & \mysee{arr} \\
+ \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
+ & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
+ & | & \mysee{term}{+} & \text {Application.}
+ \end{array}
+ } \\
+ \multicolumn{3}{@{}l}{\text{Typed names.}} \\
+ \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
+ \multicolumn{3}{@{}l}{\text{Declarations.}} \\
+ \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
+ \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
+ \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
+ \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
+ \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
+ \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
+ \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
+ \mysee{constrs} & ::= & \mysee{typed} \\
+ & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
+ \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
+ \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
+ \mysee{projs} & ::= & \mysee{typed} \\
+ & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
+ \end{array}
+ $
+
+ \caption{\mykant' syntax. The non-terminals are marked with
+ $\langle\text{angle brackets}\rangle$ for greater clarity. The
+ syntax in the implementation is actually more liberal, for example
+ giving the possibility of using arrow types directly in
+ constructor/projection declarations.}
+ \label{fig:syntax}
+\end{figure}
+
+The syntax of \mykant\ is presented in Figure \ref{fig:syntax}.
+Examples showing the usage of most of the constructs are present in
+Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and
+\ref{app:hurkens}.
+