请输入您要查询的字词:

 

单词 2HomotopyTypeTheory
释义

2. Homotopy Type Theory


The central new idea in homotopy type theory is that types can be regarded asspaces in homotopy theory, or higher-dimensional groupoidsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in categorytheoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

We begin with a brief summary of the connection between homotopy theoryand higher-dimensional category theory.In classical homotopy theory, a space X is a set of points equippedwith a topologyMathworldPlanetmath,and a path between points x and y is represented bya continuous map p:[0,1]X, where p(0)=x and p(1)=y.This function can be thought of as giving a point in X at each“moment in time”. For many purposes, strict equality of paths(meaning, pointwise equal functions) is too fine a notion. For example,one can define operationsMathworldPlanetmath of path concatenation (if p is a path fromx to y and q is a path from y to z, then the concatenation p\\centerdotq is a path from x to z) and inversesMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath (p-1 is a pathfrom y to x). However, there are natural equations between theseoperations that do not hold for strict equality: for example, the pathp\\centerdotp-1 (which walks from x to y, and then back along thesame route, as time goes from 0 to 1) is not strictly equal to theidentity path (which stays still at x at all times).

The remedy is to consider a coarserPlanetmathPlanetmath notion of equality of paths calledhomotopyMathworldPlanetmathPlanetmath.A homotopy between a pair of continuous maps f:X1X2 and g:X1X2 is a continuous map H:X1×[0,1]X2 satisfying H(x,0)=f(x) and H(x,1)=g(x). In the specific case of paths p and q from x to y, a homotopy is acontinuous map H:[0,1]×[0,1]Xsuch that H(s,0)=p(s) and H(s,1)=q(s) for all s[0,1].In this case we require also that H(0,t)=x and H(1,t)=y for all t[0,1],so that for each t the function H(,t) is again a path from x to y;a homotopy of this sort is said to be endpoint-preserving or rel endpoints.Such a homotopy is theimage in X of a square that fills in the space between p and q,which can be thought of as a “continuous deformation” between p andq, or a 2-dimensional path between paths.

For example, becausep\\centerdotp-1 walks out and back along the same route, you know thatyou can continuously shrink p\\centerdotp-1 down to the identitypath—it won’t, for example, get snagged around a hole in the space.Homotopy is an equivalence relationMathworldPlanetmath, and operations such asconcatenation, inverses, etc., respect it. Moreover, the homotopyequivalenceMathworldPlanetmathPlanetmath classes of loops at some point x0 (where two loops pand q are equated when there is a based homotopy between them,which is a homotopy H as above that additionally satisfies H(0,t)=H(1,t)=x0 for all t) form a group called the fundamentalgroupMathworldPlanetmathPlanetmath. This group is an algebraic invariant of a space, whichcan be used to investigate whether two spaces are homotopyequivalent (there are continuous maps back and forth whose compositesare homotopicMathworldPlanetmath to the identity), because equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath spaces haveisomorphicPlanetmathPlanetmathPlanetmath fundamental groups.

Because homotopies are themselves a kind of 2-dimensional path, there isa natural notion of 3-dimensional homotopy between homotopies,and then homotopy between homotopies between homotopies, and soon. This infiniteMathworldPlanetmathPlanetmath tower of points, path, homotopies, homotopies betweenhomotopies, …, equipped with algebraic operations such as thefundamental group, is an instance of an algebraic structurePlanetmathPlanetmath called a(weak) -groupoid. An -groupoid consists of acollectionMathworldPlanetmath of objects, and then a collection of morphismsMathworldPlanetmath betweenobjects, and then morphisms between morphisms, and so on,equipped with some complex algebraic structure; a morphism at level k is called a k-morphism. Morphisms at each levelhave identity, composition, and inverse operations, which are weak inthe sense that they satisfy the groupoid laws (associativity ofcomposition, identity is a unit for composition, inverses cancel) onlyup to morphisms at the next level, and this weakness gives rise tofurther structureMathworldPlanetmath. For example, because associativity of composition ofmorphisms p\\centerdot(q\\centerdotr)=(p\\centerdotq)\\centerdotr is itself ahigher-dimensional morphism, one needs an additional operation relatingvarious proofs of associativity: the various ways to reassociate p\\centerdot(q\\centerdot(r\\centerdots)) into ((p\\centerdotq)\\centerdotr)\\centerdots give rise to MacLane’s pentagonMathworldPlanetmath. Weakness also creates non-trivial interactions betweenlevels.

Every topological space X has a fundamental -groupoidwhosek-morphisms are the k-dimensional paths in X. The weakness of the-groupoid corresponds directly to the fact that paths form agroup only up to homotopy, with the (k+1)-paths serving as thehomotopies between the k-paths. Moreover, the view of a space as an-groupoid preserves enough aspects of the space to do homotopy theory:the fundamental -groupoid construction is adjoint to thegeometric realization of an -groupoid as a space, and thisadjunctionMathworldPlanetmath preserves homotopy theory (this is called the homotopyhypothesis/theorem,because whether it is a hypothesisMathworldPlanetmath or theoremdepends on how you define -groupoid). For example, you caneasily define the fundamental group of an -groupoid, and if youcalculate the fundamental group of the fundamental -groupoid ofa space, it will agree with the classical definition of fundamentalgroup of that space. Because of this correspondence, homotopy theoryand higher-dimensional category theory are intimately related.

