分野（例： IT, math, tech, program-semantics） 理論 トピック／サブジェクト 製品名、ソフトウェア名（プログラミング言語も含む） 製品群、ソフトウェア群（例： database） intro（入門情報）, tips（コツ）, text（教科書）など レーティング／評価 人…

象手露 コレクション／サブコレクションは仮想フォルダ。リンクを構造化しているだけで、実体には影響しない。 タグは階層化できない。もし、Obsidianのような階層化タグをサポートすると、タグ階層とコレクション階層の区別が困難だろう。つうか、同じにな…

象手露 本体のダウンロード＆インストール the Zotero Connector for Chrome （プラグイン／拡張機能）を Arc にインストール LibreOfficeのプラグインはスキップ（使うことはない）。 Zoteroアカウント作成はスキップ（後でも出来るだろう）。

帰納的にデータ型を定義するとき：$`\require{color} % Using \newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name \newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression \newcommand{\T}[1]{ \text{#1} } \newcommand{\B}[1]{ \m…

バンドル射 ＝ アロー圏の射 バンドル射がアロー圏のCodに関するデカルト射＝バンドル射がプルバック四角形 バンドル射がプルバック四角形 ＝ エタール射 ＝ 局所同型

一般代数学 ： ローヴェアセオリー ＝ 型理論 ： C-システム その状況証拠は： [Voe15] Title: Lawvere theories and C-systems Author: Vladimir Voevodsky Submitted: 26 Dec 2015 Pages: 15p URL: https://arxiv.org/abs/1512.08104 長さ双射〈l-bijectiv…

以前、プライベートな xxx/yyy/zzz を設定した記録が残っていたので、それを載せる。過去の記録で現状にあっているとは限らない。一部は現状にあわせて編集したが、ごく一部。旧「はてなダイアリー」の設定が混じっている。今気付いたが、はてな記法の星ひと…

以前、UIからの切り替えができたと思うが、今は、UIのテーマにより、あるいは全面的に“UIからの切り替え”は出来ない仕様らしい。次のURLにアクセスするとサブアカウント切り替えができる。 https://accounts.hatena.ne.jp/settings/accounts そんなに頻繁に…

3rdブログを作成したが、いくつか問題がある。 他の設定とあわせてない。最初から設定せねば。 Markdownにしたが、現状（何も設定してないから）数式は出ないし、ましてや、xyjaxが使えない。 一番下にはてな自身の広告が出る。 編集ボタンが出ない → https:…

全体的な参照URLなどは「Overleaf + pandoc」。 4年前 テンプレートとinput XeLaTeX はやめた pandoc による変換 結論 追記： LuaLaTeX 4年前 4年前にOverleafで実験したときに、次がコンパイルは通った。 \documentclass[a4paper]{bxjsarticle} \usepackage…

先にこれ読んでおいたほうがいい。 今風なLaTeXに関するメモ 「今風」とは言っても5年以上前ではあるが、~/latexmkrc や bxjsクラスについて書いている。オーバーリーフのいいところは： https://qiita.com/FluffyHernia/items/0cc751e56858c9c55b58 （2021…

カリー／ハワード／ランベック対応を徹底するには： calc/compute（動作・行為）とprove（動作・行為）proof（すること）を同義とする。 function returns a velue of type T と theorem returns a witness of prop T を同義とする。 prop は広義の型の一種…

名前空間、知識記述〈knowledge description〉の名前空間と用語レキシコンの名前空間は別。 名前空間名と名前空間階層ツリー 名前の分類子、分類子による名前空間のパーティショニング。異なるパーティションの同一ローカル名は異なる。 「名前空間名」は名…

テンプレートは、穴〈スロット〉を埋めることにより具体物を作り出すことが目的。 穴〈スロット〉がないテンプレートをリテラル・テンプレート、あるいは単にリテラルと呼ぶ。それだけで具体物。 穴が実際にあるテンプレートは非リテラル・テンプレート。「…

in◯◯, un◯◯, non-◯◯, dis◯◯, ◯◯less◯◯, ◯◯ without ◯◯、非◯◯、不◯◯、無◯◯、◯◯なし◯◯ など。用法： 制限的用法 拡張的用法 排他的用法 冗長な用法 非可換／可換： 拡張的用法： デフォルトで環が可換のときの、非可換環。スーパー指標を追加して、既存指標「…

同義語句による置き換え〈replacement〉 例： pointing function ＝ example 変形ルールによる変形 例： example of type Nat named k → example k returns type Nat 省略可能な情報の省略と補完 例： type T → type T in U 注記情報の追加と削除（これも省…

$`\require{color} % Using \newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name \newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression `$$`\text{volatile namespace}\\ \text{we define function }\NN{f1}\\ \quad \text{by pos…

define applying end が定義の構文だが、キーワード applying の直後に記述フォーマット名を付けてよい。つうか、付けるのが推奨。 applying record-schema-template-diagram ◯◯ end applying record-schema-template-text ◯◯ end applying standaard-arithm…

次は同義 $`\text{we define example of type }T \text{ named }e`$ $`\text{we define pointing function } e \text{ returns type }T`$ example〈事例 | 具体例〉は pointing function に展開されるが、of は語順を変えてしまう。of は戻り値型を先に記述…

トピックワードとは、記述本体内に散在して出現するワードで、トピックを表すキーワード。以下、実際に予定しているトピックワード。 基本データ型 基本データ値 複合データ型 複合データ値 自然数による非負有理数の構成 自由な帰納的構成 自由な相互再帰的…

使用法変種とは usage variant 、使用法により記号が変化する。本質的な意味は変わらない。 $`\mapsto`$ ： 割り当て単位〈assignment unit〉を記述する。 $`:\in`$ ： 割り当てが、所属宣言であることを示す。 $`:=`$ ： 割り当てが、代入単位であることを…

中括弧の使用法が、列挙記法〈外延的記法〉と内包的記法で違いすぎる。暫定的だが、記法を決める。 集合の列挙記法： $`\{a, b, c\}`$ 集合の名前隠蔽内包的記法： $`\{\!| x :\in X \mid \cdots |\!\}`$ 縦棒を追加、厳密にZFCの意味で使う。ただし、$`\{\!…

リスト／タプル囲み括弧（具体データ構成子記号／型項構成子記号の一部と考える） 引数囲み括弧（評価演算の二項演算子記号の一部と考える） 演算の優先度括弧（パーズツリーに影響する） まとまり括弧（パーズツリーに影響しない） 規則と注意 引数囲み括弧…

$`\newcommand{\Imp}{\mathop{ =\!\!\triangleright }} \newcommand{KER}{ \mathrel{\stackrel{\rightharpoonup}{\sim}} } % Kleene Equarity Right \newcommand{KEL}{ \mathrel{\stackrel{\leftharpoonup}{\sim}} } % Kleene Equarity Left \newcommand{\le…

主語 we 動詞 declare, define, approve〈アプルーブ〉 副動詞 request, respond 名前の修飾語 type, function typeへの副修飾語 logical, type-param, prop-param functionへの副修飾語 section, bundle, type-velued, prop-valued, partial 終止語 end そ…

主動詞： declare〈宣言する〉, define〈定義する〉, approve〈承認する〉 副動詞： request〈要求する〉, respond〈応答する〉 主語は We, One of us, I だが、省略可能。組み合わせは： declare 名前 仕様 ： 名前を宣言する。存在に関しては中立。 declar…

記述の事例： 圏論/小さいとは限らない【形】 -(同義)→ 圏論/大きい 圏論/小さくない【形】 -(同義)→ 圏論/真に大きい 圏論/大きい集合 -(同義)→ 集合論/クラス 圏論/小さい集合 -(同義)→ 集合論/集合 圏論/小さくない集合 -(同義)→ 集合論/真のクラス 一般/…