「ローヴェア」のほうが近いので、「ローヴェア」にする。 https://ja.forvo.com/word/william_lawvere/ https://ja.wikipedia.org/wiki/%E3%82%A6%E3%82%A3%E3%83%AA%E3%82%A2%E3%83%A0%E3%83%BB%E3%83%AD%E3%83%BC%E3%83%B4%E3%82%A7%E3%82%A2

ステイ／メレディス(↓)から辿って、主にローヴェル・セオリー関係の文献。 Logic as a distributive law Mike Stay, Lucius Gregory Meredith 17p https://arxiv.org/abs/1610.02247 ステイ／メレディス(↑)が参照しているもの。まずはハイランド／パワー： T…

匿名性、非差別性 - 檜山正幸のキマイラ飼育記 メモ編の続き。環境依拠主義（って言葉が適切な気はしないが）は、要素還元主義とは違う（たぶん対極的）。なぜなら、対象（圏論の意味での対象でもあり、一般的な語彙としての対象でもある）を解体（分解、腑…

要素還元主義と環境依拠主義 - 檜山正幸のキマイラ飼育記 メモ編の続き。nLab記事 https://ncatlab.org/nlab/show/principle+of+equivalence の同値性原理〈principle ofequivalence〉は、 リスコフの置換原則 「インターフェイスに対してプログラミングせよ…

仏教 大乗仏教中観派と一般モデル理論 - 檜山正幸のキマイラ飼育記 スノーグローブ スノーグローブ現象 再び - 檜山正幸のキマイラ飼育記 マイクロコスモ原理 マイクロコスモ原理の恐怖 - 檜山正幸のキマイラ飼育記 入れ子 入れ子の世界が大好きだけど怖い -…

ステイ／メリディスの次の論文、とても良い。 Title: Logic as a distributive law Author: Mike Stay, Lucius Gregory Meredith URL: https://arxiv.org/abs/1610.02247 僕がふだん考えていることだから、問題意識が一致して分かりやすい。本論じゃないとこ…

困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 で述べたこと： 自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出…

"Monoidal Topology, A Categorical Approach to Order, Metric and Topology" 508ページのPDF http://sweet.ua.pt/dirk/artigos/HST14_Monoidal_topology_A_categorical_approach_to_order_metric_and_topology.pdf モノイド概念がトポロジーにも使える、と…

本編で書いた米田モナドだが、 http://d.hatena.ne.jp/m-hiyama/20180110/1515553121 次の論文にほとんど書いてある。 https://arxiv.org/abs/1612.03678 上記本文では、単に前層モナドと言っている。台が前層関手だから。前層モナド＝米田モナドは、PSh:Cat…

今まで、指標はコンピュータッドの同義語としてきたが、どうも違う。その違いは指標は名前（ラベル）があること。単なるグラフとラベル付きグラフの違い。2つの指標をとると、まったく無関係とは限らない。ラベリングによって、必然的にスパン構造＝貼り合わ…

宣言（名前のプロファイリング）と定義（束縛、名前のアタッチング）をゴッチャに混ぜて書いた形式をミクスチャと呼ぶことにする。 mixture Succ := { type X; X := int; value e: X; function succ : X->X }これはミクスチャの例。同じ名前に対して、「宣言…

シャドーイングの問題 - 檜山正幸のキマイラ飼育記 メモ編の続き。入れ子 Σ | Δ があるとき、シャドーイングがあろうとなかろうと、Σ←Σ'→(Σ' + Δ) ができる。この事実から、一段階の入れ子はスパンで表現できることがわかる。一般のスパンではなくて、両脚が…

まず、nLabのカン拡張項目： https://ncatlab.org/nlab/show/Kan+extension Proposition 2.8. Let C be a small category; D have all small limits. Then the right Kan extension of a functor F:C→D of locally small categories along a functor p:C→C' …

あれ、これって指標のラムダ計算に役立つぞ。 「確率変数」の一般論は可能か - 檜山正幸のキマイラ飼育記

等値的圏と同値的的圏 k-等値的圏〈k-equational category〉は、k≦n であるn-射がすべて恒等になってしまう圏。 0-等値的圏： 0-射がすべて恒等？ 対象がすべて恒等？ うーん？？ 空集合か単元集合のことだ。よって、0-等値的圏の全体はブール集合になる。 1…

