何を今更な話をします。この記事は、他の記事から参照することを主な目的にしています。モノに対してその種別と相対役割りを区別しましょう； 区別しないとダメです。例えば、人というモノ（「モノ」は広義、人も一種のモノと考える）について、未成年と成人…

「最近の型理論： 宇宙と世界、そして銀河」(2023-04-21) 以来、型理論で使う宇宙、つまり型宇宙に興味を持っています。型宇宙は、型達をホストする場所（「ホストする」については「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」参照）です。型…

ひとつ前の記事「Propositions-As-Typesを曲解しないで理解するために」の最初の節や最後の節で、同義語・曖昧多義語を話題にしました。曖昧さは色々な形で現れます。なにごとかを正確に理解するには、曖昧さを処理していくことが必要です。まー、曖昧に書く…

「贅沢なグロタンディーク宇宙とPropositions-As-Types」に対して、老婆心的な補足をします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\In}{\text{ in }} `$内容： 「命題」を排除したい！ ベリティ型とその型…

次の2つの記事の続きです。 贅沢主義者のグロタンディーク宇宙 型・インスタンス・宇宙とタルスキ宇宙系列 Propositions-As-Typesというよく知られたキャッチフレーズを、グロタンディーク宇宙の観点からなるべく明確にします。$`\newcommand{\mrm}[1]{\math…

「贅沢主義者のグロタンディーク宇宙」でグロタンディーク宇宙の話をしました。贅沢主義か節約主義かは、公理系を設定するときの態度であって、どちらの態度で公理系を設定しても、得られる概念は同じです。ところで、単一のグロタンディーク宇宙ではなくて…

たいていの公理系はミニマリスト・アプローチで定義されていて、無駄な（他の公理達から導出可能な）公理は入れないで、必要最小限の公理達から構成されています。しかし、導出可能な命題を最初から公理系に入れておくのが絶対にダメなわけではないです。「…

ダラッっと語る。$`\newcommand{\In}{\text{ in }} \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } %\newcommand{\u}[1]{\underline{#1} } %\newcommand{\Imp}{\Rightarrow} %\newcommand{\If…

同一の概念にたくさんの呼び名があるのは、よくあることです。呼び名が違うことで同一性に気付かなかったり混乱したりします。表題にある概念の同一性について整理しておきます。$`\newcommand{\In}{\text{ in }} \newcommand{\mrm}[1]{\mathrm{#1} } \newco…

「スライス圏の大域的な定義： スラッシュ記号の解釈」で、スラッシュ記号 '$`/`$' で表現されるスライス構成について述べました。そこで次のように書きました。 二番目の $`f^*`$ は定義に条件が必要で複雑でもあるので、ここでは一番目だけを扱います。 過…

以下の過去記事達で指摘した問題の一部に対する対策をします。 型理論に出てくる第一射影と第二射影 最近の型理論のハマリ所 ファイバー積の場合の第一射影と第二射影で使う記法を新たに約束します。双対であるコファイバー和についても論じます。$`\newcomm…

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

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