请输入您要查询的字词:

 

单词 62InductionPrinciplesAndDependentPaths
释义

6.2 Induction principles and dependent paths


When we describe a higher inductive type such as the circle as being generated by certain constructors, we have to explain what this means by giving rules analogous to those for the basic type constructors from http://planetmath.org/node/87533Chapter 1.The constructors themselves give the introduction rules, but it requires a bit more thought to explain the elimination rules, i.e. the inductionMathworldPlanetmath and recursion principles.In this book we do not attempt to give a general formulation of what constitutes a “higher inductive definition” and how to extract the elimination rule from such a definition — indeed, this is a subtle question and the subject of current research.Instead we will rely on some general informal discussion and numerous examples.

The recursion principle is usually easy to describe: given any type equipped with the same structureMathworldPlanetmath with which the constructors equip the higher inductive type in question, there is a function which maps the constructors to that structure.For instance, in the case of 𝕊1, the recursion principle says that given any type B equipped with a point b:B and a path :b=b, there is a function f:𝕊1B such that f(𝖻𝖺𝗌𝖾)=b and 𝖺𝗉f(𝗅𝗈𝗈𝗉)=.

The latter two equalities are the computation rules.There is, however, a question of whether these computation rules are judgmental equalities or propositional equalities (paths).For ordinary inductive types, we had no qualms about making them judgmental, although we saw in http://planetmath.org/node/87578Chapter 5 that making them propositional would still yield the same type up to equivalence.In the ordinary case, one may argue that the computation rules are really definitional equalities, in the intuitive sense described in the Introduction.

