ホモトピー型理論
[002P] 演習

\(i\)を階数、\(A:\mathcal {U}(i)\)を型、\(a_{1},a_{2}:A\)を要素、\( p:a_{1}=a_{2}\)を同一視とする。同一視\(\mathord {\textnormal {\textsf {unit-l}}}( p):\mathord {\textnormal {\textsf {refl}}}\circ p= p\)\(\mathord {\textnormal {\textsf {unit-r}}}( p): p= p\circ \mathord {\textnormal {\textsf {refl}}}\)を構成せよ。