順序対の定義

任意の$x,y$に対して

$$\{ \{ x,y \}, \{ x \} \}$$

を$[x,y]$で表すことを$x,y$から$[x,y]$を作り出す $functor$(作用）として定義します。

 definition let x,y;
  func [x,y] equals :Def5:
   { { x,y }, { x } };
  coherence;
 end;
canceled;