nLab
type

Skip the Navigation Links | Home Page | All Pages | Recently Revised | Authors | Feeds | Export |
Redirected from "universe of discourse".

Context

Type theory

type theory (dependent, extensional, intensional type theory)

syntax

propositions as types

logictype theory
propositionh-level 1 / hProp
trueunit type / h-level 0
falseempty type
conjunctionproduct type
disjunctionsum type (bracket type of)
implicationfunction type
universal quantificationdependent product type
existential quantificationdependent sum type (bracket type of)
equivalenceidentity type
quotientquotient type
SethSet / h-level 2

homotopy levels

semantics

Theorems

Contents

Idea

In modern logic, we understand that every variable should have a type, or domain of discourse. Untyped logic may be seen as simply a special case, in which there is only a single unique type. (Thus, untyped logic has one type, not no type.)

It is possible to build foundations of mathematics on type theory alone.

type, type theory

dependent type, dependent type theory, Martin-Löf dependent type theory

homotopy type, homotopy type theory

Revised on November 2, 2011 23:02:54 by Urs Schreiber (89.204.137.79)
Edit | Back in time (5 revisions) | See changes | History | Views: Print | TeX | Source | Linked from: set, logic, equivalence relation, internal logic, context, essentially algebraic theory, homotopy type, subset, type theory, coherent logic, sequent calculus, boolean-valued function, collection, type, preset, propositions as types, proposition, elementary embedding, logical functor, empty family, theory, dependent type, applications of (higher) category theory, W-type, type theory - contents, first-order hyperdoctrine, internal logic of an (infinity,1)-topos, identity type, display map, rewriting, signature (in logic), Kleene equality, family, type-theoretic definition of category, cohesive topos, modal logic, regular logic, term, variable, model theory, cartesian logic, 2-type theory, hyperdoctrine, syntactic site, 2-logic, categorical semantics, lambda-calculus, syntactic category, theory of objects, regular theory, cartesian theory, axiom, homotopy type theory, type of propositions, theorem, directed homotopy type theory, unit type, type of types, Boolean hyperdoctrine, contents of contents, product type, quotient type, stack semantics, cohesive homotopy type theory, interval type, homotopy level, function type, bracket type, dependent product type, Coq, empty type, inductive type, function extensionality, Agda, higher inductive type, notions of type, existential quantifier, universal quantifier, Kripke-Joyal semantics, sub-(infinity,1)-category - internal formulation, positive type, proofs as programs, proof, HoTT methods for homotopy theorists, univalence axiom, intensional type theory, type-theoretic model category, type (in model theory), dependent type theory, contractible type, extensional type theory, sum type, reflective sub-(infinity,1)-category - internal formulation, semantics, Oberwolfach HoTT-Coq tutorial, h-set, h-proposition, equivalence in homotopy type theory, dcpo, canonical form, coherent hyperdoctrine, negative type, beta-reduction, eta-conversion, dependent sum type, certified programming, substitution, relation between type theory and category theory, M-type