定義と仕様

次のようなシーケントスタイルの定義は、

For C in Cat, D in 0Cat
For FO : C.Obj → D.Obj in Set
For FM(A, B in C.Obj) : C(A, B) → D(FO(A), FO(B)) in Set
Define
  F : C → D in Cat // F is-a-functor
  :⇔
  F = (FO, FM)
  SuchTaht
  ...
End

仕様としてまとめられる。

specification functor := {
 dom in 0Cat as C,
 cod in 0Cat as D,
 obj-part : C.Obj → C.Obj in Set as FO,
 hom-part(A, B in C) : C(A, B) → D(FO(A), FO(B)) as FH,
! laws
 ...
}

仕様と定義は同じだが、仕様のほうがモジュール化されている。