请输入您要查询的字词:

 

单词 AFormalTypeTheory
释义

A. Formal type theory


Just as one can develop mathematics in set theoryMathworldPlanetmath without explicitly using the axioms of Zermelo–Fraenkel set theory,in this book we have developed mathematics in univalent foundations without explicitly referring to a formalsystem of homotopy type theory. Nevertheless, it is important to have aprecise description of homotopy type theory as a formal system in order to, for example,

  • state and prove its metatheoretic properties, including logicalconsistency,

  • construct models, e.g. in simplicial sets, model categories, higher toposes,etc., and

  • implement it in proof assistants like Coq or Agda.

Even the logical consistency of homotopy type theory, namely that in the empty context there is no term a:𝟎, is not obvious: if we had erroneouslychosen a definition of equivalence for which 𝟎𝟏, thenunivalence would imply that 𝟎 has an element, since 𝟏 does.Nor is it obvious that, for example, our definition of 𝕊1 as a higherinductive type yields a type which behaves like the ordinary circle.

There are two aspects of type theoryPlanetmathPlanetmath which we must pin down before addressingsuch questions. Recall from the Introduction that type theorycomprises a set of rules specifying when the judgments a:A and aa:Ahold—for example, productsPlanetmathPlanetmathPlanetmath are characterized by the rule that whenever a:Aand b:B, (a,b):A×B. To make this precise, we must first defineprecisely the syntax of terms—the objects a,a,A, which these judgmentsrelate; then, we must define precisely the judgments and their rules ofinferenceMathworldPlanetmath—the manner in which judgments can be derived from other judgments.

In this appendix, we present two formulations of Martin-Löf typetheory, and of the extensionsPlanetmathPlanetmathPlanetmath that constitute homotopy type theory.The first presentationMathworldPlanetmathPlanetmath (\\autorefsec:syntax-informally) describes the syntax ofterms and the forms of judgments as an extension of the untypedλ-calculus, while leaving the rules of inference informal.The second (\\autorefsec:syntax-more-formally) defines the terms, judgments,and rules of inference inductively in the style of natural deduction, asis customary in much type-theoretic literature.

随便看

 

数学辞典收录了18232条数学词条,基本涵盖了常用数学知识及数学英语单词词组的翻译及用法,是数学学习的有利工具。

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 6:47:13