main.tex

% !TEX program = xelatex
% !TEX options = -synctex=1 -interaction=nonstopmode -file-line-error --shell-escape "%DOC%"

%----------------------------------------------------------------------------------------
%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
%----------------------------------------------------------------------------------------

\documentclass[
  fontsize=10pt,
  twoside=false
  % overfullrule
]{kaobook}

% Choose the language
% \usepackage[french,english]{babel} % Load characters and hyphenation
\usepackage[english=british]{csquotes}	% English quotes

\frenchsetup{PartNameFull=false}

% Load the bibliography package
\usepackage{styles/kaobiblio}
\addbibresource{main.bib} % Bibliography file

% Load mathematical packages for theorems and related environments. NOTE: choose only one between 'mdftheorems' and 'plaintheorems'.
\usepackage{styles/mdftheorems}
%\usepackage{styles/plaintheorems}

\graphicspath{{images/}} % Paths in which to look for images

\makeindex[columns=3, title=Alphabetical Index, intoc] % Make LaTeX produce the files required to compile the index

\makeglossaries % Make LaTeX produce the files required to compile the glossary

\makenomenclature % Make LaTeX produce the files required to compile the nomenclature

% Reset sidenote counter at chapters
%\counterwithin*{sidenote}{chapter}

%%% Then my own packages

\usepackage{fontspec}

\usepackage{mathpartir}

% Trick for current font size
\makeatletter
\newcommand{\currentfontsize}{\fontsize{\f@size}{\f@baselineskip}\selectfont}
\makeatother

% For code highlighting
\usepackage{minted}
\setminted{
	fontsize=\footnotesize,
	encoding=utf8
}
\setmintedinline{fontsize=\currentfontsize}

% HACK: Remove red boxes
% From https://tex.stackexchange.com/questions/343494/minted-red-box-around-greek-characters
\usepackage{etoolbox,xpatch}

\makeatletter
\AtBeginEnvironment{minted}{\dontdofcolorbox}
\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}
\xpatchcmd{\inputminted}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}
\xpatchcmd{\mintinline}{\minted@fvset}{\minted@fvset\dontdofcolorbox}{}{}
\makeatother

% Without red boxes: xcode, arduino, abap,
% \usemintedstyle{abap}

\usepackage{stmaryrd}

% Miniature document
% \usepackage{minidocument}
% \def\minidocumentscale{0.25}
% \usepackage{blindtext}

% Tikz
\usetikzlibrary{
  tikzmark,
  arrows,
  arrows.meta,
  decorations.pathmorphing,
  positioning
}

% Tikz styles
\tikzstyle{tred} = [-{Triangle[open]}]
% \tikzstyle{arrow} = [thick,->,>=stealth]
\tikzstyle{barrow} = [->, bend angle=40]

% https://tex.stackexchange.com/questions/88949/curved-waved-lines-with-tikz
\tikzset{sim/.style={decorate, decoration={coil, aspect = 0, segment length = 0.9cm, pre = moveto, post = moveto}}}

% https://tex.stackexchange.com/questions/104119/star-next-to-arrowhead-in-tikz
\tikzset{
    to*/.style = {
        shorten >=.25em,#1-to,
        to path = {-- node[inner sep=0pt,at end,sloped] {${}^\star$} (\tikztotarget) \tikztonodes}
    },
    to*/.default=
}

\tikzset{
    *to/.style = {
        shorten >=.25em,#1-to,
        to path = {-- node[inner sep=0pt,at end,sloped] {${}_\star$} (\tikztotarget) \tikztonodes}
    },
    *to/.default=
}

\RequirePackage{epigraph} % \cleartoevenpage

\include{macros}
\input{cpp-macros} % TODO Integrate into macros and factorise

