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

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

blank
blank
blank
Красота
blank
Jacobs B. — Categorical Logic and Type Theory
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.


Язык: en

Рубрика: Computer science/

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

ed2k: ed2k stats

Издание: 1st edition

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

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

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

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID
blank
Предметный указатель
Quotient type in a fibration, effective      295 296
Quotient type in a fibration, full      295 296
Quotient type in dependent predicate logic      650
Quotient type in simple predicate logic      283
Quotient type in simple predicate logic, effective      284
Quotient type in simple predicate logic, full      284
r.e.      see “Recursive enumerability”
RCCC      see “Relatively Cartesian closed category”
Realisability fibration      241 245 331 376
Realisability interpretation      240
Realisability topos      383 456
Realisability tripos      334
Realisability, Kleene      240
Realisability, Kleene, higher order      373
Realisability, Lifschitz      334
Realisability, modified      334 443
Recursive enumerability      241 329
Recursive function, partial      xvii
Recursive mathematics      400
Recursive subset      329
Reductio ad absurdum      224 232
Reflection      542 546
Reflection between types and kinds      690
Reflection, fibred      543 546
Reflection, separated      363 387
Reflexive closure      289
Reflexive coequaliser      421
Reflexive congruence relation      533
Reflexive dcpo      153 156 670
Reflexive graph      501
Reflexive object      156
Reflexive object in a presheaf topos      157
Reflexive relation      44
Reflexive relation, category of -s      303
Reflexivity combinator      196
Reflexivity rule in equational logic      179
Regular category      257 297
Regular epi      261 350 355
Regular epi topology      707
Regular fibration      233 234 246 374
Regular logic      227
Regular mono      46 345
Regular specification      227
Regular subobject      46
Regular subobject classifier      336
Regular subobject in a category of sheaves      365
Regular subobject of a family of PERs      499 552
Regular subobject of a metric space      330
Regular subobject of a PER      270 337 499
Regular subobject of an $\omega$-set      336 496 697
Reindexing      48
Reindexing functor      48
Relabelling functor      48
Relation      205
Relation classifier      346
Relation in a fibration      253 291 524
Relation, equivalence      45
Relation, equivalence, almost      384 390
Relation, equivalence, effective      297
Relation, equivalence, partial      45
Relation, extensional      375
Relation, functional      368
Relation, functional in a fibration      254 265
Relation, induction in terms of -s      533
Relation, logical      505 518 519
Relation, reflexive      44 303
Relation, reflexive, least      303
Relation, single-valued      254 304 368 375
Relation, strict      375
Relation, symmetric      44
Relation, total      254 368 375
Relation, transitive      44
Relatively Cartesian closed category      610 623
Replacement combinator      197
Replacement combinatorin dependent type theory      587
Replacement combinatorin polymorphic type theory      450
Replacement rule in equational logic      179
Replacement rule in predicate logic      225
Representable fibration      116 325
Representable functor      351
Representable presheaf      116 157
Ring      311 650
Ring, local      232
Ring, module over a      514
Saturated subset      270 329
Scone      57 524
Scott closed      106 153
Scott continuous      xvii
Scott domain      482 643
Scott topology      153
Separated family      364 577 709
Separated family, $\neg\neg$-, in Eff      396 709
Separated object      360 363 371
Separated object, $\neg\neg$-, in Eff      390
Separated reflection      363 387
Separated, canonically      388
Setoid      591 623
setting      686
Sheaf      360 363 371 707
Sheaf on a site      361 383
Sheaf, $\neg\neg$-, in Eff      390
Sheaf, canonically a      388
Sheaf, family of -ves      364 577 709
Sheafification      363
Sheafification, fibred      366
Sieve      340 355
Signature      64 460
Signature with predicates      222
Signature with predicates, fibration of      222
Signature, distributive      144
Signature, fibration of -s      65 104 526
Signature, Hagino      145 456 527
Signature, heterogeneous      64
Signature, higher order      313
Signature, higher order, fibration of -s      313
Signature, homogeneous      64
Signature, many-sorted      64
Signature, many-typed      64
Signature, polymorphic      449 464 472
Signature, single-sorted      64
Signature, single-typed      64 70
Signature, underlying      129
Simple comprehension category      614 627
Simple coproduct in a fibration      94 427
Simple coproduct in an internal category      419 427
Simple equality      190
Simple fibration      41 439 627
Simple fibration in $Fib(\mathbb{B})$      551
Simple fibration in Fib      555
Simple fibration over a fibration      487 488 551 555
Simple limits of type C      436
Simple opfibration      511
Simple opslice category      512
Simple parameters      157
Simple predicate logic      3 495
Simple product in a fibration      94 427 437
Simple product in an internal category      419 427 430
Simple slice category      19 41 165
Simple T-coproduct      149
Simple T-product      148
Simple type theory      3 119
Simplicial object      412
Single-valued relation      254 304 368 375
Singleton map      341
Singleton predicate      317
Singleton type      138 586
Singleton, j-      356 363
Site      355
Slice (category)      19 28
Slice (category), simple      165
Small category, xiii      410 423 430
Small complete category      439 467 702
Small complete fibration      439
Small fibration      423 438 564 578
Small limit, in a fibration      436
sort      1 64
Soundness of a rule      185
Soundness of algebraic equational logic in a category      185
Soundness of equational logic in a fibration      208
Soundness of predicate logic in a fibration      249
span      342 561
Span, fibred      133 189 514
Specification      170
Specification, algebraic      178 513 517
Specification, equational      178
Specification, first order      227
Specification, higher order      315
SPL      see “Simple predicate logic”
Split epi      264
Split fibration      50 324
Split fibred adjunction      84
Split functor      74
Split generic object      322 422
Split indexed category      51
Split opfibration      511
Splitting      50
STACK      708
Stack completion      708
Stack completion of families of $\omega$-sets over Eff      710
Stack completion of families of PERs over Eff      713
Strength      163
Strengthening rule in logic      173 230
Strict initial object      59 63 266
Strict predicate      379
Strict relation      375
Strong coproduct in a comprehension category      624
Strong coproduct type in dependent type theory      591
Strong coproduct wrt. a comprehension category      677
Strong coproduct, fibred      636
Strong equality in a comprehension category      624 633
Strong equality type      680
Strong equality type in dependent type theory      589 590
Strong equality wrt. a comprehension category      682
Strong functor      163
Strong generic object      326
Strong monad      168
Strong normalisation      7 334
Strong normalisation for dependent type theory      592
Strong normalisation for polymorphic type theory      442
Strong normalisation for simple type theory      134
Strong sum type      675
Strong sum type in dependent type theory      589
STT      see “Simple type theory”
Subfibration      574 583
Subfibration, definable      574
Subfunctor      579
Subobject      19
Subobject classifier      335
Subobject comprehension category      614 627 683
Subobject fibration      43 193 201 202 266 267 278 297 307 334 409 429 627
Subobject in a category of sheaves      365
Subobject on a family      552
Subobject, closed      355
Subobject, dense      355
Subobject, regular comprehension category      683
Subobject, regular fibration      309
Subobject, vertical      351
Subquotient      39
Subquotient, separated, in Eff      403
Subset term      316
Subset type in a DPL-structure      656
Subset type in a fibration      274 570
Subset type in dependent predicate logic      650
Subset type in simple predicate logic      272
Subset type, full, in a fibration      274 410
Subset type, full, in simple predicate logic      273
Substitution      48
Substitution combinator      197
Substitution functor      12 48
Substitution in category theory      23
Substitution in type theory      xv 123
Substitution lemma      126
Substitution rule in dependent type theory      585
Substitution rule in equational logic      179
Substitution rule in logic      172
Substitution rule in simple type theory      123 125
Substitution, simultaneous      66 125
Subtyping      495 506
Sum type, definable      453 459
Sum type, dependent      586
Sum type, higher order      448
Sum type, second order      446
Sum type, strong      675
Sum type, strong in dependent type theory      589
Sum type, very strong      675
Sum type, weak      674
Sum type, weak in dependent type theory      588
Symmetry combinator      196
Symmetry combinator in polymorphic type theory      450
Symmetry rule in equational logic      179
Term as in universal algebra      66
Term in a comprehension category      615
Term model      7
Term model of a dependent type theory      601
Term model of a logic over polymorphic type theory      497
Term model of a polymorphic type theory      471 481
Term model of a signature      69
Term model of a simple type theory      124
Term model of dependent predicate logic      651 656
Term model of dependent type theory      628
Term model of full higher order dependent type theory      689
Term model of polymorphic dependent type theory      666
Term model of the untyped $\lambda$-calculus      156
Terminal co-algebra with simple parameters      168
Terminal co-algebra, co-inductive      532
Terminal co-algebra, construction of -s      167
Terminal object      xiii
Terminal object, fibred      85
Terminal object, indecomposable      636
Terminal object, internal      418 420 430
Tertium non datur      226 232
Theory      170
Theory in equational logic      181
Theory of predicates      647 663
Theory, first order      227
Topological group      408
Topological space      209 239 265 408
Topological space, hausdorff      209
Topological system      516
Topology, Grothendieck      355
Topology, Lawvere — Tierney      354
Topology, regular epi      355 707
Topology, sup      355 383
Topos      334 429
Topos as a closed comprehension category      632
Topos as a DPL-structure      654
Topos as a FhoDTT-structure      695
Topos of sheaves      365
Topos, effective      376 383
Topos, elementary      339
Topos, fibrewise      568
Topos, Grothendieck      365 700
Topos, presheaf      157 340 428 485
Topos, realisability      383
Total category      26
Total category, Cartesian product in      520
Total category, coproduct in      521 567
Total category, exponent in      523
Total category, structure in      487
Total relation      254 368 375
1 2 3 4 5
blank
Реклама
blank
blank
HR
@Mail.ru
       © Электронная библиотека попечительского совета мехмата МГУ, 2004-2024
Электронная библиотека мехмата МГУ | Valid HTML 4.01! | Valid CSS! О проекте