依存型に一般化したカリー同型：$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{ \text{ in } } `$$`\quad \cat{C} \in |{\bf Cat}|\\ \quad A:I \to |\cat{C}|_0 \In {\bf Set}\\ \quad \prod_{i\in I} \ca…

次のような対応があると思う。 テレスコープ ←→ フォレスト テレスコープのシグマ構成圏の対象 ←→ フォレストのパス テレスコープのシグマ構成圏の対象集合 ←→ フォレストのパス集合 テレスコープに関して、レベルk（k - 0, 1, ...）のベース圏を考える。レ…

カリー同型とフビニ定理は切っても切れない。フビニ定理は、カリー同型で互いに移る高階関数と多変数関数の積分が一致することを主張している。同様に、依存カリー同型と依存フビニ定理は切っても切れない。依存フビニ定理は、カリー同型で互いに移る高階依…

カリー同型は、複関数〈multifunction | 多重関数 | 多変数関数〉と高階関数〈higher-order function〉との1：1対応を与える。同様に、依存カリー同型は、依存複関数と依存高階関数のあいだの対応を与える。さらに、関数を関手に一般化するると、依存複関手…

テレスコープとグロタンディーク構成とグロタンディーク／フビニの定理の関係：indexed thing = indexed family of things を単にファミリーと呼ぶ。インデックス付き圏もファミリーになる。テレスコープはファミリーに関して定義できる。テレスコープの第1…

Wikipediaに ニコラース・ホーヴァート・ド・ブラウン という項目があるので、「ド・ブラウン」にする。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1} } %`$Automathの論文 "Telescopic mappings in typed lambda calculus" by N.…

型カインドの定義は次にある。 https://m-hiyama.hatenablog.com/entry/2020/10/21/175259 これだと、単に「型の集合」だが、排他的型カインドという概念を入れないとまずいな。排他的型カインドと型ファミリー（型でインデックスされた型の族）をしっかり区…

グロタンディーク／フビニの定理は、ファイブレーションに関する公式ではなくて、平坦化圏に関する同型性を言っているだけ。射影は関係しない。一般的な形は：簡略に書けば：加群層の例では：より普通の記法にして、特に対象に注目すると：次の書き方の変換…

気休め語〈consolation word〉で印象が変わる、という大問題。逆に、気休め語を分析する。 キーワード無し構文 - (新) 檜山正幸のキマイラ飼育記 メモ編 列挙。随時追加予定。 オフィシャル構文 気休め語 1-σ signature, class, typeclass, specification, i…

気付いた！考えた時系列にだいたい沿って書く； ゲージ群G、ファイバーFの自明バンドルの圏を考える。バンドル射は底写像を考えるが底写像は可逆とする。この状況で、バンドル射は可逆となるので、自明バンドルの圏は亜群となる。これを (G, F)-自明バンドル…

フビニの定理関係で例が欲しい。最近興味持ってるファイバーバンドル関係から。PrinBdl[X, G]を主バンドルの圏とする。 PrinBdlX[G] := PrinBdl[X, G] PrinBdlG[X] := PrinBdl[X, G] PrinBdlGX := PrinBdl[X, G] これで、PrinBdlGは、多様体の圏をインデクシ…