\contentsline {chapter}{Preface}{i}{chapter*.1}%
\contentsline {chapter}{\numberline {0}Introduction}{3}{chapter.0}%
\contentsline {section}{\numberline {0.1}Appetizer: inverses in group objects}{3}{section.0.1}%
\contentsline {section}{\numberline {0.2}On syntax and free objects}{9}{section.0.2}%
\contentsline {section}{\numberline {0.3}On type theory and category theory}{13}{section.0.3}%
\contentsline {section}{\numberline {0.4}Expectations of the reader}{17}{section.0.4}%
\contentsline {chapter}{\numberline {1}Unary type theories}{19}{chapter.1}%
\contentsline {section}{\numberline {1.1}Posets}{19}{section.1.1}%
\contentsline {section}{\numberline {1.2}Categories}{23}{section.1.2}%
\contentsline {subsection}{\numberline {1.2.1}Primitive cuts}{24}{subsection.1.2.1}%
\contentsline {subsection}{\numberline {1.2.2}Cut admissibility}{28}{subsection.1.2.2}%
\contentsline {section}{\numberline {1.3}Meet-semilattices}{37}{section.1.3}%
\contentsline {subsection}{\numberline {1.3.1}Sequent calculus for meet-semilattices}{38}{subsection.1.3.1}%
\contentsline {subsection}{\numberline {1.3.2}Natural deduction for meet-semilattices}{41}{subsection.1.3.2}%
\contentsline {section}{\numberline {1.4}Categories with products}{44}{section.1.4}%
\contentsline {section}{\numberline {1.5}Categories with coproducts}{52}{section.1.5}%
\contentsline {section}{\numberline {1.6}Universal properties and modularity}{57}{section.1.6}%
\contentsline {section}{\numberline {1.7}Presentations and theories}{59}{section.1.7}%
\contentsline {subsection}{\numberline {1.7.1}Group presentations}{59}{subsection.1.7.1}%
\contentsline {subsection}{\numberline {1.7.2}Category presentations}{61}{subsection.1.7.2}%
\contentsline {subsection}{\numberline {1.7.3}$\times $-presentations}{62}{subsection.1.7.3}%
\contentsline {subsection}{\numberline {1.7.4}Theories}{70}{subsection.1.7.4}%
\contentsline {chapter}{\numberline {2}Simple type theories}{79}{chapter.2}%
\contentsline {section}{\numberline {2.1}Towards multicategories}{79}{section.2.1}%
\contentsline {section}{\numberline {2.2}Introduction to multicategories}{82}{section.2.2}%
\contentsline {section}{\numberline {2.3}Multiposets and monoidal posets}{86}{section.2.3}%
\contentsline {subsection}{\numberline {2.3.1}Multiposets}{86}{subsection.2.3.1}%
\contentsline {subsection}{\numberline {2.3.2}Sequent calculus for monoidal posets}{88}{subsection.2.3.2}%
\contentsline {subsection}{\numberline {2.3.3}Natural deduction for monoidal posets}{91}{subsection.2.3.3}%
\contentsline {section}{\numberline {2.4}Multicategories and monoidal categories}{93}{section.2.4}%
\contentsline {subsection}{\numberline {2.4.1}Multicategories}{93}{subsection.2.4.1}%
\contentsline {subsection}{\numberline {2.4.2}Monoidal categories}{97}{subsection.2.4.2}%
\contentsline {section}{\numberline {2.5}Adding products and coproducts}{101}{section.2.5}%
\contentsline {section}{\numberline {2.6}Some generalized multicategories}{105}{section.2.6}%
\contentsline {section}{\numberline {2.7}Intuitionistic logic}{110}{section.2.7}%
\contentsline {subsection}{\numberline {2.7.1}\ensuremath {\mathfrak {S}}\xspace -monoidal lattices}{110}{subsection.2.7.1}%
\contentsline {subsection}{\numberline {2.7.2}Heyting algebras}{114}{subsection.2.7.2}%
\contentsline {subsection}{\numberline {2.7.3}Natural deduction and logic}{116}{subsection.2.7.3}%
\contentsline {section}{\numberline {2.8}Simply typed $\ensuremath {\your@lambda }\xspace $-calculus}{123}{section.2.8}%
\contentsline {section}{\numberline {2.9}Cartesian presentations}{130}{section.2.9}%
\contentsline {subsection}{\numberline {2.9.1}Finite-product theories}{130}{subsection.2.9.1}%
\contentsline {subsection}{\numberline {2.9.2}Presheaves on multicategories}{133}{subsection.2.9.2}%
\contentsline {section}{\numberline {2.10}Symmetric monoidal categories}{136}{section.2.10}%
\contentsline {subsection}{\numberline {2.10.1}Shuffles}{136}{subsection.2.10.1}%
\contentsline {subsection}{\numberline {2.10.2}Symmetric $\tensor $-presentations}{140}{subsection.2.10.2}%
\contentsline {chapter}{\numberline {3}Classical type theories}{151}{chapter.3}%
\contentsline {section}{\numberline {3.1}Props and symmetric monoidal categories}{151}{section.3.1}%
\contentsline {section}{\numberline {3.2}Cyclic multicategories and cosubunary polycategories}{162}{section.3.2}%
\contentsline {section}{\numberline {3.3}Classical logic}{163}{section.3.3}%
\contentsline {section}{\numberline {3.4}Polycategories and linear logic}{163}{section.3.4}%
\contentsline {chapter}{\numberline {4}First-order logic}{165}{chapter.4}%
\contentsline {section}{\numberline {4.1}Predicate logic}{165}{section.4.1}%
\contentsline {subsection}{\numberline {4.1.1}Structural rules and simple rules}{166}{subsection.4.1.1}%
\contentsline {subsection}{\numberline {4.1.2}The universal quantifier}{168}{subsection.4.1.2}%
\contentsline {subsection}{\numberline {4.1.3}The existential quantifier}{170}{subsection.4.1.3}%
\contentsline {subsection}{\numberline {4.1.4}Equality}{172}{subsection.4.1.4}%
\contentsline {subsection}{\numberline {4.1.5}First-order theories}{173}{subsection.4.1.5}%
\contentsline {subsection}{\numberline {4.1.6}Natural deduction}{175}{subsection.4.1.6}%
\contentsline {section}{\numberline {4.2}First-order hyperdoctrines}{179}{section.4.2}%
\contentsline {section}{\numberline {4.3}Hyperdoctrines of subobjects}{188}{section.4.3}%
\contentsline {subsection}{\numberline {4.3.1}Horn hyperdoctrines from finite limits}{188}{subsection.4.3.1}%
\contentsline {subsection}{\numberline {4.3.2}Regular categories}{189}{subsection.4.3.2}%
\contentsline {subsection}{\numberline {4.3.3}Coherent categories}{194}{subsection.4.3.3}%
\contentsline {subsection}{\numberline {4.3.4}Heyting categories}{195}{subsection.4.3.4}%
\contentsline {section}{\numberline {4.4}Comprehension}{198}{section.4.4}%
\contentsline {section}{\numberline {4.5}Finite-limit theories}{201}{section.4.5}%
\contentsline {section}{\numberline {4.6}Indexed monoidal categories}{201}{section.4.6}%
\contentsline {chapter}{\numberline {A}Deductive systems}{207}{appendix.A}%
\contentsline {section}{\numberline {A.1}Trees and free algebras}{207}{section.A.1}%
\contentsline {section}{\numberline {A.2}Indexed trees}{209}{section.A.2}%
\contentsline {section}{\numberline {A.3}Free algebras with axioms}{210}{section.A.3}%
\contentsline {section}{\numberline {A.4}Rules and deductive systems}{212}{section.A.4}%
\contentsline {section}{\numberline {A.5}Terms}{213}{section.A.5}%
\contentsline {section}{\numberline {A.6}Variable binding and $\ensuremath {\your@alpha }\xspace $-equivalence}{216}{section.A.6}%