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

∞-グルーポイド

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

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

高次元圏に関係ある

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

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

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

∞-グルーポイドは(∞, 0)-category？

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

→ 基本グルーポイド

弱∞-グルーポイド

関連文献

『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の言及について

『高次元圏入門』

メモ

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

高次グルーポイド構造

k-morphism in nLab

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