ホモトピー型理論

[005B]

[005C] 定義

iiを階数とする。型PreCat(i):U(succ(i))\mathord {\textnormal {\textsf {PreCat}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))を次のレコード型と定義する。

  • -対象(object)の型Obj:U(i)\mathord {\textnormal {\textsf {Obj}}}:\mathcal {U}(i)
  • -射(morphism)の型の族Map:ObjObjU(i)\mathord {\textnormal {\textsf {Map}}}:\mathord {\textnormal {\textsf {Obj}}}\to \mathord {\textnormal {\textsf {Obj}}}\to \mathcal {U}(i)
  • -恒等射(identity)id:{x:Obj}Map(x,x)\mathord {\textnormal {\textsf {id}}}:\prod _{\lbrace x:\mathord {\textnormal {\textsf {Obj}}}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x,x)
  • -射の合成(composition)comp:{x1,x2,x3:Obj}Map(x2,x3)Map(x1,x2)Map(x1,x3)\mathord {\textnormal {\textsf {comp}}}:\prod _{\lbrace x_{1},x_{2},x_{3}:\mathord {\textnormal {\textsf {Obj}}}\rbrace }\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{3})
  • -_:x1,x2:ObjIsSet(Map(x1,x2))\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\mathord {\textnormal {\textsf {IsSet}}}(\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2}))
  • -_:x1,x2:Objf:Map(x1,x2)comp(id,f)=f\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {id}}},f)=f
  • -_:x1,x2:Objf:Map(x1,x2)comp(f,id)=f\_:\prod _{x_{1},x_{2}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\mathord {\textnormal {\textsf {comp}}}(f,\mathord {\textnormal {\textsf {id}}})=f
  • -_:x1,x2,x3,x4:Objf1:Map(x1,x2)f2:Map(x2,x3)f3:Map(x3,x4)comp(comp(f3,f2),f1)=comp(f3,comp(f2,f1))\_:\prod _{x_{1},x_{2},x_{3},x_{4}:\mathord {\textnormal {\textsf {Obj}}}}\prod _{f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})}\prod _{f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})}\prod _{f_{3}:\mathord {\textnormal {\textsf {Map}}}(x_{3},x_{4})}\mathord {\textnormal {\textsf {comp}}}(\mathord {\textnormal {\textsf {comp}}}(f_{3},f_{2}),f_{1})=\mathord {\textnormal {\textsf {comp}}}(f_{3},\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1}))
PreCat(i)\mathord {\textnormal {\textsf {PreCat}}}(i)の要素を(階数iiの)前圏(precategory)と呼ぶ。

射の型Map(x1,x2)\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})は集合であると要請される。これは、群の定義([004W])においてCarrier\mathord {\textnormal {\textsf {Carrier}}}は集合としたのと同様である。対して、Obj\mathord {\textnormal {\textsf {Obj}}}は集合とは限らない。

[005D] 記法

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏とする。xxCCの対象であることをx:C.Objx:C.\mathord {\textnormal {\textsf {Obj}}}の代わりに単にx:Cx:Cと書く。対象x1,x2:Cx_{1},x_{2}:Cに対して、C.Map(x1,x2)C.\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})の代わりに単にMap(x1,x2)\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})と書く。x1:Cx_{1}:Cと書いた時点でCCの前圏の構造が暗黙に了解されるのでこの表記で曖昧性はない。同様に、対象x:Cx:Cに対して、C.id{x}C.\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace の代わりに単にid{x}\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace と書く。合成comp(f2,f1)\mathord {\textnormal {\textsf {comp}}}(f_{2},f_{1})は二項演算子を使ってf2f1f_{2}\circ f_{1}と書く。

[006H]

関数外延性を仮定する。iiを階数とする。前圏Set(Cat)(i):PreCat(succ(i))\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i):\mathord {\textnormal {\textsf {PreCat}}}(\mathord {\textnormal {\textsf {succ}}}(i))を次のように定義する。

  • -Obj{A:U(i)IsSet(A)}\mathord {\textnormal {\textsf {Obj}}}\equiv \lbrace A:\mathcal {U}(i)\mid \mathord {\textnormal {\textsf {IsSet}}}(A)\rbrace
  • -Mapλ(A,B).(AB)\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (A,B).(A\to B)
  • -恒等射は[0010]、合成は[0011]による。
  • -[0048]より、各Map(A,B)\mathord {\textnormal {\textsf {Map}}}(A,B)は集合である。
  • -他の公理は自明である。

