Locally cartesian closed categories and type theory
scientific article