history.tex

\documentclass[UTF8]{ctexbook}
\usepackage[T1]{fontenc}
\usepackage[a4paper]{geometry}
\usepackage{graphicx}
\usepackage[dvipsnames]{xcolor}
\usepackage{amssymb,amsmath,amsthm}
\usepackage[lightning]{stmaryrd}
\usepackage{tcolorbox,fancyhdr,marginnote}
\usepackage{mathrsfs,verbatim,quiver}
\usepackage{biblatex}
\usepackage{hyperref}
\usepackage{fontspec}
\usepackage{minted}

% Chinese font
\setCJKmainfont{Songti SC}[
  UprightFont = Songti SC Light,
  ItalicFont = Kaiti SC,
  BoldItalicFont = Kaiti SC Bold,
]

% Load computer modern font for e.g. cyrillic.
% Referring by file name is needed
% to get compatibility on my laptop and GitHub CI.
\newfontfamily\tempfont[
  BoldFont={cmunbx.otf},
  ItalicFont={cmunti.otf},
  BoldItalicFont={cmunbi.otf},
  Ligatures=TeX
]{cmunrm.otf}

% Lightning symbols
\DeclareMathOperator\Reflect{\rotatebox[origin=c]{180}{\(\lightning\)}}
\DeclareMathOperator\Reify{\reflectbox{\(\lightning\)}}

% mathrsfs only supports a set of fixed sizes.
% Fixed by declaring myself.
\DeclareFontFamily{U}{rsfs}{\skewchar\font127 }
\DeclareFontShape{U}{rsfs}{m}{n}{%
   <-6.5> rsfs5
   <6.5-8.5> rsfs7
   <8.5-> rsfs10
}{}

% Defining some colors for hyperref
\newcommand\myshade{80}
\colorlet{mylinkcolor}{violet}
\colorlet{mycitecolor}{orange}
\colorlet{myurlcolor}{Aquamarine}

\hypersetup{
  linkcolor  = mylinkcolor!\myshade!black,
  citecolor  = mycitecolor!\myshade!black,
  urlcolor   = myurlcolor!\myshade!black,
  colorlinks = true,
}

