6.4 functor の定義

次に，functor の定義ですが，例えば2変数の functor を考えましょう．集合（set）X,Yから，Zという新しい集合を作りだしたいとします．このときどうするかという話をします．



      X ∩ Y -> Z
 


      set set   set



  definition



   let  X , Y  be set;



   func X ∩ Y -> set



   means



   :N: x ∈ it iff



      x ∈ X & x ∈ Y;



   existence ......;



   uniqueness



   proof



   end;



  end;

この場合も，f （X,Y）=Z という関数定義でなく，オペレーションの形で書けます．Z=X ∩ Y，こういう記号を定義したいとします．集合 X と集合 Y からあたらしい集合 Z を作り出す，それがまさにこの functor です．let X,Y be set; で，集合 X ，Y を用意して，これも reserve してあれば be set は必要ありませんが，そして，func X ∩ Y -> set で，X ∩ Y が set であるということを表わしています．means の次の行が，その functor の意味です．先程と同じ様にラベルをつけて，functor の意味を書きます．この意味中で，X ∩ Y を it と置きます．

そして，証明部（意味の内容）では, existence （存在）と uniqueness|（ユニーク）の証明をしなければいけません．存在して，かつユニークであることをいわなくてはいけないわけです．

uniqueness の証明のしかたですが，以下のことを言えばいいわけです．

it として A1，A2 を取ってくると，

x ∈ A1 <=> x ∈ X　& x ∈ Y

x ∈ A2 <=> x ∈ X & x ∈ Y

A1 = A2

これを書くと，



      uniqueness



       proof



        let A1,A2 be set such that



          A1: x ∈ A1  iff  x ∈ X  &  x ∈ Y



          and



          A2: x ∈ A2  iff  x ∈ X  &  x ∈ Y;



          now let y;



           y ∈ A1 iff y ∈ X  &  y ∈ Y  by A1;



           hence y ∈ A1  iff  y ∈ A2  by A2;



          end;



         hence A1=A2 by TARSKI:2;

というふうになります．つまり，この条件をみたす集合2つ A1，A2 をとってくると，実はそれらは等しいということを証明することで uniqueness を証明したことになります．

この uniqueness の証明の中で，まず，3行目に such that がありますから，そのあとに2つの文，ラベル A1 文とラベル A2 文が and で結ばれていることがわかります．そして，now let y となっています．この y は Any であることが reserve されているとします．そして，ラベル A1 より，y ∈ A1 iff y ∈ X & y ∈ Y であることが言えて，さらに，このこととラベル A2 より，y ∈ A1 iff y ∈A2 であることが言えるわけです．そして，A1=A2 であるための必要十分条件は任意の y に対して，y ∈ A1 と y ∈ A2 が同値であるという，TARSKI:2 より，A1=A2 が証明されたわけです．

existence も同様に証明しなければいけないのですが，こういう it が存在するということを言わなければならないのです．