Categorical logic and type theory

Content: Part 1 Prospectus: logic, type theory and fibred category theory
the logic and type theory of sets. Part 2 Introduction to fibred category theory: fibrations
some concrete examples - sets, omega-sets and PERs
some general examples
cloven split fibrations
change-of-base and composition for fibrations
fibrations of signatures
categories of fibrations
fibrewise structure and fibred adjunctions
fibred products and coproducts
indexed categories. Part 3 Simple type theory: the basic calculus of types and terms
functorial semantics
exponents, products and coproducts
semantics of simple type theories
semantics of the untyped lambda calculus as a corollary
simple parameters. Part 4 Equational logic: logics
specifications and theories in equational logic
algebraic specifications
fibred equality
fibrations for equational logic
fibred functorial semantics. Part 5 First order predicate logic: signatures, connective and quantifiers
fibrations for the first order predicate logic
functorial interpretation and internal language
subobject fibrations 1 - regular categories
subobject fibrations 2 -coherent categories and logoses
subest types
quotient types
quotient types, categorically
a logical characterization of subobject fibrations. Part 6 Higher order predicate logic: higher order signatures
generic objects
fibrations for higher order logic
elementary toposes
colimits, powerobjects and well-poweredness in topos
nuclei in a topos
separated objects and sheaves in a topos
a logical description of separated objects and sheaves. Part 7 The effective topos: constructing a topos from a higher order fibration
the effective topos and its subcategories of sets, omega-sets and PERs
families of PERs and omega-sets over the effective topos
natural numbers in the effective topos and some associated principles. Part 8 Internal category theory: definition and examples of internal categories
internal functors and natural transformations
externalization
internal diagrams and completeness. Part 9 Polymorphic type theory: syntax
use of polymorphic type theory
naive set theoretic semantics
fibrations for polymorphic type theory
small polymorphic fibrations
logic over polymorphic type theory. Part 10 Advanced fibred category theory: opfibrations and fibred spans
logical predicates and relations
quantification
category theory over a fibration
locally small fibrations
definability. Part 11 First order dependent type theory: a calculus of dependent types
use of dependent types
a term model
display maps and comprehension categories
closed comprehension categories
domain theoretic models of type dependency. Part 12 Higher order dependent type theory: dependent predicate logic
dependent predicate logic, categorically
polymorphic dependent type theory
strong and very strong sum and equality
full higher order dependent type theory
full higher order dependent type theory, categorically
completeness of the category of PERs in the