∞-グルーポイド - pogi-log

∞-グルーポイド

∞-グルーポイド(∞-groupoid、infinity groupoid)

∞-グルーポイドは群と亜群(グルーポイド)を∞-圏に一般化したもの

高次元圏に関係ある

高次グルーポイドという分類にもなる

(∞, 0)-categoryと等価らしい

Homotopy Type Theory(HoTT)では型は∞-グルーポイドとして扱われるとのこと

HoTTで∞-グルーポイドとして扱う型のことをホモトピー型(homotopy type)と呼ぶ？(要調査)

k-射(k-morphism)というものが出てきて、これは0～∞の射の型を定義してそう

→ 基本グルーポイド

弱∞-グルーポイド

HoTTの∞-グルーポイドに関連する文献

『Homotopy Type Theory: Univalent Foundations of Mathematics』

Weak omega-categories from intensional type theory

Types are weak ω-groupoids

確認用

Q. ∞-グルーポイド

関連

『Homotopy Type Theory 入門』

(∞, 1)-category

コヒーレンス則

単体的集合

高次トポス論

参考

infinity-groupoid

Leanのzulipchatでの∞-groupoidの言及について

『高次元圏入門』

メモ

Jacob Lurie, Section 1.1.2 in: Higher Topos Theory, Annals of Mathematics Studies 170, Princeton University Press 2009 (pup:8957, pdf)

∞-groupoid は空間である～Joyal の拡張定理の応用とその証明～ | Mathlog

高次グルーポイド構造

k-morphism in nLab

#数学 #ホモトピー型理論