>>405
>>>372のカンファレンスのAbstractsによると、ZFCGとかではなくunivalent foundationsみたいだぞ？

(参考)追加
https://uemurax.github.io/notes/ctac-2022.html
Taichi Uemura
「正しい」圏論
この文書は圏論 Advent Calendar 2022の17日目の記事です。
概要
「正しい」圏の定義を紹介します。主に (Ahrens et al., 2015) と (HoTT Book; 9章) の内容です。
はじめに
まずは圏の定義を確認しましょう。圏 C とは次の要素からなる構造です。

対象のなす集合 Object C
対象 x : Object C と y : Object C に対し、射のなす集合 Map C x y
恒等射、合成、単位律、結合律
この定義は「正しい」でしょうか。もちろん正しいのですが、少し微妙な点があります。それは圏がどう同一視されるかです。圏に対しては少なくとも4つの同一視の概念が考えられます。

メタ理論における標準的な同一視の概念 (例えば集合論では集合としての等しさ)
代数構造としての同型 (圏同型)
圏同値 (合成が恒等関手と自然同型という意味で逆関手を持つ)
弱圏同値 (充満忠実かつ本質的全射)
流石に集合としての等しさを論じることはないと思いますが、圏同型はしばしば登場します。群同型、環同型などから類推できる自然な概念です。「正しい」圏の同一視のしかたはもちろん圏同値です。圏同値と弱圏同値は同値ですが、それはあくまで定理なのでいったん区別しておきます。圏同値が「正しい」圏の同一視のしかたというのは、あらゆる「圏論的」な構成は圏同値で不変ということです。しかし、圏同値より強い同一視のしかたがあるということは、圏同値で不変でないような「圏論的」ではない構成もあるということです。理想としては「圏論的」な構成のみを使って「正しい」圏論をしたいところですが、現実では「圏論的」ではない構成も多用されています。 2-圏論とか。

もう一つ微妙な点があります。圏同値と弱圏同値の同値性を示すには選択公理を使います。これは同型を除いて一意な対象を選択する必要があるからです。しかし、同型を除いてとはいえ一意な対象を選択するというは不自然な話です。また、具体的な圏同値を思い浮かべると、本質的全射の証明では具体的な構成が与えられることがほとんどです。圏論に選択公理が要るはずがありません。

メタ理論: Univalent Foundations
この文書では Univalent Foundations (HoTT Book) をメタ理論として採用します
略す