For higher inductive types, this is less clear. Moreover, since the operationMathworldPlanetmath 𝖺𝗉f is not really a fundamental part of the type theoryPlanetmathPlanetmath, but something that we defined using the induction principle of identity types (and which we might have defined in some other, equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath, way), it seems inappropriate to refer to it explicitly in a judgmental equality.Judgmental equalities are part of the deductive system, which should not depend on particular choices of definitions that we may make within that system.There are also semantic and implementation issues to consider; see the Notes (http://planetmath.org/chapter6notes).

It does seem unproblematic to make the computational rules for the point constructors of a higher inductive type judgmental.In the example above, this means we have f(𝖻𝖺𝗌𝖾)b, judgmentally.This choice facilitates a computational view of higher inductive types.Moreover, it also greatly simplifies our lives, since otherwise the second computation rule 𝖺𝗉f(𝗅𝗈𝗈𝗉)= would not even be well-typed as a propositional equality; we would have to compose one side or the other with the specified identification of f(𝖻𝖺𝗌𝖾) with b.(Such problems do arise eventually, of course, when we come to talk about paths of higher dimension, but that will not be of great concern to us here.See also §6.7 (http://planetmath.org/67hubsandspokes).)Thus, we take the computation rules for point constructors to be judgmental, and those for paths and higher paths to be propositional.11In particular, in the languagePlanetmathPlanetmath of §1.1 (http://planetmath.org/11typetheoryversussettheory), this means that our higher inductive types are a mix of rules (specifying how we can introduce such types and their elements, their induction principle, and their computation rules for point constructors) and axioms (the computation rules for path constructors, which assert that certain identity types are inhabited by otherwise unspecified terms).We may hope that eventually, there will be a better type theory in which higher inductive types, like univalence, will be presented using only rules and no axioms.

Remark 6.2.1.

Recall that for ordinary inductive types, we regard the computation rules for a recursively defined function as not merely judgmental equalities, but definitional ones, and thus we may use the notation : for them.For instance, the truncated predecessor function p:NN is defined by p(0):0 and p(succ(n)):n.In the case of higher inductive types, this sort of notation is reasonable for the point constructors (e.g. f(base):b), but for the path constructors it could be misleading, since equalities such as f(loop)= are not judgmental.Thus, we hybridize the notations, writing instead f(loop):= for this sort of “propositional equality by definition”.

Now, what about the induction principle (the dependent eliminator)?Recall that for an ordinary inductive type W, to prove by induction that (x:W)P(x), we must specify, for each constructor of W, an operation on P which acts on the “fibers” above that constructor in W.For instance, if W is the natural numbersMathworldPlanetmath , then to prove by induction that (x:)P(x), we must specify

  • An element b:P(0) in the fiber over the constructor 0:, and

  • For each n:, a function P(n)P(𝗌𝗎𝖼𝖼(n)).

The second can be viewed as a function “PP” lying over the constructor 𝗌𝗎𝖼𝖼:, generalizing how b:P(0) lies over the constructor 0:.

By analogyMathworldPlanetmath, therefore, to prove that (x:𝕊1)P(x), we should specify

  • An element b:P(𝖻𝖺𝗌𝖾) in the fiber over the constructor 𝖻𝖺𝗌𝖾:𝕊1, and

  • A path from b to b “lying over the constructor 𝗅𝗈𝗈𝗉:𝖻𝖺𝗌𝖾=𝖻𝖺𝗌𝖾”.

Note that even though 𝕊1 contains paths other than 𝗅𝗈𝗈𝗉 (such as 𝗋𝖾𝖿𝗅𝖻𝖺𝗌𝖾 and 𝗅𝗈𝗈𝗉\\centerdot𝗅𝗈𝗈𝗉), we only need to specify a path lying over the constructor itself.This expresses the intuition that 𝕊1 is “freely generated” by its constructors.

The question, however, is what it means to have a path “lying over” another path.It definitely does not mean simply a path b=b, since that would be a path in the fiber P(𝖻𝖺𝗌𝖾) (topologically, a path lying over the constant path at 𝖻𝖺𝗌𝖾).Actually, however, we have already answered this question in http://planetmath.org/node/87569Chapter 2: in the discussion preceding Lemma 2.3.4 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem3) we concluded that a path from u:P(x) to v:P(y) lying over p:x=y can be represented by a path p*(u)=v in the fiber P(y).Since we will have a lot of use for such dependent pathsin this chapter, we introduce a special notation for them:

(u=pPv):(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍P(p,u)=v).(6.2.2)
Remark 6.2.3.

There are other possible ways to define dependent paths.For instance, instead of p*(u)=v we could consider u=(p-1)*(v).We could also obtain it as a special case of a more general “heterogeneous equality”,or with a direct definition as an inductive type family.All these definitions result in equivalent types, so in that sense it doesn’t much matter which we pick.However, choosing p*(u)=v as the definition makes it easiest to conclude other things about dependent paths, such as the fact that apdf produces them, or that we can compute them in particular type families using the transport lemmas in §2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers).

With the notion of dependent paths in hand, we can now state more precisely the induction principle for 𝕊1: given P:𝕊1𝒰 and

  • An element b:P(𝖻𝖺𝗌𝖾), and

  • A path :b=𝗅𝗈𝗈𝗉Pb,

there is a function f:(x:𝕊1)P(x) such that f(𝖻𝖺𝗌𝖾)b and 𝖺𝗉𝖽f(𝗅𝗈𝗈𝗉)=.As in the non-dependent case, we speak of defining f by f(𝖻𝖺𝗌𝖾):b and 𝖺𝗉𝖽f(𝗅𝗈𝗈𝗉):=.

Remark 6.2.4.

When describing an application of this induction principle informally, we regard it as a splitting of the goal “P(x) for all x:S1” into two cases, which we will sometimes introduce with phrases such as “when x is base” and “when x varies along loop”, respectively.There is no specific mathematical meaning assigned to “varying along a path”: it is just a convenient way to indicate the beginning of the corresponding sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath of a proof; see Lemma 6.4.2 (http://planetmath.org/64circlesandspheres#Thmprelem2) for an example.

Topologically, the induction principle for 𝕊1 can be visualized as shown in Figure 6.1 (http://planetmath.org/62inductionprinciplesanddependentpaths#S0.F1).Given a fibration over the circle (which in the picture is a torus), to define a section of this fibration is the same as to give a point b in the fiber over 𝖻𝖺𝗌𝖾 along with a path from b to b lying over 𝗅𝗈𝗈𝗉.The way we interpret this type-theoretically, using our definition of dependent paths, is shown in Figure 6.2 (http://planetmath.org/62inductionprinciplesanddependentpaths#S0.F2): the path from b to b over 𝗅𝗈𝗈𝗉 is represented by a path from 𝗅𝗈𝗈𝗉*(b) to b in the fiber over 𝖻𝖺𝗌𝖾.

\\includegraphics

HoTT_fig_6.2.1.png

Figure 6.1: The topological induction principle for 𝕊1
\\includegraphics

HoTT_fig_6.2.2.png

Figure 6.2: The type-theoretic induction principle for 𝕊1

Of course, we expect to be able to prove the recursion principle from the induction principle, by taking P to be a constant type family.This is in fact the case, although deriving the non-dependent computation rule for 𝗅𝗈𝗈𝗉 (which refers to 𝖺𝗉f) from the dependent one (which refers to 𝖺𝗉𝖽f) is surprisingly a little tricky.

Lemma 6.2.5.

If A is a type together with a:A and p:a=Aa, then there is afunction f:S1A with

f(𝖻𝖺𝗌𝖾):a
𝖺𝗉f(𝗅𝗈𝗈𝗉):=p.
Proof.

We would like to apply the induction principle of 𝕊1 to the constant type family, (λx.A):𝕊1𝒰.The required hypotheses for this are a point of (λx.A)(𝖻𝖺𝗌𝖾)A, which we have (namely a:A), and a dependent path in a=𝗅𝗈𝗈𝗉xAa, or equivalently 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍xA(𝗅𝗈𝗈𝗉,a)=a.This latter type is not the same as the type a=Aa where p lives, but it is equivalent to it, because by Lemma 2.3.5 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem4) we have 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍𝗅𝗈𝗈𝗉A(a):𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍xA(𝗅𝗈𝗈𝗉,a)=a.Thus, given a:A and p:a=a, we can consider the composite

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍𝗅𝗈𝗈𝗉A(a)\\centerdotp:(a=𝗅𝗈𝗈𝗉xAa).

Applying the induction principle, we obtain f:𝕊1A such that

f(𝖻𝖺𝗌𝖾)a  and(6.2.6)
𝖺𝗉𝖽f(𝗅𝗈𝗈𝗉)=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍𝗅𝗈𝗈𝗉A(a)\\centerdotp.(6.2.6)

It remains to derive the equality 𝖺𝗉f(𝗅𝗈𝗈𝗉)=p.However, by Lemma 2.3.8 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem5), we have

𝖺𝗉𝖽f(𝗅𝗈𝗈𝗉)=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍𝗅𝗈𝗈𝗉A(f(𝖻𝖺𝗌𝖾))\\centerdot𝖺𝗉f(𝗅𝗈𝗈𝗉).

Combining this with (6.2.6) and canceling the occurrences of 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍 (which are the same by (6.2.6)), we obtain 𝖺𝗉f(𝗅𝗈𝗈𝗉)=p.∎

We also have a corresponding uniqueness principle.

Lemma 6.2.6.

If A is a type and f,g:S1A are two maps together with twoequalities p,q:

p:f(𝖻𝖺𝗌𝖾)=Ag(𝖻𝖺𝗌𝖾),
q:f(𝗅𝗈𝗈𝗉)=pλx.x=Axg(𝗅𝗈𝗈𝗉).

Then for all x:S1 we have f(x)=g(x).

Proof.

This is just the induction principle for the type family P(x):(f(x)=g(x)).∎

These two lemmas imply the expected universal propertyMathworldPlanetmath of the circle:

Lemma 6.2.7.

For any type A we have a natural equivalence

(𝕊1A)x:A(x=x).
Proof.

We have a canonical function f:(𝕊1A)(x:A)(x=x) defined by f(g):(g(𝖻𝖺𝗌𝖾),g(𝗅𝗈𝗈𝗉)).The induction principle shows that the fibers of f are inhabited, while the uniqueness principle shows that they are mere propositions.Hence they are contractible, so f is an equivalence.∎

As in §5.5 (http://planetmath.org/55homotopyinductivetypes), we can show that the conclusionMathworldPlanetmath of Lemma 6.2.7 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprelem3) is equivalent to having an induction principle with propositional computation rules.Other higher inductive types also satisfy lemmas analogous to Lemma 6.2.5 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprelem1),Lemma 6.2.7 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprelem3); we will generally leave their proofs to the reader.We now proceed to consider many examples.

随便看

 

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

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 17:21:32