プレ圏（グラフ上に部分的な圏構造）の圏をPrecatとする。さらに、プレ圏に同値関係（一般化合同）が与えられたものを(P, E)として、その全体をEPrecatとする。EPrecatは有限余完備だと期待している。EPrecatが有限余完備ならその上の余スパンの圏が作れる。…

パラメータ付き指標／セオリー（仕様モジュール）とCafeOBJのprotected importって同じような気がする。インポートって余スパンで説明されるような。

どう違う？ 同じような気もするが。