basics.tex

\chapter{同伦类型论}
\label{cha:basics}
\input{source/basics/basics}

\section{类型和高阶广群}
\label{sec:equality}
\input{source/basics/equality}

\section{函数是函子}
\label{sec:functors}
\input{source/basics/functors}

\section{类型族是纤维化}
\label{sec:fibrations}
\input{source/basics/fibrations}

\section{同伦和等价}
\label{sec:basics-equivalences}
\input{source/basics/basics-equivalences}

\section{类型的形成器的高维广群结构}
\label{sec:computational}
\input{source/basics/computational}

\section{笛卡尔积类型}
\label{sec:compute-cartprod}
\input{source/basics/compute-cartprod}

\section{\texorpdfstring{$\Sigma$}{Σ}-类型}
\label{sec:compute-sigma}
\input{source/basics/compute-sigma}

\section{单元类型}
\label{sec:compute-unit}
\input{source/basics/compute-unit}

\section{\texorpdfstring{$\Pi$}{Π}-类型和函数外延性公理}
\label{sec:compute-pi}
\input{source/basics/compute-pi}

\section{全集和单值公理}
\label{sec:compute-universe}
\input{source/basics/compute-universe}

\section{恒等类型}
\label{sec:compute-paths}
\input{source/basics/compute-paths}

\section{余积}
\label{sec:compute-coprod}
\input{source/basics/compute-coprod}

\section{自然数}
\label{sec:compute-nat}
\input{source/basics/compute-nat}

\section{例子: 结构的等价}
\label{sec:equality-of-structures}
\input{source/basics/equality-of-structures}

\section{泛性质}
\label{sec:universal-properties}
\input{source/basics/universal-properties}


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