named objectの呼び名と書き方

name	object	呼び名	圏論
変数名	型	型宣言	指標対象成分
関数名	項	関数	指標射成分
ラベル	命題	表明	論理対象
定理名	証明	定理	論理射

名前の宣言

name	宣言	名前のソート	ソート式
変数名	var x:X	型	型項
関数名	function f:(x:X, y:Y)->Z	プロファイル	型項のフォーク
命題名	proposition P :(x:X, y:Y)	論域	型項のタプル
定理名	theorem t: (p:P, q:Q)->R	ステートメント	論理式のフォーク

名前へのバインディング

name	バインディング	右辺
変数名	x := a	閉項
関数名	f := t	項
命題名	P := F	論理式
定理名	t := p	証明記述