同一視型 - pogi-log

同一視型

#Fleeting_Notes

同一視型(identity type)

$ \mathrm{Id}_A : A \to A \to \mathcal{U}

$ \mathcal{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(英)