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

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

Decidable proposition      401
Definability of equality      574
Definability of functors      573
Definability of isomorphisms      574
Definability of vertical morphisms      574
Definable Cartesian product type in polymorphic type theory      453 483
Definable collection      569 709
Definable coproduct type in polymorphic type theory      453 483
Definable subfibration      574
Definable sum type in polymorphic type theory      453 459
Deliverable      526 556
Dense image      359
Dense partial map      360
Dense, $\neg\neg$ -, in Eff      389
Dense, j-, for a nucleus j      355
Dependency      7 684
Dependent parameters      165
Dependent predicate logic      3 645 648
Dependent type theory      3 581 584
Derivability      122
Derivability in predicate logic      224
Descent theory      9 412 431 514
destructor      160 456
Diagonal      xiii
Diagonal element      242
Diagonal, parametrised      xiii 130 190
Diagram, internal      431 564
Diagram, internal, parametrised      434
Dialectica category      117 518
Dinatural transformation      484 485
Directed complete partial order      xvi 128 153 203 637
Directed complete partial order, continuously indexed      637
Directed complete partial order, reflexive      153 156 670
Directed subset      xvii
Disjoint coproduct in a fibration      533
Disjoint coproduct type      526
Disjoint union type      591
Disjunction      223
Display indexing      21 29 32 51 58 59 107 109
Display map      583 603 708
Display map category      610
Display map in a comprehension category      614
Distributive category      63 323 522
Distributive category, fibred      522
Distributive coproduct      63 90 105 158
Distributive lattice      167 233
Distributivity, complete      106 600
Domain fibration      30 325 429
Domain opfibration      511
Domain theoretic model of polymorphic type theory      482
Domain theoretic model of simple type theory      153
Domain theoretic model of the untyped $\lambda$ -calculus      156
Donkey sentence      597 601
Double negation in Eff      389
Double negation nucleus      354
Double negation rule      xv
DPL      see “Dependent predicate logic”
DPL-structure      654
DTT      see “Dependent type theory”
ECC      see “Calculus of constructions extended”
Effective object      388
Effective operation      699
Effective quotient type      284
Effective topos      376 383
Eilenberg — Moore category      46
Eilenberg — Moore category, fibred      80
elf      598
Embedding between dcpos      638
Encapsulation      460
Epi      xiii
Epi, regular      261 350 355
Epi, split      264
Eq-fibration      201
Eq-fibration classifying      201
Equaliser in a fibration      282
Equaliser, internal      419
Equality combinators      196
Equality componentwise      525
Equality external      177 192 226 227
Equality functor      291
Equality in a comprehension category, strong      624 633
Equality in a comprehension category, weak      624
Equality in a fibration      190
Equality intensional      591
Equality internal      177 192 226 227
Equality type, dependent      586
Equality type, polymorphic      449
Equality type, strong      589 590 680
Equality type, very strong      681
Equality type, weak      588 680
Equality wrt. a comprehension category      540
Equality wrt. a comprehension category, strong      682
Equality wrt. a comprehension category, very strong      682
Equality wrt. a weakening and contraction comonad      538
Equality, Lawvere rule for, in equational logic      179 195
Equality, Lawvere rule for, in predicate logic      229
Equality, Lawvere rule with Frobenius for, in equational logic      181 195
Equality, Lawvere rule with Frobenius for, in predicate logic      232
Equality, Leibniz      315 454
Equality, pointwise      525
Equality, propositional      177 226
Equality, simple, in a fibration      541
Equality, very strong      371 410
equation      178
Equation, algebraic      178
Equation, non-conditional      178
Exact category      297
Exchange rule for propositions      172
Exchange rule for types      172
Exchange rule in dependent type theory      586
Exchange rule in simple type theory      122
Excluded Middle      226 232
Existence predicate      33 375
Existential quantification      223
Exponent object      xiii
Exponent of a fibration with a category      92 573
Exponent of fibrations      117
Exponent type      xv
Exponent, fibred      92
Exponent, internal      419 429
Extension      511 513 514
Extension functor      510
Extension, Kan      513 635
Extensional dependent type theory      590
Extensional entailment in higher order logic      315 452 650
Extensional entailment rule      314
Extensional logic      177 192
Extensional partial equivalence relation      697
Extensional propositional equality      285
Extensional relation      375
Extensive category      62
Extensive fibration      534
Extent of a predicate      274
External equality      177 192
External existence      255
Externalisation      421 422 425 465 486 560
Extremal morphism      260
Factorisation in higher order logic      319
Factorisation system      260 359
Factorisation via quotients, in a fibration      302
Factorisation via subsets, in a fibration      281
Factorisation, image      257
Falsum      223
Family comprehension category over Cat      635
Family comprehension category over Sets      618 636
Family fibration of a fibration      106
Family fibration over Cat      108 635
Family fibration over Sets      32 95 98 105 108 194 201 239 278 299 322 331 353 360 376 571 618 625
Family of sets      20
Family of sheaves      364 709

