$`\Gamma \mapsto \psi : T`$ が判断のとき、コンテキストのラベル〈名前〉をすべて取り除いたものを $`\widehat{\Gamma}`$ とする。プロファイルは：$`\quad \widehat{\Gamma}\to T`$$`f := \big\langle \Gamma \mapsto \psi : T\big\rangle`$ が定義のとき…

圏論 型理論 論理 メタ論理 指数 [_, _] [_→_], → ⇒, → (⇒) 項の定義 |→ |→, |- |-, |→ (|-) プロファイル → →, ~~> →, ~~> (→) ホムセット {_→_} {_→_}, {_~~>_} {_→_}, {_~~>_} {_(→)_}