pdf

Author: 5HT

doc/anders.tex

@@ -333,7 +333,7 @@ \subsection{Dependent Types}
 
 The presheaf with only Pi and Sigma is called \textbf{MLTT-72} \cite{MLTT72}. Its internalization in \textbf{anders} is as follows:
 
-\begin{table}[ht!][ht!]
+\begin{table}[ht!]
 \tabstyle
 \begin{tabular}{rl}
 \textbf{def} & MLTT-72 (A : U) (B : A $\rightarrow$ U) : U := $\Sigma$ \\