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

∞-グルーポイド

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

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

高次元圏に関係ある

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

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

グルーポイドは射が可逆(同型射)

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

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

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

→ 基本グルーポイド

k-射（1 ≤ k ≤ n）が可逆

日本語で読めるHoTTにおける高次グルーポイドは下記をとりあえず見る

高次グルーポイド構造 -- ホモトピー型理論

0-グルーポイド

対象: 対象(= 集合の要素)

射: なし

等しさ: 同一性のみ

1-グルーポイド

対象:

n-グルーポイド

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

『Homotopy Type Theory: Univalent Foundations of Mathematics』

Weak omega-categories from intensional type theory

Types are weak ω-groupoids

infinity-groupoid

確認用

Q. ∞-グルーポイド

関連

弱∞-グルーポイド

(∞, 1)-category、圏Grpd、∞Grpd

コヒーレンス則

単体的集合

高次トポス論

『Homotopy Type Theory 入門』

参考

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

#無限圏論 #高次元圏

#ホモトピー型理論