|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Jacobs B. — Categorical Logic and Type Theory |
|
|
|
| Предметный указатель |
Track 33
Track, uniform 52 54 394
Transition system 513 526
Transitivity combinator 197
Transitivity combinator in polymorphic type theory 450
Transitivity rule in equational logic 179
Tripos 332 374 377
Tripos, realisability 334
Truth 223
Tuple morphism xiii
Tuple term 139
Type, 1 context 171 224 445
Type, 1 scheme 455
Type, 1, (co-)inductively defined 145
Type, 1, (co-)inductively defined in second order polymorphic type theory 456
Type, 1, abstract 461
Type, 1, atomic 134
Type, 1, basic 134
Type, 1, Cartesian product 138
Type, 1, Cartesian product, definable 453 483
Type, 1, coproduct 140
Type, 1, coproduct, definable 453 483
Type, 1, coproduct, disjoint 526
Type, 1, coproduct, distributive 142
Type, 1, coproduct, in polymorphic type theory 457
Type, 1, coproduct, strong 591
Type, 1, coproduct, universal 526
Type, 1, coproduct, weak 591
Type, 1, data 7 162 456
Type, 1, data, proof principles for -s 526 532 533
Type, 1, disjoint union 591
Type, 1, empty 141
Type, 1, equality, dependent 586
Type, 1, equality, strong 589 590 680
Type, 1, equality, very strong 681
Type, 1, equality, weak 588 680
Type, 1, exponent xv
Type, 1, Hagino 145 457
Type, 1, identity 584
Type, 1, power 316
Type, 1, product, dependent 586
Type, 1, product, higher order 448
Type, 1, product, second order 446
Type, 1, quotient 283
Type, 1, quotient in dependent predicate logic 650
Type, 1, quotient in simple predicate logic 283
Type, 1, singleton 138 586
Type, 1, subset in dependent predicate logic 650
Type, 1, subset in simple predicate logic 272
Type, 1, sum, definable 453 459
Type, 1, sum, dependent 586
Type, 1, sum, higher order 448
Type, 1, sum, second order 446
| Type, 1, sum, strong 589 675
Type, 1, sum, very strong 675
Type, 1, sum, weak 588 674
Type, 1, unit 138 586
Uniformity Principle 402
Unique choice 304 371 391
Universal colimits in a topos 349
Universal coproduct 58 90 266 637
Universal coproduct in a fibration 533
Universal coproduct type 526
Universal quantification 223
Validity of a conditional equation in a category 184
Validity of a conditional equation in a fibration 202
Validity of a predicate 247
Validity of a sequent 247
Validity of an algebraic equation 183
Valuation 67
Veritas 582
Vertical mono 351
Vertical morphism 26
Vertical subobject 351
Very strong coproduct wrt. a comprehension category 678
Very strong equality 209 306 362 371 410
Very strong equality type 681
Very strong equality wrt. a comprehension category 682
Very strong sum type 675
Weak completeness, for a fibration 708
Weak coproduct type, in dependent type theory 591
Weak coproduct, in a comprehension category 624
Weak equality type 680
Weak equality type in dependent type theory 588
Weak equality, in a comprehension category 624
Weak FhoDTT-structure 694
Weak full higher order dependent type theory 688
Weak generic object 325
Weak initial algebra 457 458
Weak natural numbers object 456
Weak sum type 674
Weak sum type in dependent type theory 588
Weak terminal co-algebra 457 458
Weakening 24 175 230 604
Weakening functor 176
Weakening functor wrt, a comprehension category 614
Weakening functor wrt. a weakening and contraction comonad 537
Weakening rule for propositions 172
Weakening rule for types 172
Weakening rule in dependent type theory 585
Weakening rule in simple type theory 122
Weakening, notation for 176
Well-powered category 351
Well-powered fibration 351
Yoneda functor 428
Yoneda functor, fibred 440
Yoneda lemma, fibred 323
|
|
|
| Реклама |
|
|
|
|
|
О проекте