入れ子になった指標と構成

親子関係で入れ子になった指標＝ジニアロジーの書き方はまだ試行錯誤だけど、ともかくも、いくつかの論理的概念の定義を試みる。

3-signature {
 sort LoicalCat

 2-signature {
  /* Cは論理的圏の構造を持った圏
     Cでは、対象定数_Bや指数ベキが意味を持つ。
  */
  sort C in LogicalCat

  signature proposition, 命題, 真偽 {
   p:_1→_B
  }
  signature predicate, 述語, "propositional function", 命題関数 {
   sort X in C
   operation p:X→_B in C
  }

  signature "logical connective", 論理結合子, "truth function", 真理関数 (value n:_1→_N){
   opertion p: _B^n→_B in C
  }
 }
}

法則とは何かを示唆する指標と構成。インデントなしで書いている。

3-signature {
 sort CartCat
2-signature {
 /* Cはデカルト圏 */
 sort C in CartCat

signature PointedMagma {
 sort X in C
 operation m:X×X→X in C
 operation a:_1→X in C
}

constructin LeftUnitLaw from PoitedMagma to predicate {
 X := X
 p := λx∈X.(eq(m(i, x), x))
}

constructin LeftUnitLaw2 from PoitedMagma to proposition {
 p := ∀x∈X.(eq(m(i, x), x))
}

}
}

親子関係で入れ子になった指標や構成の書き方としてダブルギュメも使ってみる。

《3-sort CartCat |
  《2-sort C in CartCat |
    《1-sort X in C, 1-operation m:X×X→X in C, 1-operation a:_1→X in C |
        1-sort X := X in C
        1-operation p:X→_B := λx∈X.(eq(m(i, x), x)) in C
     》
   》
》

大きなラムダ式を含めて、ダブルギュメは何らかの構成の記述で、コンテキスト部がソース指標、ターゲット指標は暗黙に指定される。