型をホモトピー的に扱う
#🌱
型を
∞-グルーポイド
として扱う
ホモトピー型
ホモトピー的な解釈だと、二つの項
$ a, b : A
があったときに、
$ a = b
はaからbへの道(path)pが存在する風な見方になる
ホモトピカル(homotopical)な同一視(identification)をすると
$ A \simeq B
これは
ホモトピー同値
#Homotopy_Type_Theory(HoTT)