Jacobs B. — Categorical Logic and Type Theory :: Электронная библиотека попечительского совета мехмата МГУ

Главная Ex Libris Книги Журналы Статьи Серии Каталог Wanted Загрузка ХудЛит Справка Поиск по индексам Поиск Форум

Авторизация

Поиск по указателям

Jacobs B. — Categorical Logic and Type Theory

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Categorical Logic and Type Theory

Автор: Jacobs B.

Аннотация:

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.

Язык:

Рубрика: Computer science/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Издание: 1st edition

Год издания: 1999

Количество страниц: 760

Добавлена в каталог: 02.07.2008

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

Предметный указатель

Above      26 28
Abstraction condition      479
Action of an internal diagram      431 564
Action of an internal diagram, monoid      70
Adjunction      xiv
Adjunction in $Fib(\mathbb{B})$       84
Adjunction in Fib      93
Adjunction, fibred      83
Adjunction, fibred, split      84
Adjunction, internal      418
Adjunction, map of -s      89
Adjunction, map of -s, pseudo      91
Adjunction, semi-      157 454
Admissible subset of a complete lattice      300
Admissible subset of a directed complete partial order      203
ALF      582 598
Algebra      7
Algebra of a functor      161
Algebra of a monad      80 433
Algebra of a signature      66
Algebra of a signature with predicates      235
Algebra, boolean      xvi 167 242
Algebra, cylindric      242
Algebra, Heyting      xvi
Algebra, partial      132 189
Almost epic      358
Almost equivalence relation      384 390
Almost monic      358
Ambient category      409
Arrow category      28
Arrow fibration in $Fib(\mathbb{B})$       551
Arrow fibration in Fib      555
Arrow object in $Fib(\mathbb{B})$       549
Arrow object in Fib      553
AUTOMATH      582 598
Axiom of Choice      47 50 106 708
Axiom of Choice in a fibration      271
Axiom of Choice in a regular category      271
Axiom of Choice in dependent type theory      596 600
Axiom of choice, countable      405
Axiom rule      172
BA      see “Boolean algebra”
Balanced category      345
Beck — Chevalley condition      86 88 94 97 191
Bicartesian closed category      143
BiCCC      see “Bicartesian closed category”
Bidense morphism      358 365
Bifibration      511 512 521
Bisimulation      532
Boolean algebra      xvi 167 242
Bounded family of finite sets      572
Bounded family of partial equivalence relations      579
Brouwer — Heyting — Kolmogorov interpretation      137 596
Calculus of constructions      647 684
Calculus of constructions, extended      691
Calculus of inductive definitions      691
Calculus of predicates      663
Calculus, $\lambda$ -      xv
Calculus, $\lambda1$ -      134
Calculus, $\lambda1_{(\times,+)}$ -      140
Calculus, $\lambda1_{\times}$ -      138
Calculus, $\lambda2$ -      446
Calculus, $\lambda\omega$ -      448
Calculus, $\lambda\rightarrow$ -      446
Canonical quotient map      292
Carrier of a co-algebra of a functor      161
Carrier of an algebra of a functor      161
Carrier of an algebra of a signature      66
Cartesian closed category      xii
Cartesian closed fibration      81 426
Cartesian closed internal category      419
Cartesian closed, locally      39 81 343 564 583 627 702
Cartesian closed, relatively      610 623
Cartesian functor      74
Cartesian lifting      27
Cartesian morphism      27
Cartesian morphism, weak      30
Cartesian product      xiii
Cartesian product in a fibration (in $Fib(\mathbb{B})$ )      520
Cartesian product in a fibration (in Fib)      93 471 520
Cartesian product type      138
Cartesian product, internal      418 429
Category (fibred) over      27
Category with families      622
Category, $\lambda$ -      155
Category, $\lambda$ -, non-extensional      157
Category, $\lambda1$ -      149 566
Category, ambient      409
Category, arrow      28
Category, base      26
Category, classifying of a signature      124
Category, classifying of an algebraic specification      185
Category, classifying, $\lambda1$ -      135
Category, classifying, $\lambda1_{\times}$ -      139
Category, coherent      266
Category, comma      55 57 79 515 548
Category, complete      102
Category, comprehension      539 583 613
Category, comprehension over a fibration      666
Category, comprehension with unit      616
Category, comprehension, closed      625 715
Category, comprehension, family      618 636
Category, comprehension, full      613
Category, comprehension, identity      614 627 637
Category, comprehension, regular subobject      683
Category, comprehension, simple      614 627
Category, comprehension, subobject      614 683
Category, D-      274
Category, display map      610
Category, distributive      63 323 522
Category, Eilenberg — Moore      46
Category, Eilenberg — Moore, fibred      80
Category, exact      297
Category, extensive      62
Category, fibre      26
Category, fibred      27
Category, indexed      50
Category, indexed, opposite      112
Category, indexed, split      51
Category, internal      7 10 408
Category, internal, Cartesian closed      419 426
Category, internal, discrete      411 429 434
Category, internal, finite      411
Category, internal, full      412 423 424 429 470 490 492 564 614 701 702
Category, internal, full, in a fibration      563
Category, internal, indiscrete      421
Category, internal, preorder      414
Category, Kleisli      46 80 117 130 205 494
Category, Kleisli, fibred      80 494
Category, locally small      xiii 4 428 558
Category, logical      266
Category, opposite      xiii
Category, opslice      30 292 511 518
Category, opslice, simple      512 518
Category, receiving      119
Category, regular      257
Category, slice      19 28
Category, slice, simple      19 41 165
Category, small      xiii 410 423 430
Category, total      26
Category, well-powered      351
Cauchy reals      290
CCC      see “Cartesian closed category”
CCompC      see “Closed comprehension category”
CHA      see “Complete Heyting algebra”
Change-of-base      56
Change-of-base functor      48
Change-of-base situation      57
Characteristic morphism      15 335
CHARITY      163 457

