books.google.si - This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists....http://books.google.si/books/about/Categorical_logic_and_type_theory.html?hl=sl&id=0hhyL4WG3ngC&utm_source=gb-gplus-shareCategorical logic and type theory
