\(f:\prod _{\lbrace x:A\rbrace }\prod _{y:B}C\)のように引数を\(\lbrace \phantom {x}\rbrace \)で囲った場合、その引数は暗黙的(implicit)であると約束する。つまり、要素\(a:A\)と\(b:B[x\mapsto a]\)に対して、関数適用を\(f(a,b)\)の代わりに\(a\)を省略して\(f(b)\)と書く。\(B\)の構成で\(x\)を明示的に使う場合には実用上は曖昧性は無い。暗黙的な引数\(a\)だけを適用したい場合は\(f\lbrace a\rbrace :\prod _{y:B[x\mapsto a]}C[x\mapsto a]\)と書く。