Family, category with -ies      622
Family, constant      22
Family, separated      364 577 709
FhoDTT      see “Full higher order dependent type theory”
FhoDTT-structure      694
FhoDTT-structure, weak      694
Fibration      4 27
Fibration in a 2-category following Johnstone      78
Fibration in a 2-category following Street      56 548
Fibration of contexts in logic      174
Fibration of monos      43
Fibration of objects      30 326
Fibration of objects, split      93 325
Fibration of relations in a fibration      291 524
Fibration over a fibration      61
Fibration over a fibration in $Fib(\mathbb{B})$       550
Fibration over a fibration in Fib      505 554
Fibration with comprehension      616
Fibration with subset types      274 618
Fibration, $\lambda2$ -      473
Fibration, $\lambda2$ -, relationally parametric      501
Fibration, $\lambda2=$ -      473
Fibration, $\lambda\omega$ -      473 644 706
Fibration, $\lambda\omega=$ -      473
Fibration, $\lambda\rightarrow$ -      473
Fibration, $\lambda\rightarrow=$ -      473
Fibration, arrow in $Fib(\mathbb{B})$       551
Fibration, arrow in Fib      555
Fibration, classifying in polymorphic type theory      482
Fibration, classifying in predicate logic      234 278 299 323
Fibration, cloven      49
Fibration, cocomplete      101
Fibration, codomain      28 193 431 439 551 560 617 627
Fibration, coherent      233 234 239 241 266
Fibration, complete      101
Fibration, complete, small      439
Fibration, domain      30 325 429
Fibration, Eq-      201
Fibration, Eq-, classifying      201
Fibration, exponent with a category      92
Fibration, exponent with another fibration      117
Fibration, extensive      534
Fibration, family of a fibration      106
Fibration, family over Cat      108 635
Fibration, family over Sets      32 95 98 105 108 194 201 239 278 299 322 331 353 360 376 571 618 625
Fibration, fibre      551 555
Fibration, first order      233 236 238 239 241 267 270
Fibration, geometric      568
Fibration, higher order      330
Fibration, locally small      559 575 577 621 626 701
Fibration, morphism of -s      73
Fibration, opposite      113
Fibration, polymorphic      471
Fibration, poset      55
Fibration, realisability      241 245 331 376
Fibration, regular      233 234 246 374
Fibration, representable      116 325
Fibration, simple      41 439 627
Fibration, simple over a fibration      487 488 551 555
Fibration, small      423 438 564 578
Fibration, split      50
Fibration, sub      574 583
Fibration, sub, definable      574
Fibration, subobject      43 193 201 202 266 267 278 297 307 334 409 429 627
Fibration, subobject, regular      309
Fibration, type theoretic      44 611 627
Fibration, well-powered      351
Fibre      26
Fibre fibration      551 555
Fibred category      27
Fibred comonad      494
Fibred CT-structure      557
Fibred functor      73 74
Fibred global section      619 620
Fibred locally Cartesian closed category      633 669
Fibred monad      79 359
Fibred preorder      174 201
Fibred reflection      543 546
Fibred sheafification      366
Fibred span      514
Fibred strong coproduct      636
Fibred structure      80
Fibred Yoneda Lemma      323
Fibrewise fibration      550
Fibrewise structure      80
Fibrewise topos      568
final      see “Terminal”
First order fibration      233 236 238 239 241 267 270
First order predicate logic      221
Formation rule for propositions in equational logic      177
Formation rule for propositions in predicate logic      223
Formation rule for types in dependent type theory      586
Formation rule for types in polymorphic type theory      446
Formation rule in simple type theory      134
Frame      xvi 239 269 282 331 360 376
Freyd cover      57
Frobenius property      xv 103
Frobenius property and distributive coproducts      105
Frobenius property for coproducts      102 105
Frobenius property for coproducts wrt. a weakening and contraction comonad      538
Frobenius property for equality      191 199
Frobenius property for equality wrt. a weakening and contraction comonad      538
Frobenius property for quotients in a fibration      295
Frobenius property for quotients in type theory      290
Frobenius property for simple coproducts      102
Full higher order dependent type theory      3 645 684 688
Full higher order dependent type theory, weak      688
Full internal (sub)category      412 423 424 429 470 490 492 564 614 701 702
Full quotient type      284
Full subset type      273
Functor over $\mathbb{B}$       74
Functor, conservative      265
Functor, fibred      74
Functor, internal      415
Functor, polynomial      161 527
Functor, representable      351
Functor, split      74
Functor, strong      163
Functorial semantics      7 517
Functorial semantics for equational logic in a fibration      211
Functorial semantics for polymorphic type theory      472 482
Functorial semantics for predicate logic      248
Functorial semantics for simple type theory in a category      126 148
Functorial semantics for simple type theory in a fibration      150
Generic model of a signature      128
Generic model of a specification in predicate logic      249
Generic model of an equational specification      186 208
Generic object      326 564 577
Generic object, split      322 422
Generic object, strong      326
Generic object, weak      325
Geometric fibration      568
Geometric logic      364
Geometric morphism      364 365 386 568
Girard’s paradox      582 644 681 688 692
Global element      39 385
Global element functor      385
Global section      39
Global section functor      57 430 621 636
Global section, fibred      619 620
Global smallness      577
Grothendieck completion      107
Grothendieck construction      29 107 111
Grothendieck construction, generalised      517
Grothendieck topology      355 361 707
Grothendieck topos      365 700
Group      31 131 161 320 601
Group in a fibration      208
Group, abelian      286 651
Group, internal      408

1 2 3 4 5

О проекте