Publisher Summary The chapter presents correspondence between topoi and theories that makes precise Lawvere's claim that the notion of topos summarizes in objective categorical form the essence of higher-order logic. Elementary topoi turn out to correspond to the theories in a quite natural logic, formally an intuitionistic type theory. The chapter develops a part of topos theory according to Lawvere and Tierne. The development is reminiscent of algebraic logic. The Cartesian-closed structure gives certain finite types and encapsulates the fact that definable maps are closed under composition, λ-abstraction, and pairing. It has been concluded that important morphisms among topoi are geometric morphisms. Reyes has shown how a Grothendieck topos may be viewed as the extension of sets obtained by adding a generic model for a suitable (possibly infinitary) first-order theory. Geometric morphisms, then, arise naturally from a consideration of models (in Grothendieck topoi) of such theories. This approach, however, depends on some fixed base topos (in this case sets) and fails to explicate the notion of topos in abstracto.