|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Jacobs B. — Categorical Logic and Type Theory |
|
|
|
| Предметный указатель |
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  -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,  -, in Eff 396 709
Separated object 360 363 371
Separated object, -, 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, -, 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  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 -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  -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
|
|
|
| Реклама |
|
|
|
|
|
О проекте