ホモトピー型理論
[000J] 記法

  • -\to は右結合の演算子である。例えば、ABCA\to B\to CA(BC)A\to (B\to C)と読む。
  • -λx1.λxn.b\lambda x_{1}.\dots \lambda x_{n}.bλ(x1,,xn).b\lambda (x_{1},\dots ,x_{n}).bと略記することがある。
  • -f(a1)(an)f(a_{1})\dots (a_{n})f(a1,,an)f(a_{1},\dots ,a_{n})と略記することがある。
  • -x:A\prod _{x:A}の結合は弱い。例えば、x:Ay:BCD\prod _{x:A}\prod _{y:B}C\to Dx:A(y:B(CD))\prod _{x:A}(\prod _{y:B}(C\to D))と読む。