请输入您要查询的字词:

 

单词 22FunctionsAreFunctors
释义

2.2 Functions are functors


Now we wish to establish that functions f:AB behave functorially on paths.In traditional type theoryPlanetmathPlanetmath, this is equivalently the statement that functions respect equality.Topologically, this corresponds to saying that every function is “continuous”, i.e. preserves paths.

Lemma 2.2.1.

Suppose that f:AB is a function.Then for any x,y:A there is an operationMathworldPlanetmath

𝖺𝗉f:(x=Ay)(f(x)=Bf(y)).

Moreover, for each x:A we have apf(reflx)reflf(x).

The notation 𝖺𝗉f can be read either as the application of f to a path, or as the action on paths of f.

First proof.

Let D:(x,y:A)(p:x=y)𝒰 be the type family defined by

D(x,y,p):(f(x)=f(y)).

Then we have

d:λx.𝗋𝖾𝖿𝗅f(x):x:AD(x,x,𝗋𝖾𝖿𝗅x).

By path inductionMathworldPlanetmath, we obtain 𝖺𝗉f:(x,y:A)(p:x=y)(f(x)=g(x)).The computation rule implies 𝖺𝗉f(𝗋𝖾𝖿𝗅x)𝗋𝖾𝖿𝗅f(x) for each x:A.∎

Second proof.

By induction, it suffices to assume p is 𝗋𝖾𝖿𝗅x.In this case, we may define 𝖺𝗉f(p):𝗋𝖾𝖿𝗅f(x):f(x)=f(x).∎

We will often write 𝖺𝗉f(p) as simply f(p).This is strictly speaking ambiguous, but generally no confusion arises.It matches the common convention in category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath of using the same symbol for the application of a functorMathworldPlanetmath to objects and to morphismsMathworldPlanetmathPlanetmath.

We note that 𝖺𝗉 behaves functorially, in all the ways that one might expect.

Lemma 2.2.2.

For functions f:AB and g:BC and paths p:x=Ay and q:y=Az, we have:

  1. 1.

    𝖺𝗉f(p\\centerdotq)=𝖺𝗉f(p)\\centerdot𝖺𝗉f(q).

  2. 2.

    𝖺𝗉f(p-1)=𝖺𝗉f(p)-1.

  3. 3.

    𝖺𝗉g(𝖺𝗉f(p))=𝖺𝗉gf(p).

  4. 4.

    𝖺𝗉𝗂𝖽A(p)=p.

Proof.

Left to the reader.∎

Now we wish to establish that functions f:AB behave functorially on paths.In traditional type theory, this is equivalently the statement that functions respect equality.Topologically, this corresponds to saying that every function is “continuous”, i.e. preserves paths.

Lemma 2.2.3.

Suppose that f:AB is a function.Then for any x,y:A there is an operation

𝖺𝗉f:(x=Ay)(f(x)=Bf(y)).

Moreover, for each x:A we have apf(reflx)reflf(x).

The notation 𝖺𝗉f can be read either as the application of f to a path, or as the action on paths of f.

First proof.

Let D:(x,y:A)(p:x=y)𝒰 be the type family defined by

D(x,y,p):(f(x)=f(y)).

Then we have

d:λx.𝗋𝖾𝖿𝗅f(x):x:AD(x,x,𝗋𝖾𝖿𝗅x).

By path induction, we obtain 𝖺𝗉f:(x,y:A)(p:x=y)(f(x)=g(x)).The computation rule implies 𝖺𝗉f(𝗋𝖾𝖿𝗅x)𝗋𝖾𝖿𝗅f(x) for each x:A.∎

Second proof.

By induction, it suffices to assume p is 𝗋𝖾𝖿𝗅x.In this case, we may define 𝖺𝗉f(p):𝗋𝖾𝖿𝗅f(x):f(x)=f(x).∎

We will often write 𝖺𝗉f(p) as simply f(p).This is strictly speaking ambiguous, but generally no confusion arises.It matches the common convention in category theory of using the same symbol for the application of a functor to objects and to morphisms.

We note that 𝖺𝗉 behaves functorially, in all the ways that one might expect.

Lemma 2.2.4.

For functions f:AB and g:BC and paths p:x=Ay and q:y=Az, we have:

  1. 1.

    𝖺𝗉f(p\\centerdotq)=𝖺𝗉f(p)\\centerdot𝖺𝗉f(q).

  2. 2.

    𝖺𝗉f(p-1)=𝖺𝗉f(p)-1.

  3. 3.

    𝖺𝗉g(𝖺𝗉f(p))=𝖺𝗉gf(p).

  4. 4.

    𝖺𝗉𝗂𝖽A(p)=p.

Proof.

Left to the reader.∎

As was the case for the equalities in Lemma 2.1.4 (http://planetmath.org/21typesarehighergroupoids#Thmlem3), those in Lemma 2.2.2 (http://planetmath.org/22functionsarefunctors#Thmlem2) are themselves paths, which satisfy their own coherence laws (which can be proved in the same way), and so on.

随便看

 

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

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 7:20:40