Categorical Logic and Type Theory
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.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Introduction to fibred category theory
Simple type theory
First order predicate logic
Higher order predicate logic
The effective topos
Other editions - View all
adjunction algebra arbitrary Assume base category Beck-Chevalley Beck-Chevalley condition canonical map Cartesian closed Cartesian morphism Cartesian products category IB category theory change-of-base codomain fibration commuting comonad composition comprehension category Consider construction coproducts correspondence Dcpo define Definition dependent type theory described diagram display map effective topos Eq-fibration equaliser equations example Exercise exponents Fam(C fibred categories fibred functor finite limits Frobenius full and faithful function symbols Hence higher order logic indexed category internal category isomorphism kinds left adjoint Lemma mono natural numbers natural transformation obtained pair polymorphic type theory poset predicate logic preorder preserves products and coproducts projection Proof Prop Proposition pullback pullback square quantification quotient types result right adjoint satisfying Sets Show signature simple fibration simple type theory slice category split fibration structure subobject fibration subset types terminal object Theorem topos total category type context UFam(PER unique vertical w-Sets yields
Page 719 - A. Carboni, S. Lack, and RFC Walters. Introduction to extensive and distributive categories.
Page 725 - In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, volume 1 of Electronic Notes in Theoretical Computer Science, Tulane University, New Orleans, Louisiana, Mar.
All Book Search results »
Logics for Coalgebras and Applications to Computer Science
Limited preview - 2001