連言 and.left : ?M_1 ∧ ?M_2 → ?M_1 （A∧B ⇒ A） and.right : ?M_1 ∧ ?M_2 → ?M_2 （A∧B ⇒ B) and.intro : ?M_1 → ?M_2 → ?M_1 ∧ ?M_2 （A B ⇒ A∧B） 含意 空白〈right-eval〉 : ((?M_1 → ?M_2) → ?M1) → ?M_2 (（A → B) A ⇒ B） assume 変数 : 型, 式 ≡ λ …

NDed は双デカルト圏モノイド構造その1 対象 射 モノイド積 単位対象 モノイド構造その2 対象 射 モノイド積 単位対象 PolyNDed は双デカルト圏モノイド構造その1 対象 射 モノイド積 単位対象 対象のリテラル： モノイド積： モノイド構造その2 対象 射 モ…

左含意導入

イイカゲンの原理： 用語・記法は適切とは限らない。整合性・一貫性を期待してはならない。 モノグサの原理： 用語・記法は省略やオーバーロードにより書く労力を節約している。読み手側に負担を押し付ける。 暗黙の原理： 暗黙の前提や約束ごとが存在する。…

平叙文〈declarative sentence〉 疑問文〈question sentence〉 命令文〈imperative sentence〉 ※ 肯定文と否定文は平叙文内の分類。

xy環境内で、マトリックスの直後に drop-frameコマンド（描画インストラクション）を付ける。

自由変数を番号にすると： 束縛変数も番号にしても構わない。

連言導入選言消去

連言導入パターン 選言消去パターン 選言消去パターン 2

[tex:\require{color}% \newcommand{\deform}[1\]{% {#1}\\% \xymatrix{ *[.\]{}\ar@2{~>} [d\] \\{} }% }% % \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1\]{ \langle\![{#1}\]\!\rangle }% \newcommand{\As}{\;::\;}% …

カリー／ハワード対応 カリー／ハワード／ランベック対応 デカルト閉圏 マルコフ圏

オブジェクトの種類 TeXオブジェクト： TeXコードで生成される、構文はTeXのブレイスブロック カーネルオブジェクト： カーネルまたは拡張で定義されるオブジェクト、構文はTeXコマンド 方向付きオブジェクト＝有向辺オブジェクト： \dir で記述される有向辺…

\xymatrix@1{ ... } でインライン向きの１行マトリックスを作れる。主に、\xymatrix@1{A \ar[r]^f & B} 。

マトリックス全体の列間寸法、行間寸法を調整する以外にアローの長さは調整できない。アローごと、行ごと、列ごとの調整は不可能。

マトリックスでエントリーを省略できるが、このときは不在エントリーとなる。不在エントリーはそこにオブジェクトがないとみなされる。{} で空エントリーを作れる。空エントリーは、内容が空なだけで存在する。不在エントリーへのアローは引けない。

modifier は「修飾子」と訳すみたいだが、Xy-pic だと別に decorator がある。decoratorはカタカタ「デコレータ」かな。とりあえず、modifier = 修正子 にしておく。修正子とデコレータ〈デコレーション〉の違いがハッキリしない。修正子は、オブジェクト修…

構文解析がXyJax側で行われるので、newcommandで定義されたマクロは効かない。TeXコードを入れたブロック内はTeX側に移譲して構文解析するからマクロが効く。複雑な組み合わせを繰り返し使うから、マクロが効かないのは辛い。

ライブラリ→ 拡張、フィーチャ XyPicインストラクション::= 位置 オペレーター 引数 オブジェクト → TeXオブジェクト、カーネルオブジェと 矩形、エクステントとサイズ（幅、高さ） 矩形データ、中心、エクステント、参照点 カーネルオブジェクト： 方向付き…

<script> MathJax = { loader: {load: ['[tex]/physics', '[tex]/bussproofs']}, tex: { inlineMath: [ ['$`', '`$'] ], packages: {'[+]': ['physics', 'bussproofs']} }, chtml: { matchFontHeight: false } }; </script>

\begin{xy} \xymatrix{A & B\\ C & D} \drop\frm{-} \drop\cir<8pt>{} \end{xy} フレーム： \frm{.}フレーム： \frm{=}フレーム： \frm{--}フレーム： \frm{-o}フレーム： \frm{o-}フレーム： \frm{==}フレーム： \frm{*}フレーム： \frm{o}

\ar[r]^(0.32){f}

対角線上に \ar@{}[dr]|\circlearrowleft