% Small set of macros
\newcommand{\cons}[1]{\textnormal{\textsf{#1}}}
\newcommand{\slogan}[1]{\begin{center}%
  \tcbox[colback=red!10, colframe=red!80!green]{%
    \large\textbf{\heiti{#1}}%
  }%
\end{center}}
% Add a single hiragana "Yo".
\DeclareFontFamily{U}{min}{}
\DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
\newcommand{\yo}{\mathop{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}}
% op
\newcommand{\op}{^\mathrm{op}}
% Tikz \mapsto arrow
\usetikzlibrary{arrows}
\tikzset{|/.tip={Bar[width=.8ex,round]}}

% Theorems and definitions
\theoremstyle{plain}
\newtheorem{lemma}{引理}[chapter]
\newtheorem{theorem}{定理}[chapter]
\newtheorem{corollary}{推论}[chapter]
\newtheorem{example}{例}[chapter]

\theoremstyle{definition}
\newtheorem{definition}{定义}[chapter]

\theoremstyle{remark}
\newtheorem*{remark}{注}

% Bib resource
\addbibresource{history.bib}

% Page style
\pagestyle{fancy}
\fancyhead[L]{\nouppercase{\kaishu\rightmark}}
\fancyhead[R]{\nouppercase{\kaishu\leftmark}}
\setlength{\headheight}{14pt}

% Berries!
\definecolor{berry1}{RGB}{230,255,170}
\definecolor{berry2}{RGB}{255,160,126}
\definecolor{berry3}{RGB}{220,200,40}
\definecolor{berry4}{RGB}{79,53,130}
\newcommand{\berryglow}[1]{
  \begin{tikzpicture}
    \useasboundingbox (-0.5cm, -0.5cm) rectangle (0.5cm, 0.5cm);
    \draw[inner color=berry#1, draw opacity=0] (-0.6,-0.6) rectangle (0.6,0.6);
    \node at (0,0) {\includegraphics[width=1cm]{images/difficulty#1.png}};
    % Pixel size 16x16, 1000% enlarged
  \end{tikzpicture}
}
\newcommand{\berryglowinf}{
  % Secret infinity category berry
  \begin{tikzpicture}
    \useasboundingbox (-0.5cm, -0.5cm) rectangle (0.8cm, 0.5cm);
    \draw[inner color=berry3, draw opacity=0] (-0.7,-0.7) rectangle (0.7,0.7);
    \node at (0,0) {\includegraphics[width=2.5cm]{images/infinity.png}};
    \node[font=\normalsize] at (0,0.7) {\(\infty\)};
    % This one has a text so we need to ensure size
    % Pixel size 40x24, 1000% enlarged
  \end{tikzpicture}
}
\newcommand{\berry}[1]{\marginnote[%
  \hfill%
  \berryglow{#1}%
]{%
  \berryglow{#1}%
  \hfill%
}}
\newcommand{\berryinf}{\marginnote[%
  \hfill%
  \berryglowinf%
]{%
  \berryglowinf%
  \hfill%
}}

\begin{document}
%%% Title Page
\thispagestyle{empty}
\vspace*{\fill}
\begin{flushright}
\zihao{0}\heiti 类型论简史\\
\Large\sf A Brief History of Type Theory\\
\vspace{1em}
\LARGE\sf Trebor
\end{flushright}
% A nice cover picture
\begin{tikzpicture}[xscale=-3.6, yscale=3.5,
  every node/.style={font=\large}]
\useasboundingbox (-1.3, -0.3) rectangle (1.8, 4);
\node (A) at (0,0) {\((((\bullet\bullet)\bullet)\bullet)\bullet\)};
\node (B) at (-1, 1) {\(((\bullet\bullet)\bullet)(\bullet\bullet)\)};
\node (C) at (0,1) {\(((\bullet(\bullet\bullet))\bullet)\bullet\)};
\node (D) at (0.5, 1.5) {\((\bullet((\bullet\bullet)\bullet))\bullet\)};
\node (E) at (1, 2) {\((\bullet(\bullet(\bullet\bullet)))\bullet\)};
\node (F) at (1.5, 1.5) {\(((\bullet\bullet)(\bullet\bullet))\bullet\)};
\node (G) at (-1, 2) {\((\bullet(\bullet\bullet))(\bullet\bullet)\)};
\node (H) at (-0.5, 2.5) {\(\bullet(((\bullet\bullet)\bullet)\bullet)\)};
\node (I) at (1.5, 2.5) {\((\bullet\bullet)((\bullet\bullet)\bullet)\)};
\node (J) at (-1, 3) {\(\bullet((\bullet\bullet)(\bullet\bullet))\)};
\node (K) at (0, 3) {\(\bullet((\bullet(\bullet\bullet)\bullet))\)};
\node (L) at (0.5, 3.5) {\(\bullet(\bullet((\bullet\bullet)\bullet))\)};
\node (M) at (1.5, 3.5) {\((\bullet\bullet)(\bullet(\bullet\bullet))\)};
\node (N) at (0.5, 4.5) {\(\bullet(\bullet(\bullet(\bullet\bullet)))\)};
\draw[black!40!white, line width=2.4pt]
  (B) -- (M);
\draw[ultra thick, double=gray, draw=white, double distance=2pt]
  (A) -- (B) (A) -- (C) (A) -- (F)
  (B) -- (G)
  (C) -- (D) (C) -- (G)
  (D) -- (E) (D) -- (H)
  (E) -- (K)
  (F) -- (E) (F) -- (I)
  (G) -- (J)
  (H) -- (J) (H) -- (K)
  (I) -- (L) (I) -- (M)
  (J) -- (N)
  (K) -- (L)
  (L) -- (N)
  (M) -- (N);
\end{tikzpicture}
\newpage
%%% Epigraph
\thispagestyle{empty}
\vspace*{0.2\pdfpageheight}
\begin{quotation}\sf
Category theory implements the relative point of
view by means of \emph{slice categories}; but this
language is greatly obfuscated in comparison to
the simplicity of working with non-relative
objects. The goal of type theory is to reconcile
the expressivity of the relative point of view
with the simplicity of the global point of view,
by providing a language that makes movement
between different slices (base change) seamless.
\begin{flushright}\rm
J. Sterling, \emph{Towards a geometry for syntax}.~\cite{sterling:2023:geometry}
\end{flushright}
\end{quotation}
\newpage
%%% Table of contents
\pagenumbering{roman}
\setcounter{tocdepth}{1}
\tableofcontents
\cleardoublepage
%%% Body matter
\pagenumbering{arabic}
% \ziju{0.1}
% \baselineskip=20pt
\include{chapters/introduction.tex}
\include{chapters/beginnings.tex}
\include{chapters/curry-howard.tex}
\include{chapters/martin-lof.tex}
\include{chapters/category.tex}
\include{chapters/hott.tex}
\include{chapters/prospect.tex}

\emergencystretch=1em
\printbibliography[title=参考文献]
\end{document}