Church numeral      456 459
Church — Rosser property      7
Church — Rosser property for dependent type theory      592
Church — Rosser property for polymorphic type theory      442
Church — Rosser property for simple type theory      134
Church’s thesis      402
Classical logic, xvi      224 270 337 358 365
Classifying category of a signature      124
Classifying category of an algebraic specification      185
Classifying category, $\lambda1$ -      135
Classifying category, $\lambda1_{\times}$ -      139
Classifying Eq-fibration      201
Classifying fibration in polymorphic type theory      482
Classifying fibration in predicate logic      234 278 299 323
Classifying morphism      335
Cleavage      49
Closed comprehension category      625 715
Closed in a topological space      209
Closed in the Scott topology      153
Closed, $\neg\neg$ -, in Eff      389
Closed, down      204
Closed, j-, for a nucleus j      355
Closure      355 642
Closure, fibration of -s      643 695
Closure, internal category of -s      644
Cloven fibration      49
Cloven opfibration      511
Co-algebra      7
Co-algebra of a comonad      433
Co-algebra of a functor      161
Co-induction      526
Co-induction assumption, as co-algebra      532
Co-induction proof principle, in a fibration      532
Cocomplete fibration      101
Code      33
Codiagonal      xiv
Codomain fibration      28 193 431 439 551 560 627
Coequaliser in a fibration      303
Cofibration      510
Coherence conditions      50
Coherent category      266
Coherent fibration      233 234 239 241 266
Coherent logic      227
Coherent specification      227
Comma category      55 57 79 515 548
Comma fibration in $Fib(\mathbb{B})$       549
Comma fibration in Fib      553
Comma object      547
Comma object in $Fib(\mathbb{B})$       549
Comma object in Fib      552
Commutation conversion for coproduct types      141
Commutation conversion for quotient types      289
Commutation conversion for sum types      454
Commutation conversion for weak dependent sum types      593
Comonad      46 168 433 494 535
Comonad, fibred      494
Comonad, weakening and contraction      536
Complete category      102
Complete category, small      439 467
Complete distributivity      105
Complete fibration      101
Complete fibration, small      439
Complete Heyting algebra      xvi 239 269 331 376
Complete lattice      xvi 300
Completeness of algebraic equational logic, in a category      186
Completeness of equational logic, in a fibration      208
Completeness of predicate logic, in a fibration      249
Comprehension      13 274
Comprehension category      539 583 613
Comprehension category from a full internal category      614
Comprehension category lifted along a fibration      544
Comprehension category over a fibration      666
Comprehension category with unit      616
Comprehension category, closed      625 715
Comprehension category, family      618 635 636
Comprehension category, full      613
Comprehension category, hom-set      566
Comprehension category, identity      614 627 637
Comprehension category, regular subobject      683
Comprehension category, simple      614 627
Comprehension category, subobject      614 683
Comprehension in a fibration      616
Congruence      533
Conjunction      223
Connective      223
Conservative functor      265
Constructive logic      xvi 237
constructor      160 162 456
context      2 121
Context kind      445
Context proposition      171 172 224
Context rules      171
Context type      171 224 445
Contraction      24 175 176
Contraction functor      176 190
Contraction functor wrt. a comprehension category      614
Contraction functor wrt. a weakening and contraction comonad      538
Contraction rule for propositions      172
Contraction rule for types      172
Contraction rule in dependent type theory      585
Contraction rule in simple type theory      122
Conversion      135 177
Conversion rule in dependent type theory      585
Conversion rule in higher order type theory      448
Coproduct      xiv
Coproduct in a comprehension category, strong      624
Coproduct in a comprehension category, weak      624
Coproduct in a fibration      97
Coproduct in a fibration in $Fib(\mathbb{B})$       521
Coproduct in a fibration in Fib      521
Coproduct type      140
Coproduct type in polymorphic type theory      457
Coproduct type, definable      453 483
Coproduct type, disjoint      526
Coproduct type, strong      591
Coproduct type, universal      526
Coproduct type, weak      591
Coproduct with simple parameters      158
Coproduct wrt. a comprehension category      540
Coproduct wrt. a comprehension category, strong      677
Coproduct wrt. a comprehension category, very strong      678
Coproduct wrt. a weakening and contraction comonad      537
Coproduct, disjoint      59
Coproduct, disjoint in a fibration      533
Coproduct, distributive      63 90 158
Coproduct, distributive and Frobenius      105
Coproduct, simple in a fibration      94 427 541
Coproduct, simple in an internal category      419 427
Coproduct, simple T-, in a fibration      149 541
Coproduct, universal      58 266 637
Coproduct, universal in a fibration      533
Coprojection morphism      xiv
Coprojection term      141
COQ      582 595 684 691
Cotuple      xiv
Cover      260 350 355
Cover, collective      578
Cover, Freyd      57
CT-structure      42 153 494 541 611 670
CT-structure, fibred      557
Cut rule      172
Cylindric algebra      242
Cylindrification operation      242
D-category      274
Data type      7 162 456
Data type, proof principles for -s      526 532 533
dcpo      see “Directed complete partial order”
Decidable partial equivalence relation      572
Decidable partial equivalence relation, family of -s, over $\omega$ -Sets      573
Decidable partial equivalence relation, family of -s, over Sets      572

1 2 3 4 5

О проекте