Now, in homotopy type theory each type can be seen to have the structureof an -groupoid. Recall that for any type A, and any x,y:A,we have a identity type x=Ay, also written 𝖨𝖽A(x,y)or just x=y. Logically, we may think of elements of x=y as evidencethat x and y are equal, or as identifications of x withy. Furthermore, type theoryPlanetmathPlanetmath (unlike, say, first-order logic) allows usto consider such elements of x=Ay also as individuals whichmay be the subjects of further propositionsPlanetmathPlanetmath. Therefore, we caniterate the identity type: we can form the typep=(x=Ay)q of identifications betweenidentifications p,q, and the typer=(p=(x=Ay)q)s, and so on. The structureof this tower of identity types corresponds precisely to that of thecontinuous paths and (higher) homotopies between them in a space, or an-groupoid.

Thus, we will frequently refer to an element p:x=Ay asa pathfrom x to y; we call x its start pointand y its end point.Two paths p,q:x=Ay with the same start and end point are said to be parallelMathworldPlanetmathPlanetmath,in which case an element r:p=(x=Ay)q canbe thought of as a homotopy, or a morphism between morphisms;we will often refer to it as a 2-pathor a 2-dimensional pathSimilarly, r=(p=(x=Ay)q)s is the type of3-dimensional pathsbetween two parallel 2-dimensional paths, and so on. If thetype A is “set-like”, such as , these iterated identity typeswill be uninteresting (see §3.1 (http://planetmath.org/31setsandntypes)), but in thegeneral case they can model non-trivial homotopy types.

An important differencePlanetmathPlanetmath between homotopy type theory and classical homotopy theory is that homotopy type theory provides a syntheticdescription of spaces, in the following sense. Synthetic geometry is geometryMathworldPlanetmath in the style of Euclid [1]: one starts from some basic notions (points and lines), constructions (a line connecting any two points), and axioms(all right anglesMathworldPlanetmathPlanetmath are equal), and deduces consequences logically. This is in contrast with analyticgeometryMathworldPlanetmath, where notions such as points and lines are represented concretely using cartesian coordinatesMathworldPlanetmath in n—lines are sets of points—and the basic constructions and axioms are derived from this representation. While classical homotopy theory is analytic (spaces and paths are made of points), homotopy type theory is synthetic: points, paths, and paths between paths are basic, indivisible, primitive notions.

Moreover, one of the amazing things about homotopy type theory is that all of the basic constructions and axioms—all of thehigher groupoid structure—-arises automatically from the inductionMathworldPlanetmathprinciple for identity types.Recall from §1.12 (http://planetmath.org/112identitytypes) that this says that if

  • for every x,y:A and every p:x=Ay we have a type D(x,y,p), and

  • for every a:A we have an element d(a):D(a,a,𝗋𝖾𝖿𝗅a),

then

  • there exists an element 𝗂𝗇𝖽=A(D,d,x,y,p):D(x,y,p) for every two elements x,y:A and p:x=Ay, such that 𝗂𝗇𝖽=A(D,d,a,a,𝗋𝖾𝖿𝗅a)d(a).

In other words, given dependent functions

D:(x,y:A)(p:x=y)𝒰
d:a:AD(a,a,𝗋𝖾𝖿𝗅a)

there is a dependent function

𝗂𝗇𝖽=A(D,d):(x,y:A)(p:x=y)D(x,y,p)

such that

𝗂𝗇𝖽=A(D,d,a,a,𝗋𝖾𝖿𝗅a)d(a)(2.0.1)

for every a:A.Usually, every time we apply this induction rule we will either not care about the specific function being defined, or we will immediately give it a different name.

Informally, the induction principle for identity types says that if we want to construct an object (or prove a statement) which depends on an inhabitant p:x=Ay of an identity type, then it suffices to perform the construction (or the proof) in the special case when x and y are the same (judgmentally) and p is the reflexivityMathworldPlanetmath element 𝗋𝖾𝖿𝗅x:x=x (judgmentally).When writing informally, we may express this with a phrase such as “by induction, it suffices to assume…”.This reductionPlanetmathPlanetmathPlanetmath to the “reflexivity case” is analogous to the reduction to the “base case” and “inductive step” in an ordinary proof by induction on the natural numbersMathworldPlanetmath, and also to the “left case” and “right case” in a proof by case analysis on a disjoint unionMathworldPlanetmathPlanetmath or disjunctionMathworldPlanetmath.

The “conversion rule” (2.0.1) is less familiar in the context of proof by induction on natural numbers, but there is an analogous notion in the related concept of definition by recursion.If a sequenceMathworldPlanetmathPlanetmath (an)n is defined by giving a0 and specifying an+1 in terms of an, then in fact the 0th term of the resulting sequence is the given one, and the given recurrence relation relating an+1 to an holds for the resulting sequence.(This may seem so obvious as to not be worth saying, but if we view a definition by recursion as an algorithm for calculating values of a sequence, then it is precisely the process of executing that algorithm.)The rule (2.0.1) is analogous: it says that if we define an object f(p) for all p:x=y by specifying what the value should be when p is 𝗋𝖾𝖿𝗅x:x=x, then the value we specified is in fact the value of f(𝗋𝖾𝖿𝗅x).

This induction principle endows each type with the structure of an -groupoid, and each function between two types the structure of an -functorMathworldPlanetmath between two such groupoids. This is interesting from a mathematical point view, because it gives a new way to work with-groupoids. It is interesting from a type-theoretic point view, because it reveals new operations that are associated with each type and function. In the remainder of this chapter, we begin to explore this structure.

References

  • 1 Euclid, Elements,Vols. 1–13 Elsevier,300 BC
随便看

 

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

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/5 2:49:46