Locally cartesian closed categories and type theory

It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/A are cartesian closed. In such a category, the notion of a ‘generalized set’, for example an ‘A-indexed set’, is represented by a morphism B → A of C, i.e. by an ... View More