同一視型
#Fleeting_Notes
同一視型(
identity type
)
$ \mathrm{Id}_A : A \to A \to \mathscr{U}
$ a = b
は
$ \mathrm{Id}_A(a,b)
と書ける
$ a =_A b
のようにも書ける
propositionally equal
同一視を
identification
$ \mathrm{refl} : \prod_{a:A}(a =_A b)
$ \mathrm{refl}
は反射律(reflexivity)
確認用
Q. 同一視型
関連
Propositions as Types
propositional equality
judgmental equality
メモ
同一視型 -- ホモトピー型理論
『Introduction to Homotopy Type Theory』
『ホモトピー型理論』上村 太一
同一視型 -- ホモトピー型理論
1.12 Identity types
調査用
Google.icon
同一視型(日)
Google.icon
identity type(日)
Google.icon
Identity type(英)
Wikipedia.icon
同一視型 - Wikipedia(日)
同一視型(検索) - Wikipedia(日)
Wikipedia.icon
Identity type - Wikipedia(英)
Identity type(検索) - Wikipedia(英)