% Customising margin citations
\renewcommand{\formatmargincitation}[1]{%
	\color{Gray!80} \parencite{#1}: \citeauthor*{#1} (\citeyear{#1}), \citetitle{#1}\\%
}

% Font fallback
\usepackage{newunicodechar}
\newfontfamily{\fallbackmonofont}{Symbola}[Scale=MatchLowercase]
\DeclareTextFontCommand{\textfallbackmono}{\fallbackmonofont}
\newcommand{\fallbackcharmono}[2][\textfallbackmono]{%
    \newunicodechar{#2}{#1{#2}}%
}
% \fallbackcharmono{⊗}
\fallbackcharmono{⊩}
\fallbackcharmono{⨶}
\fallbackcharmono{⊨}
\fallbackcharmono{⨷}
% \fallbackcharmono{⊕}
% \fallbackcharmono{∘}
% \fallbackcharmono{∀}

\newfontfamily{\dejavusansfont}{DejaVu Sans}[Scale=MatchLowercase]
\DeclareTextFontCommand{\textfallbackdejavusans}{\dejavusansfont}
\newcommand{\fallbackchardejavusans}[2][\textfallbackdejavusans]{%
    \newunicodechar{#2}{#1{#2}}%
}
\fallbackchardejavusans{ᵗ}
\fallbackchardejavusans{∘}
\fallbackchardejavusans{∀}
% \fallbackchardejavusans{⟦}
% \fallbackchardejavusans{⟧}
% \fallbackchardejavusans{∈}

\newfontfamily{\dejavusansmonofont}{DejaVu Sans Mono}[Scale=MatchLowercase]
\DeclareTextFontCommand{\textfallbackdejavusansmono}{\dejavusansmonofont}
\newcommand{\fallbackchardejavusansmono}[2][\textfallbackdejavusansmono]{%
    \newunicodechar{#2}{#1{#2}}%
}
% \fallbackchardejavusansmono{∈}
\fallbackchardejavusansmono{⟦}
\fallbackchardejavusansmono{⟧}
\fallbackchardejavusansmono{⊢}

\newfontfamily{\firamathfont}{Fira Math}[Scale=MatchLowercase]
\DeclareTextFontCommand{\textfallbackfiramath}{\firamathfont}
\newcommand{\fallbackcharfiramath}[2][\textfallbackfiramath]{%
    \newunicodechar{#2}{#1{#2}}%
}
\fallbackcharfiramath{∈}
% \fallbackcharfiramath{⊢}
% \fallbackcharfiramath{∘}
\fallbackcharfiramath{⊗}
\fallbackcharfiramath{⊕}
% \fallbackcharfiramath{∀}
\fallbackcharfiramath{∥}

% Allow arrays in mathpar, use this command instead of \\ in array
\makeatletter
\def\arcr{\@arraycr}
\makeatother

%----------------------------------------------------------------------------------------

\begin{document}

% XeLaTeX tikzmark fix
% Coutesy of https://tex.stackexchange.com/questions/364498/tikz-offsets-origin-when-compiled-in-xelatex-as-compared-to-pdflatex
\makeatletter
\def\pgfsys@hboxsynced#1{%
  {%
    \pgfsys@beginscope%
    \setbox\pgf@hbox=\hbox{%
      \hskip\pgf@pt@x%
      \raise\pgf@pt@y\hbox{%
        \pgf@pt@x=0pt%
        \pgf@pt@y=0pt%
        \special{pdf: content q}%
        \pgflowlevelsynccm%
        \pgfsys@invoke{q -1 0 0 -1 0 0 cm}%
        \special{pdf: content -1 0 0 -1 0 0 cm q}% translate to original coordinate system
        \pgfsys@invoke{0 J [] 0 d}% reset line cap and dash
        \wd#1=0pt%
        \ht#1=0pt%
        \dp#1=0pt%
        \box#1%
        \pgfsys@invoke{n Q Q Q}%
      }%
      \hss%
    }%
    \wd\pgf@hbox=0pt%
    \ht\pgf@hbox=0pt%
    \dp\pgf@hbox=0pt%
    \pgfsys@hbox\pgf@hbox%
    \pgfsys@endscope%
  }%
}
\makeatother

\setmainfont[
	Ligatures=TeX,
	% UprightFont = ,
	ItalicFont = Fira Sans Light Italic,
	% SmallCapsFont = ,
	BoldFont = Fira Sans,
	BoldItalicFont = Fira Sans Italic
]{Fira Sans Light}
% \setsansfont[Ligatures=TeX]{Fira Sans}
\setmonofont[Ligatures=TeX]{Fira Mono}

%----------------------------------------------------------------------------------------
%	BOOK INFORMATION
%----------------------------------------------------------------------------------------

% \titlehead{Some text}
\subject{PhD Thesis}

\title{Formalisation and Meta-Theory of Type Theory}
% \subtitle{Customise this page according to your needs}

\author{Théo Winterhalter}

\date{}

% \publishers{Supervised by Nicolas Tabareau and Matthieu Sozeau}

%----------------------------------------------------------------------------------------

\frontmatter % Denotes the start of the pre-document content, uses roman numerals

%----------------------------------------------------------------------------------------
%	OPENING PAGE
%----------------------------------------------------------------------------------------

%\makeatletter
%\extratitle{
%	% In the title page, the title is vspaced by 9.5\baselineskip
%	\vspace*{9\baselineskip}
%	\vspace*{\parskip}
%	\begin{center}
%		% In the title page, \huge is set after the komafont for title
%		\usekomafont{title}\huge\@title
%	\end{center}
%}
%\makeatother

%----------------------------------------------------------------------------------------
%	COPYRIGHT PAGE
%----------------------------------------------------------------------------------------

% \makeatletter
% \uppertitleback{\@titlehead} % Header

% \lowertitleback{
% 	\textbf{Disclaimer}\\
% 	You can edit this page to suit your needs. For instance, here we have a no copyright statement, a colophon and some other information. This page is based on the corresponding page of Ken Arroyo Ohori's thesis, with minimal changes.

% 	\medskip

% 	\textbf{No copyright}\\
% 	\cczero\ This book is released into the public domain using the CC0 code. To the extent possible under law, I waive all copyright and related or neighbouring rights to this work.

% 	To view a copy of the CC0 code, visit: \\\url{http://creativecommons.org/publicdomain/zero/1.0/}

% 	\medskip

% 	\textbf{Colophon} \\
% 	This document was typeset with the help of \href{https://sourceforge.net/projects/koma-script/}{\KOMAScript} and \href{https://www.latex-project.org/}{\LaTeX} using the \href{https://github.com/fmarotta/kaobook/}{kaobook} class.

% 	The source code of this book is available at:\\\url{https://github.com/fmarotta/kaobook}

% 	(You are welcome to contribute!)

% 	\medskip

% 	\textbf{Publisher} \\
% 	First printed in May 2019 by \@publishers
% }
% \makeatother

%----------------------------------------------------------------------------------------
%	DEDICATION
%----------------------------------------------------------------------------------------

% \dedication{
% 	Figure something to put here or remove it altogether.\\
% 	\flushright -- Myself
% }

%----------------------------------------------------------------------------------------
%	OUTPUT TITLE PAGE AND PREVIOUS
%----------------------------------------------------------------------------------------

% Note that \maketitle outputs the pages before here

% If twoside=false, \uppertitleback and \lowertitleback are not printed
% To overcome this issue, we set twoside=semi just before printing the title pages, and set it back to false just after the title pages
\KOMAoptions{twoside=semi}
\includepdf{import/cover}
\maketitle
\KOMAoptions{twoside=false}

%----------------------------------------------------------------------------------------
%	PREFACE
%----------------------------------------------------------------------------------------

%\input{chapters/preface.tex}
\input{chapters/ack.tex}
\pagelayout{margin} % Restore margins
\input{chapters/how-to-read.tex}
\input{chapters/french.tex}
\pagelayout{wide} % No margins

%----------------------------------------------------------------------------------------
%	TABLE OF CONTENTS & LIST OF FIGURES/TABLES
%----------------------------------------------------------------------------------------

\begingroup % Local scope for the following commands

% Define the style for the TOC, LOF, and LOT
%\setstretch{1} % Uncomment to modify line spacing in the ToC
%\hypersetup{linkcolor=blue} % Uncomment to set the colour of links in the ToC
\setlength{\textheight}{23cm} % Manually adjust the height of the ToC pages

% Turn on compatibility mode for the etoc package
\etocstandarddisplaystyle % "toc display" as if etoc was not loaded
\etocstandardlines % "toc lines as if etoc was not loaded

% Add link to TOC
\addtocontents{toc}{\protect\hypertarget{toc}{}}

\tableofcontents % Output the table of contents

% \listoffigures % Output the list of figures

% % Comment both of the following lines to have the LOF and the LOT on different pages
% \let\cleardoublepage\bigskip
% \let\clearpage\bigskip

% \listoftables % Output the list of tables

\endgroup

%----------------------------------------------------------------------------------------
%	MAIN BODY
%----------------------------------------------------------------------------------------

\mainmatter % Denotes the start of the main document content, resets page numbering and uses arabic numbers

\setchapterstyle{kao} % Choose the default chapter heading style

\input{chapters/introduction.tex}

\pagelayout{wide} % No margins
\addpart{Proofs, Types and Programs}
\pagelayout{margin} % Restore margins

\input{chapters/proof-theory.tex}
\input{chapters/simple-types.tex}
\input{chapters/dependent-types.tex}
\input{chapters/usual-defs.tex}
\input{chapters/flavours.tex}
\input{chapters/desirable-props.tex}
\input{chapters/models.tex}
\input{chapters/formalisation.tex}
\input{chapters/translations.tex}

\pagelayout{wide} % No margins
\addpart{Elimination of Reflection}
\labpart{elim-reflection}
\pagelayout{margin} % Restore margins

\input{chapters/elim-reflection-intro.tex}
\input{chapters/elim-reflection-framework.tex}
\input{chapters/elim-rel.tex}
\input{chapters/elim-trans.tex}
\input{chapters/elim-hott.tex}
\input{chapters/elim-formalised.tex}
\input{chapters/elim-conclusion.tex}

\pagelayout{wide} % No margins
\addpart{A verified type-checker for \Coq, in \Coq}
\labpart{coq-in-coq}
\pagelayout{margin} % Restore margins

\input{chapters/coq-overiew.tex}
\input{chapters/coq-spec.tex}
\input{chapters/coq-meta-theory.tex}
\input{chapters/coq-orders.tex}
\input{chapters/coq-positions.tex}
\input{chapters/coq-reduction.tex}
\input{chapters/coq-conversion.tex}
\input{chapters/coq-inference.tex}

% \appendix % From here onwards, chapters are numbered with letters, as is the appendix convention

% \pagelayout{wide} % No margins
% \addpart{Appendix}
% \pagelayout{margin} % Restore margins

% \input{chapters/appendix}

%----------------------------------------------------------------------------------------

\backmatter % Denotes the end of the main document content
\setchapterstyle{plain} % Output plain chapters from this point onwards

\pagelayout{margin} % Restore margins
\input{chapters/conclusions.tex}
\pagelayout{wide} % No margins

%----------------------------------------------------------------------------------------
%	BIBLIOGRAPHY
%----------------------------------------------------------------------------------------

% The bibliography needs to be compiled with biber using your LaTeX editor, or on the command line with 'biber main' from the template directory

\defbibnote{bibnote}{\label{bib}Here are the references in citation order.\par\bigskip} % Prepend this text to the bibliography
\printbibliography[heading=bibintoc, title=Bibliography, prenote=bibnote] % Add the bibliography heading to the ToC, set the title of the bibliography and output the bibliography note

%----------------------------------------------------------------------------------------
%	NOMENCLATURE
%----------------------------------------------------------------------------------------

% The nomenclature needs to be compiled on the command line with 'makeindex main.nlo -s nomencl.ist -o main.nls' from the template directory

\nomenclature{$\isjg{\Gamma}{J}$}{Judgment in some type theory (often \acrshort{ITT} or \Coq)}
\nomenclature{$\xisjg{\Gamma}{J}$}{Judgment in \acrshort{ETT}}

\renewcommand{\nomname}{Notation} % Rename the default 'Nomenclature'
\renewcommand{\nompreamble}{The next list describes several symbols that will be later used within the body of the document.} % Prepend this text to the nomenclature

\printnomenclature % Output the nomenclature

%----------------------------------------------------------------------------------------
%	GLOSSARY
%----------------------------------------------------------------------------------------

% The glossary needs to be compiled on the command line with 'makeglossaries main' from the template directory

\newglossaryentry{computer}{
	name=computer,
	description={is a programmable machine that receives input, stores and manipulates data, and provides output in a useful format}
}

% Glossary entries (used in text with e.g. \acrfull{fpsLabel} or \acrshort{fpsLabel})
\newacronym[longplural={Frames per Second}]{fpsLabel}{FPS}{Frame per Second}
\newacronym[longplural={Tables of Contents}]{tocLabel}{TOC}{Table of Contents}
\newacronym[longplural={Extensional Type Theories}]{ETT}{ETT}{Extensional Type Theory}
\newacronym{ITT}{ITT}{Intensional Type Theory}
\newacronym{WTT}{WTT}{Weak Type Theory}
\newacronym[longplural={Pure Type Systems}]{PTS}{PTS}{Pure Type System}
\newacronym{PCUIC}{PCUIC}{Predicative Calculus of Cumulative Inductive Constructions}
\newacronym{CoC}{CoC}{Calculus of Constructions}
\newacronym{CIC}{CIC}{Calculus of Inductive Constructions}
\newacronym{MLTT}{MLTT}{Martin-Löf Type Theory}
\newacronym{UIP}{UIP}{Uniqueness of Identity Proofs}
\newacronym{funext}{funext}{functional extensionality}
\newacronym{JMeq}{JMeq}{John Major equality}
\newacronym{LEM}{LEM}{Law of Excluded Middle}
\newacronym{HoTT}{HoTT}{Homotopy Type Theory}
\newacronym{CubicalTT}{CubicalTT}{Cubical Type Theory}
\newacronym{2WTT}{2WTT}{2-level Weak Type Theory}
\newacronym[longplural={2-level Type Theories}]{2TT}{2TT}{2-level Type Theory}
\newacronym{HTS}{HTS}{Homotopy Type System}
\newacronym{CoqMT}{CoqMT}{Coq Modulo Theory}
\newacronym{OTT}{OTT}{Observational Type Theory}
\newacronym{STT}{STT}{Setoid Type Theory}
\newacronym{TCB}{TCB}{Trusted Code Base}
\newacronym{TTB}{TTB}{Trusted Theory Base}
\newacronym{CbV}{CbV}{Call by Value}
\newacronym{STL}{STL}{Simply Typed \(\lambda\)-calculus}
\newacronym[longplural={Quotient Inductive Types}]{QIT}{QIT}{Quotient Inductive Type}
\newacronym[longplural={Categories with Families}]{CwF}{CwF}{Category with Families}
\newacronym{HOAS}{HOAS}{Higher Order Abstract Syntax}
\newacronym{HOL}{HOL}{Higher Order Logic}
\newacronym{BNF}{BNF}{Backus--Naur Form}

\setglossarystyle{listgroup} % Set the style of the glossary (see https://en.wikibooks.org/wiki/LaTeX/Glossary for a reference)
\printglossary[title=Special Terms, toctitle=List of Terms] % Output the glossary, 'title' is the chapter heading for the glossary, toctitle is the table of contents heading

%----------------------------------------------------------------------------------------
%	INDEX
%----------------------------------------------------------------------------------------

% The index needs to be compiled on the command line with 'makeindex main' from the template directory

\printindex % Output the index

%----------------------------------------------------------------------------------------
%	BACK COVER
%----------------------------------------------------------------------------------------

% If you have a PDF/image file that you want to use as a back cover, uncomment the following lines

% \clearpage
% \thispagestyle{empty}
% \null%
% \clearpage
\cleartoevenpage[\thispagestyle{empty}]
\includepdf[pages={2}]{import/cover}

%----------------------------------------------------------------------------------------


\end{document}