| ホムセット | アノテーション |
|---|---|
| Map(-, -) | map, function |
| ParMap(-, -) | par-map, partial |
| NDMap(-, -) | nd-map, nondet |
| Rel(-, -) | rel, relation |
ホムセットを“対象としての集合〈set as object〉”とみなす行為を[+レイフィケーション]と言う。[/レイフィケーション]したことを示すために、ホムセットを中括弧〈ブレイス〉で囲む。以下の `function` はアノテーション。
- f ∈Map(RelLable, {Rel(Label, Item)})
- f:RelLabel → {Rel(Label, Item)} function
[/コアージョン〈キャスト〉]は、ホムセットを小文字にした名前で行う。
- (:ndmap f) ∈NDMap(X, Y) アップキャスト
- (:rel f) ∈Rel(X, Y) アップキャスト
- (:map r) ∈Map(X, Y) ダウンキャストは失敗するかも知れない
(:map ) ダウンキャストが成功する条件は：
- r:X → Y relation, total, univalent
ダウンキャストとアップキャストの組がEPペアのとき、[+コアージョンペア =: コアージョン・ペア]と呼ぶ。
