このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

カートメル林の圏

木〈ツリー〉や林〈フォレスト〉は重要なデータ構造です。以下の過去記事で説明したことがあります。 木と林(有向グラフ) 木と林(有向グラフ) その2 レベル付き林の圏 (最後の追記参照) カートメル〈John Cartmell〉による木・林の定義が使いやすいと…

論理計算のための宇宙と型 補遺

「論理計算のための宇宙と型、二種類の述語」において、二元の宇宙 $`{\bf Prop}`$ を次のように定義しました。$`\quad {\bf Prop} := |{\bf Bool}|`$$`{\bf Bool}`$ は2つの対象 $`{\bf 0}, {\bf 1}`$ だけを持つ集合圏の充満部分圏です。しかし実際の証明…

論理計算のための宇宙と型、二種類の述語

型理論と圏論の言葉は次のように対応します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mfk}[1]{ \mathfrak{#1} } \newcommand{\In}{ \text{ in } }`$ 型理論 圏論 型 対象 型宇宙 圏の対象達のクラス インスタンス 射 Sets As Types(集合が型だ…

シグマ型とパイ型の短縮記法(便利)

一部の証明支援系/プログラミング言語において、シグマ型を直積型と同じ '$`\times`$' で、パイ型を指数型と同じ '$`\to`$' で書くという記法が採用されています。これは短く書けて便利なのですが、当然ながら混乱を招くので、少し変更した形で紹介します。…

最近の型理論のハマリ所

色々とハマル。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\In}{\text{ in }} \newcommand{\op}{ \mathrm{op} } % used \newcommand{\hyp}{\text{-} } % used \newcommand{\ILT}{ \triangleleft } % immediately…

前層の表現可能性 再論:指標による記述

以前、圏論の普遍性という概念は難しい、という話を書いたことがあります。 圏論の普遍性が難しい理由 普遍性は“前層の表現可能性”により語られるので、普遍性の難しさは“前層の表現可能性”の難しさです。「表現可能である」ことは前層の性質ですが、「当該…

GAT〈ガット〉

日記風にダラッと書きます。ヴォエヴォドスキー〈Vladimir Voevodsky〉のC-システム(「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照)は、名前を変更しただけでカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉と…

型理論的形式体系の構文代数系はファイバー付き依存多圏

型理論的形式体系〈type-theoretic formal system〉とは、抽象的演繹系(「演繹系とオペラッド」参照)の一種で、基本的な構文構成素としてコンテキストと何種類かの判断を持ちます。型理論的形式体系があると、コンテキストを対象として、コンテキストのあ…

複前層の圏とファミリー付き圏

「ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層」で述べたように、ヴォエヴォドスキーとパルムグレンは、同じ時期に同じ概念を独立に考えていたようです。その概念を、パルムグレンによる呼び名 "multivariable presheaf over $`\mathcal{C}`$" を縮め…

型理論に出てくる第一射影と第二射影

ファミリー付き圏〈category with families | CwF〉やC-システム〈C-system〉(コンテキスト圏〈contextual category〉と同じ)など、型理論の構文的側面を圏論的に定式化した圏(型理論的圏)では、「射影〈projection〉」と呼ばれる射が登場します。射影が…

ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層

最近、カートメル/ヴォエヴォドスキーのC-システム(「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照)に興味を持っています。で、次の論文を眺めてみました。 [Voe14-15] Title: A C-system defined by a universe category Author: Vl…

パチモンの圏 = システム

「C-システム、分裂ディスプレイクラス、カートメルツリー」より: ヴォエヴォドスキー〈Vladimir Voevodsky〉は、型理論の理論〈theory of type theories〉の基礎としてカートメル〈John Cartmell〉のコンテキスト圏〈contextual category〉を採用しました…

C-システム、分裂ディスプレイクラス、カートメルツリー構造

インスティチューション理論の骨組みに、型理論やモナドを使って肉付けしようという目論見(「構文付き変換手インスティチューション 1/n」における“半具象インスティチューション”)は、型理論的圏の反対圏が指標の圏として使えることが分かってちょっと進…

型理論とインスティチューション理論が繋がるぞ!

ビンゴ! 「インスティチューションの“指標の圏”の具体化として、型理論的圏の反対圏をとればいいだろう」と見当をつけていたのですが、アタリだったようです。型理論的圏は、拡張包括構造を持ちます。拡張包括構造を持つ圏上の、プルバック四角形(コスパン…

ファイブレーションの亀裂と分裂

昨日の記事「拡張包括構造のもうひとつの定式化」で次のように書きました。 $`\mathrm{Disp}`$ が関手になるとき、選択した $`(d, f) \mapsto f^\# d`$ 達を、ディスプレイクラス $`\mathscr{D}`$ の分裂子〈splitting〉と呼びます。分裂子を持つディスプレ…