検索やソートに利用できる項目ソート／グルーピング ブックマークの生成時刻 タイトル文字列のソート順、あまり意味ねー URLのあるレベル（ドメイン名など）でグルーピングする。 人気順（ユーザー数が多い順） 検索／制限 タグによる検索 コメント内にある…

http://b.hatena.ne.jp/help/entry/port#export に従う。 ユーザー画面から設定画面に 「データ管理」タブに移動します エクスポートより、Atomフォーマットを選んで、右クリックでダウンロード。 何も変更しないと、ダウンロードのファイル名はdump.htmとな…

当然にインスティチューション 当然に述語論理＝ハイパードクトリン 限量子随伴性 ＝ ΣΔΠ随伴性 否定があるなら、否定双対性。スター自律圏かな？ 継続との関連は？ 契約は仕様と関連するから、メイヤー先生のDbCとは関連する。 仕様モジュール、セオリー・…

スペクトラム〈spectrum〉の複数形がスペクトラ〈spectra〉。スペクトルはスペクトラと同義だろう。forvoでは、 https://ja.forvo.com/search/spectra/ 「ペッ！」を強調するスペクトラと聞こえる。スペクト「ル」とは聞こえないがaが消えるとspectrで「ル」…

name object 呼び名 圏論 変数名 型 型宣言 指標対象成分 関数名 項 関数 指標射成分 ラベル 命題 表明 論理対象 定理名 証明 定理 論理射 名前の宣言 name 宣言 名前のソート ソート式 変数名 var x:X 型 型項 関数名 function f:(x:X, y:Y)->Z プロファイ…

Sを指標圏、Lを論理ドクトリンとするハイパードクトリンH:S→Lがあるとする。Σ∈|S| に対してH[Σ]は指標Σ上の論理圏であり、その論理圏は論理ドクトリンLに所属する。ハイパードクトリンHをインデックス付き圏とみなして、そのグロタンディーク平坦化をTheo(H)…

計算解釈 論理解釈 項 証明 項ブロック 証明ブロック ユニット型 真 エンプティ型 偽 型 命題 型構成子 論理結合子 依存型構成子 限量子 定数 公理 関数 定理 関数の定義項 定理の証明 関数のヘッダ 定理のヘッダ 定数・関数名 公理・定理ラベル 関数コンビ…