[006N]

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏とする。前圏Op(C):PreCat(i)\mathord {\textnormal {\textsf {Op}}}(C):\mathord {\textnormal {\textsf {PreCat}}}(i)を次のように定義する。

  • -ObjC.Obj\mathord {\textnormal {\textsf {Obj}}}\equiv C.\mathord {\textnormal {\textsf {Obj}}}
  • -Mapλ(x1,x2).C.Map(x2,x1)\mathord {\textnormal {\textsf {Map}}}\equiv \lambda (x_{1},x_{2}).C.\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})
  • -idλx.C.id{x}\mathord {\textnormal {\textsf {id}}}\equiv \lambda x.C.\mathord {\textnormal {\textsf {id}}}\lbrace x\rbrace
  • -compλ(x1,x2,x3).λ(g:Map(x2,x3),f:Map(x1,x2)).C.comp(f,g)\mathord {\textnormal {\textsf {comp}}}\equiv \lambda (x_{1},x_{2},x_{3}).\lambda (g:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3}),f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})).C.\mathord {\textnormal {\textsf {comp}}}(f,g)
  • -前圏の公理はCCのそれから分かる。

前圏CCの対象の間には、同一視型の他に同型という同一視の概念が考えらる。

[005E] 定義

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏、x1,x2:Cx_{1},x_{2}:Cを対象、f:Map(x1,x2)f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})を射とする。

  • -LInv(f):U(i)\mathord {\textnormal {\textsf {LInv}}}(f):\mathcal {U}(i)Record{ ⁣inv:Map(x2,x1),id:invf=id ⁣}\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1}),\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {inv}}}\circ f=\mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }と定義する。
  • -RInv(f):U(i)\mathord {\textnormal {\textsf {RInv}}}(f):\mathcal {U}(i)Record{ ⁣inv:Map(x2,x1),id:finv=id ⁣}\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {inv}}}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1}),\mathord {\textnormal {\textsf {id}}}:f\circ \mathord {\textnormal {\textsf {inv}}}=\mathord {\textnormal {\textsf {id}}}\mathclose {|\negmedspace \} }と定義する。
  • -IsIso(f):U(i)\mathord {\textnormal {\textsf {IsIso}}}(f):\mathcal {U}(i)Record{ ⁣linv:LInv(f),rinv:RInv(f) ⁣}\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {linv}}}:\mathord {\textnormal {\textsf {LInv}}}(f),\mathord {\textnormal {\textsf {rinv}}}:\mathord {\textnormal {\textsf {RInv}}}(f)\mathclose {|\negmedspace \} }と定義する。
IsIso(f)\mathord {\textnormal {\textsf {IsIso}}}(f)の要素がある時、ff同型(isomorphism)であるという。

[005G] 補題

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏、x1,x2:Cx_{1},x_{2}:Cを対象、f:Map(x1,x2)f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})を射とする。次は論理的に同値である。

  1. 1ffは同型である。
  2. 2任意の対象y:Cy:Cに対して、関数λg.fg:Map(y,x1)Map(y,x2)\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(y,x_{1})\to \mathord {\textnormal {\textsf {Map}}}(y,x_{2})は同値である。
  3. 3任意の対象y:Cy:Cに対して、関数λg.gf:Map(x2,y)Map(x1,y)\lambda g.g\circ f:\mathord {\textnormal {\textsf {Map}}}(x_{2},y)\to \mathord {\textnormal {\textsf {Map}}}(x_{1},y)は同値である。

証明

1から2を示す。定義から、関数λg.fg:Map(y,x1)Map(y,x2)\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(y,x_{1})\to \mathord {\textnormal {\textsf {Map}}}(y,x_{2})は両側可逆であることが分かる。よって、[004K]よりこれは同値である。

2から1を示す。λg.fg:Map(x2,x1)Map(x2,x2)\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})\to \mathord {\textnormal {\textsf {Map}}}(x_{2},x_{2})が同値なので、射h:Map(x2,x1)h:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{1})と同一視p:fh=idp:f\circ h=\mathord {\textnormal {\textsf {id}}}を得る。関数λg.fg:Map(x1,x1)Map(x1,x2)\lambda g.f\circ g:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{1})\to \mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})が同値なので、同一視

