nLab
homotopy type theory - contents

Skip the Navigation Links | Home Page | All Pages | Recently Revised | Authors | Feeds | Export |
Created on November 1, 2012 14:58:45 by Stephan Alexander Spahn (79.227.160.169)
Edit | Views: Print | TeX | Source | Linked from: function, logic, internal logic, homotopy n-type, homotopy type, type theory, computer science, syntax - semantics duality, theory, W-type, type theory - contents, tripos, identity type, algebraic model for modal logics, pure type system, the logic S4(m), modal logic, variable, hyperdoctrine, axiom, homotopy type theory, type of types, axiom UIP, contents of contents, syntax, product type, quotient type, cohesive homotopy type theory, homotopy level, function type, bracket type, Coq, inductive type, Agda, higher inductive type, existential quantifier, universal quantifier, proof, HoTT methods for homotopy theorists, univalence axiom, intensional type theory, extensional type theory, sum type, semantics, h-set, equivalence in homotopy type theory, canonical form, substitution, relation between type theory and category theory, first-order theory, Haskell, logical framework, judgment, context extension, numeral, Brouwer-Heyting-Kolmogorov interpretation, monad (in computer science), computation, programming language, natural deduction, Practical Foundations for Programming Languages, modal type, Bishop set, h-groupoid, modal type theory, differential homotopy type theory, axiom K, observational type theory, meaning explanation, natural numbers type