圏論に関して質問があります。 種々の圏の存在はどのようにして主張されますか？

例えば、公理的集合論では、論理式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