Preface. Contents. Preliminaries. Prospectus. Logic, ty pe theory, and fibred category theory. The logic and type theory of sets . Introduction to fibred category theory. Fibrations. S ome concrete examples: sets, &ohgr;-sets and PERs. Some general examples . Cloven and split fibrations. Change-of-base and composition for fibrat ions. Fibrations of signatures. Categories of fibrations. Fibrewise stru cture and fibred adjunctions. Fibred products and coproducts. Indexed ca tegories. Simple type theory. The basic calculus of typ es and terms. Functorial semantics. Exponents, products and coproducts. Semantics of simple type theories. Semantics of the untyped lambda calcu lus as a corollary. Simple parameters. Equational logic. Logics. Specifications and theories in equational logic. Algebraic spe cifications. Fibred equality. Fibrations for equational logic. Fibred fu nctorial semantics. First order predicate logic. Signat ures, connectives and quantifiers. Fibrations for the first order predic ate logic. Functorial interpretation and internal language. Subobject fi