ドクトリンは、CCCのような、Cat上の具象圏だとする。ハイパードクトリンは拡張されたドクトリンくらいの意味だが、 ベース圏（論域の圏）の上のインデックス付き圏であり、余域はCCCのようなドクトリンになる。 ベース圏の射に対して、ΣΔΠ随伴性がある。Σは…

ハイパードクトリン インスティチューション ベース対象 型コンテキスト 指標 ベース射 コンテキスト拡張／置換 指標射 ファイバー 命題の圏 モデルの圏 誘導関手 引き戻し リダクト関手 随伴関手 限量子 - 妥当性 - 充足関係 こうして見ると、限量子随伴性…

カリー／ハワード対応を信じるなら、関数の記述と定理の証明はまったく同じはず。だったら同じ書き方ができるはず。 // f:X×Y→Z function f given x:X, y:Y ensures Z begin ... end // t:A∧B→C theorem t given a:A, b:B ensures C begin ... end関数定義に…

管理・配布のメカニズム パッケージ バージョン（パッケージに付く） スクリプト（物理的にはファイル、拡張子は.tenjinscript） モジュール（スクリプトに制限を付けたもの、拡張子は.tenjin） リポジトリ インターネット上でパッケージを保存している場所 …

定理記述 - 檜山正幸のキマイラ飼育記 メモ編の続き。少し変える。 theorem 定理の名前 import モジュール1, モジュール2 for 宣言1, 宣言2 given 命題1, 命題2 ensures 命題 begin 証明 end endproofという語は避けた。 圏論 論理 始対象 False 終対象 True…