Revision #2499 → #2952 · back to history
addedType theory (overview)cc1a232e2a1d
addedRussell's paradox42d3b1eaa74c
addedRamified theory of typesc7e60974194c
addedSimply typed lambda calculus41767f193253
addedIntuitionistic type theoryc5fcdd190626
addedCalculus of constructionsd6ccdb4ac1b1
addedType theory as a mathematical logice8246330c456
addedFour basic judgmentsb9352ec1664b
addedJudgment from assumptions9820291709a7
addedContext of a judgmentabb8af36d2f2
addedInference rulef0223dee31b3
addedSubstitution rule for judgmental equality077ca18e16fd
addedProof tree5d7cbb7a14f9
addedConstant term typing rulefb73edf83f34
addedType inhabitation problemf62792bb1ea6
addedGirard's paradox856725f5e0be
addedFour kinds of type rulesabba582917aa
addedBHK interpretation of intuitionistic logic8a3126fd4521
addedNo term of excluded-middle typea9c91cb5fce6
addedConstructive existence proof25518ca6e511
addedProof by contradiction (non-constructive)09a1ae547671
addedCurry–Howard correspondence9f4d28b8aaec
addedCartesian closed categories correspond to typed λ-calculus0bd29c97f2f7
addedC-monoids correspond to untyped λ-calculus314fddc13259
addedLocally cartesian closed categories correspond to Martin-Löf type theories80b856feee0f
addedHomotopy type theory989a892666e4
addedCubical type theory6b9b454ef784
addedAtomic term1a49b7bf9404
addedFunction type (simple type)fe777ea97c86
addedTwo-argument natural number functionf80f9d85e60e
addedRight associativity of function arrowsd6643d67b5bf
addedLambda term4d24d6a21494
addedDoubling function lambda term9ca88bdeee7c
addedFunction application rule995b0fc39af7
addedDeduced type notations from application45d345689720
addedBeta- and eta-reduction177a8fccca14
addedBeta-reduction example term69a6b561546f
addedEmpty type454bd1ad6190
addedUnit typef18a48dabca7
addedBoolean type0d312fb4f752
addedNatural numbers (Peano style)196a4478ce17
addedType constructor88cef3cbe359
addedProduct type2dd1539f5616
addedSum type (tagged union)4353220e5536
addedPolymorphic termf42b3a658431
addedPolymorphic identity functiona98aa69833b1
addedPolymorphic list-append function0038220b8516
addedGeneric product eliminator functionseedcc15cabee
addedGeneric sum type constructorse60def6af373
addedDependent type574698573b41
addedVector-length dependent type (dot product)698387ab64f4
addedLambda cube239df73896a8
addedDependent product and sum types80442677928a
addedDependent pair (Boolean eliminator)c47fbcf68d6a
addedIdentity type1434c5b2b997
addedReflexivity constructor for identity type61a0069f9d07
addedInductive typed6e968c61fc9
addedSet theory has rules and axioms; type theory only rules363e527b4af8
addedClassical logic has excluded middle; type theory need notf6c733e0c287
addedSet membership vs. single-typing of terms00dcda2216e8
addedType theory's built-in computation0da91e55c000
addedSet theory encodes numbers as setse28c5af530e0
addedProofs have types in type theory806d42770bc2
addedStrongly normalizing type theory0d3852123168
addedType equivalences (algebraic identities)94adda08c5fe
addedMost type theories lack axioms3ab806a6d6ce
addedUnivalence axiom3e08bf51f24a
addedAxiom of choice derivable in type theoryd791f058c9cf
addedBasic types for individuals and truth-values (Montague)2f2348e4b853
addedComplex type as function type81b27d35d94a
addedNatural language quantifier type12d70d3129be
addedType theory with records04a276e0a036