preliminaries.tex

\chapter{类型论}
\label{cha:typetheory}

\section{类型论与集合论}
\label{sec:types-vs-sets}
\input{source/preliminaries/types-vs-sets}

\section{函数类型}
\label{sec:function-types}
\input{source/preliminaries/function-types}

\section{全集和族}
\label{sec:universes}
\input{source/preliminaries/universes}

\section{依值函数类型 (\texorpdfstring{$\Pi$}{Π}-类型)}
\label{sec:pi-types}
\input{source/preliminaries/pi-types.tex}

\section{乘积类型}
\label{sec:finite-product-types}
\input{source/preliminaries/finite-product-types}

\section{依值序对类型 (\texorpdfstring{$\Sigma$}{Σ}-类型)}
\label{sec:sigma-types}
\input{source/preliminaries/sigma-types}

\section{余积类型}
\label{sec:coproduct-types}
\input{source/preliminaries/coproduct-types}

\section{布尔类型}
\label{sec:type-booleans}
\input{source/preliminaries/type-booleans}

\section{自然数}
\label{sec:inductive-types}
\input{source/preliminaries/inductive-types}

\section{模式匹配和递归}
\label{sec:pattern-matching}
\input{source/preliminaries/pattern-matching}

\section{命题作为类型}
\label{sec:pat}
\input{source/preliminaries/pat.tex}

\section{恒等类型}
\label{sec:identity-types}
\input{source/preliminaries/identity-types}

\input{source/preliminaries/notes}
\input{source/preliminaries/exercises}
% Local Variables:
% TeX-master: "hott-online"
% End: