|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Jacobs B. — Categorical Logic and Type Theory |
|
|
|
| Предметный указатель |
Group, quotient 286 650
Group, topological 408
Group, torsion free 178
Groupoid 30
Groupoid, internal 412 414
HA see “Heyting Algebra”
Hagino signature 145 456 527
Hagino type 145 457
Heyting algebra xvi
Heyting algebra, complete xvi 239 269 331 376
Higher order fibration 330 357 365
Higher order logic 314 650
Higher order signature 313
Higher order, full, dependent type theory 3 645 684 688
Higher order, weak 688
HML 647 663
HOL 311
Ideal in a dcpo 153 670
Ideal in a ring 232 311
Identity comprehension category 627 637
Identity extension condition 477
Identity rule 172
Identity type 584
Image 257
Image factorisation 257
Image, stable 257
Implication 223
Impredicativity 442
Indecomposable object 636
Indeterminate 114 555
Indexed category 50
Indexed category, opposite 112
Indexed category, split 51
Induction 526
Induction assumption, as algebra 527
Induction proof principle in a fibration 528
Induction proof principle in terms of relations 533
Inequality 13 18
Inhabitation 121
Initial algebra 162
Initial algebra with simple parameters 164 168
Initial algebra, construction of -s 167
Initial algebra, inductive 528 529 532
Initial object xiv
Initial object, strict 59 63 266
Institution 133 517
Intensional equality 591
Internal adjunction 418
Internal Cartesian closed category 419 426
Internal Cartesian product 418 429
Internal category 7 10 408
Internal category, discrete 411 429 434
Internal category, finite 411
Internal category, full 412 423 424 429 470 490 492 564 614 701 702
Internal category, full, in a fibration 563
Internal category, indiscrete 421
Internal category, preorder 414
Internal diagram 431 564
Internal diagram, parametrised 434
Internal equaliser 419
Internal equality 177 192
Internal existence 255 420
Internal exponent 419 429
Internal functor 415
Internal functor category 417
Internal group 184 408
Internal group in a fibration 208
Internal groupoid 412 414
Internal injectivity 254
Internal language 5 8 188 251 374 409
Internal language of a topos 649
Internal logic 192 251
Internal monoid 439
Internal natural transformation 415
Internal simple coproduct 419
Internal simple product 419 430
Internal surjectivity 254
Internal terminal object 418 420 430
Internalisation 428 485
Intrinsic property 54 109
Intuitionism 400
Invariant 527
Inverse image functor 48
ISABELLE 311 442 598
Kind context 445
Kind context in full higher order dependent type theory 688
Kind context in polymorphic dependent type theory 663
Kind context in polymorphic type theory 444
Kleene application xvii 332 334
Kleene application in Eff 400
Kleene equality xvii
Kleene normal form theorem 401
Kleene realisability 240
Kleene star 65
Kleisli category 46 80 117 130 205 494
Kleisli category, fibred 80
Kripke model 236
KZ-doctrine 40
Lattice xvi
Lattice, complete xvi 300
Lattice, complete, internally 352
Lattice, distributive 167 233
Lawvere — Tierney topology 354
LCCC see “Locally Cartesian closed category”
LEGO 582 595 684 691
Leibniz equality 315 454
Lift object 341
Lindenbaum algebra 125 154
Local exponential 82
Local ring 232
Locale xvi 239 516
Localisation 100
Locally Cartesian closed category 39 81 343 560 564 583 627 702
Locally Cartesian closed category, fibred 90 633 669
Locally small category xiii 428 558
Locally small fibration 559 575 577 621 626 701
Logical category 266
Logical framework 7 597
Logical framework and internal categories 7 599
Logical framework, Edinburgh 598
Logical framework, Martin-Loef 598
Logical morphism 339
Logical predicate 518
Logical relation 505 518 519
Logos 267
Logos, pre 266
Markov’s Principle 401
Martin-Loef type theory 582
Mate rule for equality in equational logic 179 181
Mate rule for equality in predicate logic 229
Mate rule for existential quantification, in predicate logic 230 234 247
Mate rule for product types, in polymorphic type theory 453
Mate rule for sum types, in polymorphic type theory 453
Mate rule for universal quantification, in predicate logic 230 235
membership 316
Membership predicate 341
Membership relation 346
Metric predicate 279 329
Metric space 279 329
ML 442 455 691
ML style polymorphism 455
Model of a signature 66 128
Model of a signature with predicates in a fibration 246
Model of a signature with predicates, set-theoretic 235
Model of a specification in equational logic 210
Model of a specification in predicate logic 249
Model,  - 150
Model, generic 128
Model, generic of an equational specification 186 208
Modest object in Eff 388
| Modest set 39 388
Modification 111
Module 514
Monad 117 130 205 352 433
Monad, fibred 79 359
Monad, strong 168
Mono xiii
Mono, fibration of -s 43
Mono, regular 345
Mono, vertical 351
Monoid 70 461 600 601
Monoid, commutative 286
Monoid, free 65
Monoid, internal 439
Monoidal structure 86 619
Monotone function xvi
Multifunction 205
Myhill — Shepherdson Theorem 699
Natural numbers object 159
Natural numbers object in  -Sets 39
Natural numbers object in Eff 399 402
Natural numbers object in PER 39
Natural numbers object with simple parameters 159
Natural numbers object, fibred 160
Natural numbers object, weak 456
Natural transformation xiii
Natural transformation, fibred 76
Natural transformation, internal 415
Natural transformation, vertical 76
Negation 223 224
Negation in a topos 354
Negative occurrence 463
NNO see “Natural numbers object”
Nucleus in a topos 354
Nucleus on a fibration 359
Nucleus on a frame 360
Nucleus, double negation 354 358
Nucleus, double negation in Eff 389
NUPRL 582
Omega set 33 336
Omega set, fibration of -s over -Sets 51 631 696
Omega set, fibration of -s over Eff 394 631 696 710
On-the-nose 73
Opcartesian morphism 292 510
Opcartesian morphism and coproducts 545
Opcartesian morphism and equality 546
Opfibration 252 511
Opfibration, cloven 511
Opfibration, simple 511
Opfibration, split 511
Opposite category xiii
Opposite fibration 113
Opposite indexed category 112
Opreindexing 511
Opslice (category) 30 292 511 518
Opslice (category), simple 512 518
Orthogonality to a collection of morphisms 260 677 682
Orthogonality to an object 469 711
Overloading 71
Parameter, dependent -s 165
Parameter, simple -s 157
Parametricity and (di)naturality conditions 484
Parametricity and definable (co)products 483
Parametricity and weakly intial algebras / terminal co-algebras 483
Parametricity in the sense of Reynolds 443 477 500
Parametricity in the sense of Strachey 442 477
Parametricity, relational 501
Parametrised diagonal xiii 130 190
Parametrised internal diagram 434
Partial combinatory algebra 332
Partial equivalence relation 35 268 270 329 337 394 402
Partial equivalence relation, category of -s 36
Partial equivalence relation, category of -s with parametric maps 477
Partial equivalence relation, decidable 572
Partial equivalence relation, extensional 697
Partial equivalence relation, fibration of -s over -Sets 53 98 424 475 572 631 670 684 696
Partial equivalence relation, fibration of -s over Eff 394 425 476 631 684 696 713
Partial equivalence relation, fibration of -s over PER 631
Partial equivalence relation, fibration of -s over PPER 479
Partial equivalence relation, fibration of -s over Sets 475 561 572
Partial equivalence relation, internal category of -s in -Sets 411 427 439
Partial equivalence relation, internal category of -s in Eff 412 428
Partial equivalence relation, internal category of -s in Sets 411
Partial function 341
Partial map 342
Partial map classifier 342 633
Partial map, dense 360
Partial map, extension of 360
PCA see “Partial combinatory algebra”
PDTT see “Polymorphic dependent type theory”
PDTT-structure 667 706
PER see Partial equivalence relation
Pointed family 38
Pointed set 39 132 188 313 341
Pointwise equality 525
Pointwise indexing 20 29 32 58 59 107 109
Polymorphic dependent type theory 3 645 663
Polymorphic fibration 471
Polymorphic predicate logic 3 495 545 552
Polymorphic signature 449 464 472
Polymorphic type theory 3 441
Polymorphic type theory, first order 441 446
Polymorphic type theory, higher order 442 448
Polymorphic type theory, logic over 495
Polymorphic type theory, second order 441 446
POSET xvi
Positive occurrence 463
Power object 341 346
Power object, non-empty 353
Power type 316
PPL see “Polymorphic predicate logic”
Pre-equality 683
Preorder xvi
Preorder, fibred 43 174 201
Presheaf 157 432 514 619 635
Presheaf, topos 157 340 428 485
Product in a comprehension category 624
Product in a fibration 97
Product type, dependent 586
Product type, higher order 448
Product type, second order 446
Product wrt. a comprehension category 540
Product wrt. a weakening and contraction comonad 537
Product, simple T-, in a fibration 148 541
Product, simple, in a fibration 94 427 437 541
Product, simple, in an internal category 419 427
Product, simple, internal 430
Profunctor 514
Projection between dcpos 638
Projection in a comprehension category 614
Projection morphism xiii
Projection rule in dependent type theory 585
Projection term 139
Projection, dependent 603
Projection, subset 274
Proposition as object 138
Proposition as type 136 137 451
Proposition as type a la de Bruijn 597
Proposition as type a la Howard 597
Proposition context 171 172 224
Pseudo functor 50
Pseudo map of adjunctions 91
PTT see “Polymorphic type theory”
Pullback functor 48
Pullback lemma 30
PVS 311 582 646
Quest 442
Quotient type 14
Quotient type in a DPL-structure 659
Quotient type in a fibration 292
|
|
|
| Реклама |
|
|
|
|
|
О проекте