$`f`$ のフルカリー化を $`f^\wedge`$ として次が意味的には同じであること。 $`f(a_1, \cdots, a_n)`$ $`f^\wedge(a_1) \cdots (a_n)`$ $`(\cdots(f^\wedge\triangleleft a_1) \cdots )\triangleleft a_n`$ $`f^\wedge\: a_1\: \cdots\: a_n`$ これをストリ…

https://www.cs.vu.nl/~jbe248/lv2017/10x4.pdf より：the {type checking | proof verification} problem Γ |-? t:A the {typability | type {synthesis | inference}} problem Γ |- t:? the {{type | proposition} inhabitation | proposition provability…

コンテキストと指標は、構文的には区別できないのだが、次の違いがある。 指標はインスティチューション的な意味での指標である。 指標のあいだの射は指標射で、モデル圏のあいだのリダクト関手を定義する。 コンテキストは、固定した指標に対する構文的圏の…