連言 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}{\;::\;}% …