fhff\circ h\circ f== {pp}ff== {前圏の公理}fidf\circ \mathord {\textnormal {\textsf {id}}}
から同一視q:hf=idq:h\circ f=\mathord {\textnormal {\textsf {id}}}を得る。よって、ffは同型である。

13の同値性も同様である。

[005H] 命題

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏、x1,x2:Cx_{1},x_{2}:Cを対象、f:Map(x1,x2)f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})を射とすると、型IsIso(f)\mathord {\textnormal {\textsf {IsIso}}}(f)は命題である。

証明

[0041]より、ffが同型であると仮定してIsIso(f)\mathord {\textnormal {\textsf {IsIso}}}(f)が可縮であることを示せばよいが、これは[005G]からすぐに従う。

[005F] 定義

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏、x1,x2:Cx_{1},x_{2}:Cを対象とする。型x1x2:U(i)x_{1}\cong x_{2}:\mathcal {U}(i){f:Map(x1,x2)IsIso(f)}\lbrace f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\mid \mathord {\textnormal {\textsf {IsIso}}}(f)\rbrace と定義する。

同型の基本性質は次のようにまとめられる。

[006X] 命題

iiを階数、C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)を前圏とする。

  1. 1任意の対象x:Cx:Cに対して、恒等射id:Map(x,x)\mathord {\textnormal {\textsf {id}}}:\mathord {\textnormal {\textsf {Map}}}(x,x)は同型である。
  2. 2任意の対象x1,x2,x3,x4:Cx_{1},x_{2},x_{3},x_{4}:Cと射f1:Map(x1,x2)f_{1}:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})f2:Map(x2,x3)f_{2}:\mathord {\textnormal {\textsf {Map}}}(x_{2},x_{3})f3:Map(x3,x4)f_{3}:\mathord {\textnormal {\textsf {Map}}}(x_{3},x_{4})に対して、f2f1f_{2}\circ f_{1}f3f2f_{3}\circ f_{2}が同型ならば、f1f_{1}f2f_{2}f3f_{3}f3f2f1f_{3}\circ f_{2}\circ f_{1}も同型である。

証明

1は定義からすぐに確かめられる。2[005G][002F]による。

とは、前圏であって対象の間の同型の型と同一視型が同値になるようなものである。

[005I] 定義

iiを階数とする。

  • -前圏C:PreCat(i)C:\mathord {\textnormal {\textsf {PreCat}}}(i)に対して、型IsCat(C):U(i)\mathord {\textnormal {\textsf {IsCat}}}(C):\mathcal {U}(i)
    x:CIsContr(y:Cxy)\prod _{x:C}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{y:C}x\cong y)
    と定義する。
  • -Cat(i):U(succ(i))\mathord {\textnormal {\textsf {Cat}}}(i):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i)){C:PreCat(i)IsCat(C)}\lbrace C:\mathord {\textnormal {\textsf {PreCat}}}(i)\mid \mathord {\textnormal {\textsf {IsCat}}}(C)\rbrace と定義する。
Cat(i)\mathord {\textnormal {\textsf {Cat}}}(i)の要素を(階数iiの)圏(category)と呼ぶ。

CCを圏とすると、恒等射は同型なので[001S]を適用できて、同値

x1,x2:C(x1=x2)(x1x2)\prod _{x_{1},x_{2}:C}(x_{1}=x_{2})\simeq (x_{1}\cong x_{2})
を得る。逆に、前圏CCが圏であることを示すにはこのような同値を構成すれば十分である。

圏の典型例として、Set(Cat)(i)\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i) ([006H])が圏であることを見る。

[006I] 補題

関数外延性を仮定する。iiを階数、A,B:Set(Cat)(i)A,B:\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)を対象、f:Map(A,B)f:\mathord {\textnormal {\textsf {Map}}}(A,B)を射とする。次は論理的に同値である。

  1. 1ffSet(Cat)(i)\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)の射として同型である。
  2. 2ffは関数として同値である。

証明

[004K]による。

[006J] 定理

関数外延性と一価性を仮定する。iiを階数とすると、Set(Cat)(i)\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)は圏である。

証明

対象A,B:Set(Cat)(i)A,B:\mathord {\textnormal {\textsf {Set}}}^{(\mathord {\textnormal {\textsf {Cat}}})}(i)に対して、[006I]より(AB)(AB)(A\cong B)\simeq (A\simeq B)を得て、一価性と[0049]より(AB)(A=B)(A\simeq B)\simeq (A=B)を得る。