Quotient types, categorically. 290. 4.9. A logical characterisation of subobject fibrations. 304. 5. Higher order predicate logic. 311. 5.1. Higher order signatures.

88 KB – 779 Pages

PAGE – 3 ============

PAGE – 4 ============
CATEGORICAL LOGIC AND TYPE THEORY Bart JACOBS Research Fellow of the Royal Netherlands Academy of Arts and Sciences Computing Science Institute^ University of Nijmegen, P.O. Box 9010, 6500 GL Nijmegen, The Netherlands 1999 ELSEVIER AMSTERDAM Ł LAUSANNE Ł NEW YORK Ł OXFORD Ł SHANNON Ł SINGAPORE Ł TOKYO

PAGE – 5 ============
ELSEVIER SCIENCE B.V. Sara Burgerhartstraat 25 P.O. Box 211, 1000 AE Amsterdam, The Netherlands © 1999 Elsevier Science B.V.. All rights reserved. This work and the individual contributions contained in it are protected under copyright by Elsevier Science B.V., and the following terms and conditions apply to its use: Photocopying Single photocopies of single chapters may be made for personal use as allowed by national copyright laws. Permission of the publisher and payment of a fee is required for all other photocopying, including multiple or systematic copying, copying for advertising or promotional purposes, resale, and all forms of document delivery. Special rates are available for educational institutions that wish to make photocopies for non-profit educational classroom use. Permissions may be sought directly from Elsevier Science Rights & Permissions Department, PO Box 800, Oxford 0X5 IDX, UK; phone: (+44) 1865 843830, fax: (+44) 1865 853333, e-mail: permissions@elsevier.co.uk. You may also contact Rights & Permissions directly through Elsevier’s home page (http://www.elsevier.nl), selecting first ‘Customer Support’, then ‘General Information’, then ‘Permissions Query Form’. In the USA, users may clear permissions and make payments through the Copyright Clearance Center, Inc., 222 Rosewood Drive, Danvers, MA 01923, USA; phone: (978) 7508400, fax: (978) 7504744, and in the UK through the Copyright Licensing Agency Rapid Clearance Service (CLARCS), 90 Tottenham Court Road, London WIP OLP, UK; phone: (+44) 171 436 5931; fax: (+44) 171 436 3986. Other countries may have a local reprographic rights agency for payments. Derivative Works Subscribers may reproduce tables of contents for internal circulation within their institutions. Permission of the publisher is required for resale or distribution of such material outside the institution. Permission of the publisher is required for all other derivative works, including compilations and translations. Electronic Storage or Usage Permission of the publisher is required to store or use electronically any material contained in this work, including any chapter or part of a chapter. Contact the publisher at the address indicated. Except as outlined above, no part of this work may be reproduced, stored in a retrieval system or transmitted in any form or by any means, electronic, mechanical, photocopying, recording or otherwise, without prior written permission of the publisher. Address permissions requests to: Elsevier Science Rights & Permissions Department, at the mail, fax and e-mail addresses noted above. Notice No responsibility is assumed by the Publisher for any injury and/or damage to persons or property as a matter of products liability, negligence or otherwise, or from any use or operation of any methods, products, instructions or ideas contained in the material herein. Because of rapid advances in the medical sciences, in particular, independent verification of diagnoses and drug dosages should be made. First edition 1999 Library of Congress Cataloging in Publication Data A catalog record from the Library of Congress has been applied for. ISBN: 0 444 50170 3 @The paper used in this publication meets the requirements of ANSI/NISO Z39.48-1992 (Permanence of Paper). Printed in The Netherlands.

PAGE – 6 ============
Preface This book has its origins in my PhD thesis, written during the years 1988 -1991 at the University of Nijmegen, under supervision of Henk Barendregt. The thesis concerned categorical semantics of various type theories, using fibred categories. The connections with logic were not fully exploited at the time. 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 a fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists. The main part of the book was written while I was employed by NWO, the National Science Foundation in The Netherlands. First, during 1992 -1994 at the Mathematics Department of the University of Utrecht, and later during 1994 – 1996 at CWI, Center for Mathematics and Computer Science, in Amsterdam. The work was finished in Nijmegen (where it started): currently, I am employed at the Computing Science Institute of the University of Nijmegen as a Research Fellow of the Royal Netherlands Academy of Arts and Sciences. This book could not have been written without the teaching, support, encouragement, advice, criticism and help of many. It is a hopeless endeavour to list them all. Special thanks go to my friends and (former) colleagues at Nijmegen, Cambridge (UK), Utrecht and Amsterdam, but also to many colleagues in the field. The close cooperation with Thomas Streicher and Clau- dio Hermida during the years is much appreciated, and their influence can be felt throughout this work. The following persons read portions of the manuscript and provided critical feedback, or contributed in some other way: Lars Birkedal, Zinovy Diskin, Herman Geuvers, Claudio Hermida, Peter Lietz, Jose Meseguer, Jaap van Oosten, Wesley Phoa, Andy Pitts, Thomas Streicher,

PAGE – 8 ============
Contents Preface v Contents vii Preliminaries xi 0. Prospectus 1 0.1. Logic, type theory, and fibred category theory 1 0.2. The logic and type theory of sets 11 1. Introduction to fibred category theory 19 1.1. Fibrations 20 1.2. Some concrete examples: sets, ct/-sets and PERs 31 1.3. Some general examples 40 1.4. Cloven and split fibrations 47 1.5. Change-of-base and composition for fibrations 56 1.6. Fibrations of signatures 64 1.7. Categories of fibrations 72 1.8. Fibrewise structure and fibred adjunctions 80 1.9. Fibred products and coproducts 93 1.10. Indexed categories 107 2. Simple type theory 119 2.1. The basic calculus of types and terms 120 2.2. Functorial semantics 126

PAGE – 9 ============
viii Contents 2.3. Exponents, products and coproducts 133 2.4. Semantics of simple type theories 146 2.5. Semantics of the untyped lambda calculus as a corollary 154 2.6. Simple parameters 157 3. Equational Logic 169 3.1. Logics 170 3.2. Specifications and theories in equational logic 177 3.3. Algebraic specifications 183 3.4. Fibred equality 190 3.5. Fibrations for equational logic 201 3.6. Fibred functorial semantics 209 4. First order predicate logic 219 4.1. Signatures, connectives and quantifiers 221 4.2. Fibrations for first order predicate logic 232 4.3. Functorial interpretation and internal language 246 4.4. Subobject fibrations I: regular categories 256 4.5. Subobject fibrations II: coherent categories and logoses 265 4.6. Subset types 272 4.7. Quotient types 282 4.8. Quotient types, categorically 290 4.9. A logical characterisation of subobject fibrations 304 5. Higher order predicate logic 311 5.1. Higher order signatures 312 5.2. Generic objects 321 5.3. Fibrations for higher order logic 330 5.4. Elementary toposes 338 5.5. Colimits, powerobjects and well-poweredness in a topos 346 5.6. Nuclei in a topos 353 5.7. Separated objects and sheaves in a topos 360 5.8. A logical description of separated objects and sheaves 368 6. The effective topos 373 6.1. Constructing a topos from a higher order fibration 374 6.2. The effective topos and its subcategories of sets, u;-sets, and PERs . 385 6.3. Families of PERs and u;-sets over the effective topos 393 6.4. Natural numbers in the effective topos and some associated principles . . 398 7. Internal category theory , . 407 7.1. Definition and examples of internal categories 408 7.2. Internal functors and natural transformations 414 7.3. Externalisation 421 7.4. Internal diagrams and completeness 430

PAGE – 10 ============
Contents ix 8. Polymorphic type theory 441 8.1. Syntax 444 8.2. Use of polymorphic type theory 454 8.3. Naive set theoretic semantics 463 8.4. Fibrations for polymorphic type theory 471 8.5. Small polymorphic fibrations 485 8.6. Logic over polymorphic type theory 495 9. Advanced fibred category theory 509 9.1. Opfibrations and fibred spans 510 9.2. Logical predicates and relations 518 9.3. Quantification 535 9.4. Category theory over a fibration 547 9.5. Locally small fibrations 558 9.6. Definability 568 10. First order dependent type theory 581 10.1. A calculus of dependent types 584 10.2. Use of dependent types 594 10.3. A term model 601 10.4. Display maps and comprehension categories 609 10.5. Closed comprehension categories 623 10.6. Domain theoretic models of type dependency 637 11. Higher order dependent type theory 645 11.1. Dependent predicate logic 648 11.2. Dependent predicate logic, categorically 653 11.3. Polymorphic dependent type theory 662 11.4. Strong and very strong sum and equality 674 11.5. Full higher order dependent type theory 684 11.6. Full higher order dependent type theory, categorically 692 11.7. Completeness of the category of PERs in the effective topos 707 References 717 Notation Index 735 Subject Index 743

88 KB – 779 Pages