定義的等号と命題的等号の区別が問題になるが、もっと問題なのは、宣言的所属関係と命題的所属関係だろう。宣言的＝合意形成的、命題的＝問題提示的所属的所属関係も $`\in`$ で書かれる。$`:`$ も使うが、宣言的所属関係を $`:`$ で書くと、圏論のコロンの…

https://arxiv.org/pdf/1311.7642 の2.1 のクライスリ構造〈クライスリ拡張構造〉$`\newcommand{\T}[1]{\text{#1}} \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\twoto}{\Rightarro…

関係しているでしょ。 普遍的なグロタンディーク構成？ スライス圏の大域的な定義： スラッシュ記号の解釈

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\ckw}[1]{ {\bf \text{ #1 }} } `$ $`\text{普通}`$ $`\text{丁寧}`$ $`\Gamma \vdash `$ $`\Vdash_\mrm{wf} \Gamma \ckw{ctx}`$ $`\Gamma \vdash A`$ $`\Gamma \vdash_\mrm{wf} A \ckw{type}`$ $`\Gamma …

次の4つは同じこと。 x は、n重〈n-fold〉の繰り返しインデックス付き圏の対象である。 x は、n重〈n-fold〉の繰り返しファイブレーション・スライス圏の対象である。 x は、長さnのファイブレーション・パス〈グロタンディーク・テレスコープ〉である。 x …

拡張包括構造を持った圏が、カートメル構造／カートメル性〈Cartmell property〉を持つとは、$`\newcommand{\cat}[1]{\mathcal{#1}}`$ |$`\cat{C}`$| 上の長さ関数 $`\ell :|\cat{C}| \to {\bf N}`$ がある。 長さが 0 の対象は終対象に限る。終対象はひとつ…

ユーザー定義の定理〈名前付き証明〉の名前には、赤で下線。 システム組み込みの定理〈証明規則〉の名前には、青で下線。 キーワード generic は総称〈多相〉の定理 ユーザー定義の定理〈名前付き証明〉の呼び出しは、ピンクで下線。 システム組み込みの定理…

目的の（でき上がりの）証明図：証明図のプロファイルは、$`\quad A \Rightarrow (B \Rightarrow C) \to (A\land B)\Rightarrow C`$あるいは、$`\mathrm{Proof}(A \Rightarrow (B \Rightarrow C), (A\land B)\Rightarrow C)`$ の要素。もっと正確に言えば、…