import FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations import FormalLab.Bridges.STLCCategoricalSemantics /-! # 全問題の解答：型理論の圏論的意味論 ## 第70章：デカルト閉圏——積・指数対象・カリー化 ### 問題1：評価射からカリー化の存在一意性を再構成する #### ヒント 指数対象B^Aと評価射 `ev:B^A×A→B` の普遍性を、任意の `f:X×A→B` について書きます。 #### 解答 指数対象の普遍性は、各fに一意な `Λf:X→B^A` が存在し、`(Λf×id_A)≫ev=f` を満たすことです。存在がカリー化、 方程式がβ則、一意性から任意の `g:X→B^A` に `Λ((g×id)≫ev)=g` というη則が従います。逆にcurry/uncurryの 自然な全単射があれば、X=B^Aで恒等射をuncurryしたものをevとして同じ普遍性を回収できます。 高階関数APIの正しさを、単なる型同型でなく評価との可換三角形として表せます。 ### 問題2：β則・η則・三角恒等式を対応させる #### ヒント 積関手 `(-)×A` と指数関手 `(-)^A` の随伴として単位・余単位を取り出します。 #### 解答 随伴 `(-)×A ⊣ (-)^A` の余単位は評価射、単位は `x↦(a↦(x,a))` に対応します。一方の三角恒等式は、カリー化してから 評価する操作が元の射へ戻るβ則です。もう一方は、関数を評価射へuncurryして再びcurryすると元へ戻るη則です。 従ってラムダ計算のβη等式は、随伴のhom全単射の逆法則または単位・余単位の三角恒等式として同じ内容を表します。 依存積やモノイダル閉圏でも、対応する随伴の三角恒等式からβη則を読み取ります。 ### 問題3：指数対象を表現可能性として構成する #### ヒント 固定したA,Bに対し、関手 `X↦Hom(X×A,B)` を表す対象を考えます。 #### 解答 対象Eが自然同型 `Hom(X,E)≅Hom(X×A,B)` を表せばEをB^Aとします。普遍元はX=Eで恒等射に対応する `ev:E×A→B`。任意のfの逆像がΛfで、全単射の逆法則が存在一意性を与えます。表現対象の一意性から指数対象は標準同型を 除いて一意です。積が存在するだけではこの関手が表現可能とは限らず、閉性は追加条件です。 内部homを探すときは、テンソルしたhom関手の表現可能性として候補と評価射を構成します。 ### 問題4：デカルト閉圏とモノイダル閉圏の差を射で検査する #### ヒント デカルト積には対角射と終対象への射が自然にありますが、一般テンソルにはありません。 #### 解答 どちらも `(-)⊗A` の右随伴 `[A,-]` を持ちます。デカルト閉圏では⊗が圏論的積なので、任意Xに自然な複製 `Δ_X:X→X⊗X` と破棄 `!_X:X→I` があります。一般のモノイダル閉圏では評価・カリー化はあってもΔと!は得られません。 従って変数を複製・未使用にする構造規則は閉性でなくデカルト性に由来します。 線形ラムダ計算と通常のラムダ計算の差を、内部homの有無でなく資源管理射の有無として説明します。 ## 第71章：単純型付きラムダ計算の圏論的意味論——判断を射へ移す ### 問題1：全ての構文的代入について意味論的置換補題を証明する #### ヒント 項tへの構造帰納を行い、変数・組・射影・ラムダ・適用をすべて扱います。 #### 解答 代入 `σ:Δ⇒Γ` の意味を文脈対象間の射 `⟦σ⟧:⟦Δ⟧→⟦Γ⟧` とすると、主張は `⟦t[σ]⟧=⟦σ⟧≫⟦t⟧`。変数では射影と代入タプルの定義、組と射影では積のβη則、適用では評価射の自然な計算、 ラムダでは指数随伴の自然性を使います。各構文子で構文的代入が意味射の合成へ移ることを示し、同時に恒等代入・合成代入も 恒等射・合成へ送られます。 依存型では通常の前合成を再添字付けへ置き換え、同じ置換補題をcoherence付きで証明します。 ### 問題2：β・η以外の等式をモデルで検査する #### ヒント 候補等式が全デカルト閉圏で成立するか、有限集合モデルなどで反例を探します。 #### 解答 βη等式と積の法則はすべてのデカルト閉圏モデルで成立します。例えば異なる自由変数x,yを無条件に同一視する等式は、 `Type` でBoolを解釈しx=true,y=falseとすれば失敗します。自然数定数など追加構造の等式は、その構造の公理を持つモデルだけで 検査します。あるモデルで意味が異なれば構文理論から導出不能ですが、あるモデルで一致するだけでは導出可能性は証明できません。 健全性で反例モデルを導出不能性へ使い、完全性がある場合だけ全モデル妥当性から導出を回収します。 ### 問題3：構文圏の対象・射・合成を設計する #### ヒント 対象を型、射A→Bを一変数文脈 `x:A⊢t:B` のβη同値類とします。 #### 解答 恒等射は変数項x、合成は項代入です。代入の単位・結合性が同値類上の圏法則を与えます。積対象は積型、終対象はUnit、 指数対象は関数型で、構文的組・射影・ラムダ・適用が普遍射になります。βη等式により普遍性の逆法則が成立します。 この構文圏から任意のモデルへの構造保存関手は型・定数の解釈により一意で、構文圏の初期性を表します。 構文圏を自由な意味論的構造として作ると、再帰的な解釈定義と健全性を普遍性へまとめられます。 ### 問題4：構造規則が意味射のどこに現れるかを追跡する #### ヒント 弱化は終対象への射、縮約は対角射、交換は積の対称性として文脈射を作ります。 #### 解答 変数を使わない弱化は `Γ×A→Γ` という射影、またはAから終対象への一意射で成分を捨てる操作です。同じ変数を二回使う縮約は `Γ→Γ×Γ` の対角射。変数順の交換は積の対称同型です。結合的な文脈再括弧付けは積の結合同型に対応します。これらが デカルト構造から自然に得られるため、通常のSTLCでは構造規則を自由に使えます。 線形論理では対応射を一般には持たないモノイダル圏を選び、資源使用制約を意味論に反映します。 ## 第72章：スライス圏・添字圏・ファイブレーション——変化する文脈の上で対象を運ぶ ### 問題1：`Type` の引戻しの普遍性を同値としてまとめる #### ヒント `f:X→Z`,`g:Y→Z` の引戻しを `{(x,y)//f x=g y}` とし、そこへの関数を可換な関数対と対応させます。 #### 解答 Pを条件付き対型とすると、関数 `h:W→P` は射影との合成 `a:W→X`,`b:W→Y` と証明 `f∘a=g∘b` を与えます。 逆に可換な対から `w↦⟨a w,b w,証明 w⟩` を作ります。部分型・積・関数外延性で両構成は逆です。従って `Hom(W,P)≃Σ(a,b),f∘a=g∘b` がWについて自然で、引戻しの普遍性を表します。 依存対を可換な射対の分類対象として読むと、型族の再添字付けを引戻しへ接続できます。 ### 問題2：スライス圏の射を手で合成する #### ヒント Γ上の対象 `p:X→Γ`,`q:Y→Γ` 間の射は `h:X→Y` と三角形 `h≫q=p` です。 #### 解答 さらに `k:Y→Z` が `k≫r=q` を満たすなら、合成h≫kは `(h≫k)≫r=h≫(k≫r)=h≫q=p` を満たしΓ上の射です。恒等射は `id_X≫p=p`。圏法則は基礎圏の法則を継承し、可換証明は 命題成分なので射の等しさは基礎射の等しさへ還元できます。 文脈Γ上の型を表示射として扱い、型間の写像を文脈を変えないスライス射として表します。 ### 問題3：二回の再添字付けを一回の再添字付けと比較する #### ヒント 型族P:Γ→Typeを `f:Δ→Γ`、`g:Θ→Δ` に沿って前合成します。 #### 解答 集合族では `g*(f*P)(θ)=f*P(gθ)=P(f(gθ))=((f∘g)*P)(θ)` なので定義的に一致します。表示射の引戻しとして構成すると、 二段引戻しと合成に沿う一段引戻しは一般に標準同型であり、選んだ引戻しによって定義的等号とは限りません。この同型は 恒等再添字付けと合成についてcoherenceを満たし、擬関手構造を作ります。 証明支援系の置換を厳密に結合的にするstrictificationと、同型を追跡する設計を比較します。 ### 問題4：Cartesian持ち上げの一意性を図式で証明する #### ヒント 同じ基底射fと終点Yを持つ二つのCartesian射を、互いの普遍性へ入力します。 #### 解答 `u:X→Y`,`u':X'→Y` がともにf上Cartesianなら、u'をuの普遍性へ入れて基底恒等射上の `h:X'→X` を得て `h≫u=u'`。 逆にk:X→X'を得ます。合成h≫kと恒等射はu'への合成が同じで同じ基底射上にあるため、Cartesian一意性から等しい。 逆合成も同様です。従って持ち上げの始点はファイバー内で一意な同型を除いて決まります。 再添字付け対象の異なる構成を、Cartesian普遍性から得る標準同型で交換できます。 ### 問題5：Grothendieck構成の射を依存対として読む #### ヒント 擬関手P:Cᵒᵖ→Catの全圏で、対象を `(c,x)`、射を基底射とファイバー射の組にします。 #### 解答 `(c,x)→(d,y)` の射は `f:c→d` と `φ:x→P(f)(y)` の依存対です。合成は基底でf≫g、ファイバーではφの後に P(f)で写したψを合成し、擬関手の合成比較同型で型を整えます。射影は `(f,φ)` をfへ送り、Cartesian射はファイバー成分が 同型、特に選択した恒等であるものとして得られます。依存対が「基底の移動と移動後の証拠」を一緒に保持します。 添字付きデータの総圏を作り、インデックス変更とデータ変換を一つの射として扱えます。 ## 第73章：局所デカルト閉圏——依存積を再添字付けの右随伴として捉える ### 問題1：二つの型族随伴の自然性を証明する #### ヒント `Σ_f⊣f*⊣Π_f` のhom対応を、型族の関数として展開します。 #### 解答 `f:Δ→Γ`、A:Δ→Type、B:Γ→Typeについて `((γ,a):Σ_{δ:fδ=γ}Aδ)→Bγ` は、各δ,aへB(fδ)を返す関数、すなわち `A→f*B` と対応します。右側は `f*B→A` 型の族を、各γ,bから全δと等式fδ=γに対しAδを返す関数 `B→Π_f A` へカリー化します。前後の族写像との 合成を点ごとに計算すれば両対応の自然性が従います。 量化子の置換則を、Σ・Πが再添字付けの随伴であることから体系的に導けます。 ### 問題2：空ファイバーと多元ファイバーで依存積を計算する #### ヒント `(Π_f A)(γ)=Π_{δ:fδ=γ}Aδ` の添字型の要素数を場合分けします。 #### 解答 γ上のfのファイバーが空なら、空族への依存関数は一つだけなので `(Π_f A)(γ)` はUnitに同型です。一要素なら対応する Aδ、多要素なら各δのAδの積になります。対してΣ_fは空ファイバーでEmpty、多要素で直和です。零項積が終対象、零項和が 始対象になる一般則がファイバーごとに現れます。 データベースのgroup-byで、キーごとの行集合上の全称制約・集約を依存積として読めます。 ### 問題3：通常のカリー化を依存カリー化から回収する #### ヒント 射影 `π:Γ×A→Γ` に沿う再添字付けと右随伴Π_πを使い、定数族Bを選びます。 #### 解答 Γ上の定数的なB族をΓ×Aへ再添字付けすると各(γ,a)でBです。Π_πを適用すると各γで `A→B`、すなわち指数対象B^Aを 得ます。随伴hom同型 `Hom_{Γ×A}(π*X,B)≅Hom_Γ(X,Π_πB)` は、要素表示で `(γ,x,a)↦b` と `(γ,x)↦(a↦b)` の通常のカリー化です。従って局所的な依存積は指数対象を含みます。 依存型理論のΠ型が非依存関数型を定数族の場合として含むことを圏論的にも示せます。 ### 問題4：合成に沿う依存積の比較同型を追跡する #### ヒント `f:Δ→Γ`,`g:Θ→Δ` に対し、右随伴の合成が合成再添字付けの右随伴になることを使います。 #### 解答 再添字付けは `(f∘g)*≅g*∘f*`。右随伴は順を反転して `Π_{f∘g}≅Π_f∘Π_g` になります。両者が同じ関手の右随伴で あるため、随伴の一意性から標準自然同型が得られます。型族では、合成写像のファイバー上の依存関数と、まずgのファイバー、 次にfのファイバーでカリー化した関数が対応します。 多重Σ・ΠのFubini則や量化子の入れ子変更を、随伴の一意性で導きます。 ### 問題5：局所デカルト閉性の二つの定義を結ぶ #### ヒント 全スライスがデカルト閉であることと、各fの再添字付けが右随伴Π_fを持つことを往復します。 #### 解答 全スライスがデカルト閉なら、f:Δ→Γに対する再添字付けはスライスの積でfを引き戻す操作と見なせ、その指数構造から右随伴 Π_fを構成できます。逆にすべてのf*が右随伴を持てば、スライスC/ΓでA→Γとの積はAへの再添字付けを含む合成で表され、 Πを使って指数対象を構成できます。有限極限がスライスと引戻しを支える共通前提です。 局所デカルト閉圏を依存積型の意味論と見る際、採用する同値な定義と必要な有限極限を明記します。 ## 第74章：依存型理論の圏論的意味論——文脈・型・項・代入を再構成する ### 問題1：`Type` モデルをcategory with familiesの法則として整理する #### ヒント 文脈を型Γ、型を族A:Γ→Type、項を切断、代入を関数として各操作を列挙します。 #### 解答 文脈圏はTypeと関数です。Γ上の型はA:Γ→Type、項は `a:Πγ,Aγ`。代入 `σ:Δ→Γ` に沿う再添字付けは `A[σ](δ)=A(σδ)`、項は `a[σ](δ)=a(σδ)`。文脈拡張は `Γ.A=Σγ,Aγ`、射影pは第一射影、標準項qは第二射影です。 組 `⟨σ,a⟩:Δ→Γ.A` は `(σδ,aδ)`。恒等・合成置換、p/qのβ則、組のη則はいずれも関数計算です。 抽象モデルでは同じインターフェースを保ち、定義的等号が同型になる箇所だけcoherenceとして分離します。 ### 問題2：項と表示射の切断の同値を証明する #### ヒント 項aから `γ↦(γ,aγ)` を作り、切断sから第二射影を取ります。 #### 解答 族Aの表示射は `p:Σγ,Aγ→Γ`。項aは射 `s_a:Γ→Σγ,Aγ`, `s_a γ=(γ,aγ)` を与え、`s_a≫p=id` なので切断です。 逆に切断sについて等式p(sγ)=γに沿って第二成分をAγへ輸送して項を得ます。Typeの標準Σ表示ではsの第一成分が定義的にγなら 単に `(sγ).2`。二構成の往復はΣ外延性と切断等式から恒等になります。 依存項を文脈拡張の切断として読むと、項代入を引戻しと切断合成へ翻訳できます。 ### 問題3：依存積のβη則を随伴の三角恒等式へ翻訳する #### ヒント 表示射p:Γ.A→Γに沿う再添字付け `p*` と右随伴Π_pを使います。 #### 解答 依存ラムダ抽象はhom同型 `Hom_{Γ.A}(p*X,B)≅Hom_Γ(X,Π_pB)` の転置、適用は逆転置です。抽象後に適用すると元の射へ 戻るβ則、関数を適用形へして再抽象すると元へ戻るη則は、hom同型の二逆法則です。単位・余単位表示では随伴の二つの 三角恒等式になります。置換に対する安定性はこのhom同型の自然性に対応します。 Σ型・同一性型についても、導入除去規則を普遍性と計算則へ分解して意味づけます。 ### 問題4：置換のcoherence問題を具体例で示す #### ヒント 二段引戻し `(fg)*A` と `g*(f*A)` が選択した引戻しでは等しくなく同型だけになる例を考えます。 #### 解答 抽象圏で各引戻しを個別に選ぶと、合成射に沿って直接選んだ対象と二回引き戻して得た対象は普遍性により標準同型ですが、 同じ対象として定義されるとは限りません。すると構文の厳密な式 `A[f][g]=A[f∘g]` はモデルで同型としてしか成立せず、 三重置換では比較同型同士の五角形的coherenceも必要です。split fibrationや局所宇宙構成で選択を厳密化できます。 定義等式を意味づける際は「同型を除いて」だけでは不十分で、厳密化またはcoherence定理を用意します。 ### 問題5：外延的同一性型と内包的同一性型を分離する #### ヒント 反射規則・J消去に加え、等式反映と証明無関連性を持つか比較します。 #### 解答 内包的同一性型は項 `p:Id_A(a,b)` をデータとして保持し、Jによりreflの場合へ帰納しますが、pの存在からaとbが定義的に 同じとはしません。外延的体系では等式反映によりpから判断的等式a≡bを得るため、型検査の変換可能性へ証明探索が入り得ます。 圏論モデルでは対角射の因子化やpath objectが内包的構造を、対角部分対象に近い厳格な解釈が外延的構造を表します。 モデルの同一性型を述べるとき、反射・J・計算則・η・等式反映のどこまでを検証したか明記します。 ### 問題6：構文モデルの初期性を正確に述べる #### ヒント 対象となるモデルの圏、モデル準同型が厳密に保存する構造、同型まで保存する構造を固定します。 #### 解答 理論Tの構文モデルSyn(T)の初期性は、指定された各TモデルMへのモデル準同型が一意に存在するという主張です。この射は 基礎型・定数・型形成・項形成・置換・定義等式を保ちます。一意性が厳密か自然同型までかはモデル準同型の2圏的定義に依存します。 宇宙、Π、Σ、同一性型のどの構造を含めるかも署名に明記します。「構文が自由」というだけでは定理の型が不足します。 初期性から再帰的解釈と健全性を得る際、採用したモデル圏の射が要求する保存強度を追跡します。 -/ namespace FormalLab.Appendix.Solutions.Chapter071Exercise002 open FormalLab.TypeTheory.SimplyTypedLambdaCalculus open FormalLab.TypeTheory.StructuralRules open FormalLab.Bridges.STLCCategoricalSemantics def composeTerm (A B C : SimpleType) : Tm [] ((B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C) := .lam (.lam (.lam (.app (.var (.succ (.succ .zero))) (.app (.var (.succ .zero)) (.var .zero))))) def swapTerm (A B C : SimpleType) : Tm [] ((A ⇒ B ⇒ C) ⇒ B ⇒ A ⇒ C) := .lam (.lam (.lam (.app (.app (.var (.succ (.succ .zero))) (.var .zero)) (.var (.succ .zero))))) example : denoteTm (Base := Bool) (constant .atom .atom) PUnit.unit true false = true := rfl example : denoteTm (Base := Bool) (swapTerm .atom .atom .atom) PUnit.unit (fun left right ↦ left && !right) false true = true := rfl /-- Boolモデルは異なる二変数を同一視する追加等式を反証する。 -/ example : (fun environment : Bool × Bool ↦ environment.1) ≠ (fun environment : Bool × Bool ↦ environment.2) := by intro equality have := congrFun equality (true, false) simp at this end FormalLab.Appendix.Solutions.Chapter071Exercise002 namespace FormalLab.Appendix.Solutions.Chapter072Exercise002 open _root_.CategoryTheory open FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations universe u v variable {C : Type u} [_root_.CategoryTheory.Category.{v} C] variable {I X Y Z : C} {p : X ⟶ I} {q : Y ⟶ I} {r : Z ⟶ I} def composeSliceMorphism (h : X ⟶ Y) (hTriangle : h ≫ q = p) (k : Y ⟶ Z) (kTriangle : k ≫ r = q) : Over.mk p ⟶ Over.mk r := sliceMorphism (h ≫ k) (by simp only [Category.assoc, kTriangle, hTriangle]) theorem composeSliceMorphism_left (h : X ⟶ Y) (hTriangle : h ≫ q = p) (k : Y ⟶ Z) (kTriangle : k ≫ r = q) : (composeSliceMorphism h hTriangle k kTriangle).left = h ≫ k := rfl theorem composeSliceMorphism_triangle (h : X ⟶ Y) (hTriangle : h ≫ q = p) (k : Y ⟶ Z) (kTriangle : k ≫ r = q) : (h ≫ k) ≫ r = p := by simp only [Category.assoc, kTriangle, hTriangle] /-- 終域を保存しない関数は、同じスライス圏の射にはならない。 -/ example : (fun n : Nat ↦ n % 2) ∘ (fun n : Nat ↦ n + 1) ≠ (fun n : Nat ↦ n % 2) := by intro triangle have := congrFun triangle 0 simp at this end FormalLab.Appendix.Solutions.Chapter072Exercise002