[logic-ml] homotopy type theory

[logic at math.tsukuba.ac.jp]

> 圏論に関して質問があります。
> 種々の圏の存在はどのようにして主張されますか？
>
> 例えば、公理的集合論では、論理式f(x),集合Xに関して、Xの元xでf(x)を満たすもの
> から成る集合{x \in X|f(x)}が存在することが分出公理によって言えますが、圏論に
> おいても、圏の存在を主張する公理群が定められていますか？
>

上記のような質問をいただいていますが、
これはこの質問者以外の広い範囲の方に
関心があることと思われますので、
ここにお答えします。質問者の名前等は
削除してあります。

まず質問を

Homotopy type theoryはZFCにかわる数学の基礎づけに
なるという話であるが、集合論はたとえばComprehensionの
ような豊かな構成原理をもっているが、HTTはどうなのか？

と変形させていただきます。

まずHTTのなかではn-typeというHierarchyが定義されます。
ｎは−２以上の整数です。これはHomotopy theoryから借用された
概念で、n-typeというのはｎを越える次元ではhomotopicalにはtrivialで
あることを意味します。Homotopy theoryの言葉づかいで言うならば、
ｎを越える次元のhomotopy groupsはすべてtrivialであることを
意味します。０-typeがいわゆるsetで、ここに話を限定するならば
comprehensionをはじめとする集合論的構成はだいたい
そのまま行えます。

一般にはdependent function typeやdependent pair typeという
構成原理を最初から内臓していますが、これだけではもちろん
足りません。HTTがもつ強力な構成原理はinductionで、特に
higher inductionが重要な役割を演じます。計算機言語のCOQや
AGDAは通常にinductionを組み込んでいますが、higher inductive typesは
まだ持っておりません。少しslogan的な言い方を許していただければ、
inductive typesはfree monadsに、higher inductive typesはmonadsの
表現に対応します。

Inductiveな構成のいい例はCauchy realsの構成です。自然数から有理数を
作るのは、古典的な話とあまりかわりません。それで有理数から実数を
作るには、Dedekindのやり方とCauchyのやり方がありますが、後者の
構成をinductiveにやるとどうなるかが、

https://homotopytypetheory.org/book/

の１１．３節に縷説されています。あるいはcirclesやspheresやsuspensionsは
どのようにinductiveに構成されるか、第６章に縷説されています。
是非ご覧になってください。

にしむら
筑波大学
数学

追伸：オマケです。手持無沙汰な折にどうぞ。

https://www.youtube.com/watch?v=VY01dVHvlFE