ユグドラシル・エクスプローラー - 檜山正幸のキマイラ飼育記 メモ編の続き。ワールドのなかにある項目を、ミクロ項目とマクロ項目に分けたほうがいい。 マクロ項目： 項目なので区分〈division〉、プロファイル、名前を持つが、名前だけでなくて、名前に関…

https://ncatlab.org/nlab/show/transfor トランスフォー〈変換手〉はワールドの項目として必要となる。nとkで、k≦n に対して (n, k)-トランスフォーが定義できる。 (0, 0)-トランスフォーは写像〈map〉 (1, 0)-トランスフォーは関手〈functor〉 (1, 1)-トラ…

ユグドラシル “ユグドラシル”は、Coqのuniverseの話を読んだ時連想した。 エクスプローラー ブラウザと言ってもいいんだけど、“エクスプローラー”のほうが探索・探検・究明の意味があるから。 我々が何かするときの文脈を世界〈world〉と呼んでしまおう。世…

ハイパーインスティチューションの目指すところは、an overall framework for computing and logic だ。主要な道具は indexed/fibred/parametrized computads だ。アイディアの源泉は、hyperdoctrineとinstitution。

プログラミングとの対応 プログラミング ハイパーインスティチューション インターフェイス 指標 インターフェイスのハード実装 モデル インターフェイスのソフト実装 指標への射 インターフェイス上のプログラム 指標からの射 インターフェイスのアダプター…

基本的な概念と用語： まだ曖昧な所があるが、 区分〈くぶん | division | ディヴィジョン〉： 特定の圏Cと次元数kのペア。Cのk-射の集合を意味する。 区分ラベル： 区分に付ける人間可読なテキスト。 区分け〈くわけ | divisioning | ディヴィジョニング〉 …

ハイパーインスティチューションは、3×3のマトリックスで整理できる。縦横どう書くかは自由だが、3ロール×3レイヤーと呼ぶ。 ロール： ベース（Base）ロール、論理（Logi）ロール、モデル（Mode）ロール レイヤー： アンビエント（Ambi）レイヤー、計算（Com…

圏論的な世界〈world〉を次のようなものだとする。 世界の構成素を領地〈dominion〉と呼ぶ。 領地は、高次の圏、複圏、多圏のいずれかである。 領地は有限個である。 それぞれの領地は小さいn-圏, n-複圏, n-多圏である。 領地の次元は有限で、最高次元nが領…

指標（"インデキシング・ベース圏”の対象）と命題（{インデキシング垂直圏 | ファイブレーションのファイバーである圏}の対象）のペアを仕様と呼ぶ。仕様はグロタンディーク／エルブラン圏＝ハイパーベース圏の対象であると同時に、ハイパーインスティチュー…

重要なのはグロタンディーク／エルブラン圏である。 MLの概念 グロタンディーク／エルブラン圏 別な言い方 シグニチャー 仕様 セオリー ストラクチャ 絶対セオリー インスタンス ファンクタ 相対セオリー トランスフォーマー シグニチャに属するストラクチャ…

素材： 名前の集合 Name アンビエントドクトリン アンビエント圏C： アンビエントドクトリンから1つ選ぶ 論理ドクトリンL 以上から、指標圏と指標射が作れて、指標圏を定義できる。この指標圏をベース圏として、論理ドクトリンLに値をとるインデックス付き圏…

用語法、表記法 オペレーター | オペレータ | 演算子 | 作用素 | コンビネータ | コンビネーター コンストラクタ | コンストラクター | 構成子 | 構築子 | 生成子 例 トレースオペレーター 不動点オペレーター CADGの微分オペレーター／微分コンビネータ デ…

「型」と「型つけ」の概念が曖昧。型の代わりにプロファイルを導入して、型つけ〈タイピング〉の代わりにプロファイリングを使う。型は対象のことだとして、型付けは、基礎射のプロファイリングの意味に限定して使う。つまり、f:->A in C の形のプロファイリ…

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。 公理 公理証明 ax_A : * -> A * ----[ax A] AAx⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、 a : X -> A X ---[a] Aつまり、Ax⊆Mor(C)。Axはどん…

A1, ..., Anを仮定（assume）してBを結論（conclude, entail, result, produce, show）する証明があるとき、その証明内で使っている暗黙の知識がある。これを証明の文脈とか環境と呼ぶ。で、文脈とは正確には何か？ が大問題。それと、トンネル論法（コンパ…