命題の文脈の擴張
存在量化$ \dashv文脈の擴張$ \dashv普遍量化
$ \exist_W\dashv W^*\dashv\forall_W:{\cal H}\xrightarrow{W^*}{\cal H}/W
$ (\exist_{w\in W};W^*)\dashv(\forall_{w\in W};W^*):{\cal H}/W\to{\cal H}/W
$ Q\vdash_\Gamma\forall w_{:W}P(x)iff.$ Q\vdash_{\Gamma,w:W}P(x)
$ \exist w_{:W}P(x)\vdash_\Gamma Qiff.$ P(x)\vdash_{\Gamma,w:W}Q
依存和$ \dashv文脈の擴張$ \dashv依存積
$ \prod_{w:W}\dashv\_\times W\dashv\sum_{w:W}:{\cal H}/\Gamma\xrightarrow{\_\times W}({\cal H}/\Gamma)/W