第8部 型・計算・圏を結ぶ

問題1評価射からカリー化の存在一意性を再構成する

Problem

問題

型 E と射 ev:A×E→B を仮定し、任意の f:A×X→B に対して λf:X→E が存在し、 ev∘(id_A×λf)=f を満たすという条件を書いてください。同じ等式を満たす射の一意性を加え、hom同値の順写像・逆写像・二逆法則へ変換します。E=A→B の場合を typeCurry と typeUncurry で検証できれば完了です。

ヒント

指数対象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β則・η則・三角恒等式を対応させる

Problem

問題

typeUncurry_typeCurry と typeCurry_typeUncurry を項ごとのβ簡約・関数η展開へ戻してください。一般圏では評価射を随伴の余単位、coevaluationを単位として二つの三角恒等式を書きます。どちらか一方だけではhom対応が全単射にならないことを、単射または全射が失敗する関数の例で示せれば完了です。

ヒント

積関手 (-)×A と指数関手 (-)^A の随伴として単位・余単位を取り出します。

解答

随伴 (-)×A ⊣ (-)^A の余単位は評価射、単位は x↦(a↦(x,a)) に対応します。一方の三角恒等式は、カリー化してから評価する操作が元の射へ戻るβ則です。もう一方は、関数を評価射へuncurryして再びcurryすると元へ戻るη則です。従ってラムダ計算のβη等式は、随伴のhom全単射の逆法則または単位・余単位の三角恒等式として同じ内容を表します。

依存積やモノイダル閉圏でも、対応する随伴の三角恒等式からβη則を読み取ります。

問題3指数対象を表現可能性として構成する

Problem

問題

固定した A,B について X↦Hom(A×X,B) の射作用を前合成で定義してください。評価射から Hom(X,B^A)→Hom(A×X,B) を作り、カリー化を逆写像にします。X'→X に関する自然性を合成律から証明し、対象ごとの全単射だけでは表現可能性にならない理由を、自然でない全単射族の可能性から説明してください。

ヒント

固定した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デカルト閉圏とモノイダル閉圏の差を射で検査する

Problem

問題

デカルト積の射影 A×B→A,B、対角射 A→A×A、終対象への射を列挙し、変数の破棄と複製へ対応させてください。一般のモノイダル積について同じ射を型だけから構成しようとし、どこで追加構造が必要になるかを特定します。閉性が与える評価・カリー化と、デカルト性が与える構造を別の欄に分類できれば完了です。

ヒント

デカルト積には対角射と終対象への射が自然にありますが、一般テンソルにはありません。

解答

どちらも (-)⊗A の右随伴 [A,-] を持ちます。デカルト閉圏では⊗が圏論的積なので、任意Xに自然な複製 Δ_X:X→X⊗X と破棄 !_X:X→I があります。一般のモノイダル閉圏では評価・カリー化はあってもΔと!は得られません。従って変数を複製・未使用にする構造規則は閉性でなくデカルト性に由来します。

線形ラムダ計算と通常のラムダ計算の差を、内部homの有無でなく資源管理射の有無として説明します。

第71章

単純型付きラムダ計算の圏論的意味論——判断を射へ移す

問題1全ての構文的代入について意味論的置換補題を証明する

Problem

問題

Substitution Γ Δ を環境射 ⟦Δ⟧→⟦Γ⟧ へ再帰的に解釈してください。変数について射影との可換性を示し、 Tm の変数・適用・抽象の場合で ⟦substitute σ t⟧=⟦t⟧∘⟦σ⟧ を証明します。抽象の場合に liftSubstitution と文脈積の結合がどう対応するかを明示できれば完了です。

ヒント

項tへの構造帰納を行い、変数・組・射影・ラムダ・適用をすべて扱います。

解答

代入 σ:Δ⇒Γ の意味を文脈対象間の射 ⟦σ⟧:⟦Δ⟧→⟦Γ⟧ とすると、主張は ⟦t[σ]⟧=⟦σ⟧≫⟦t⟧。変数では射影と代入タプルの定義、組と射影では積のβη則、適用では評価射の自然な計算、ラムダでは指数随伴の自然性を使います。各構文子で構文的代入が意味射の合成へ移ることを示し、同時に恒等代入・合成代入も恒等射・合成へ送られます。

依存型では通常の前合成を再添字付けへ置き換え、同じ置換補題をcoherence付きで証明します。

問題2β・η以外の等式をモデルで検査する

Problem

問題

合成関数、定数関数、引数交換を表す閉じた Tm を構成し、denoteTm を計算してください。同じ型を持つが βη同値でない二項を有限な原子型モデルで区別し、モデルが項等式の反例を与える仕組みを示します。まず原子型を Bool とし、二項の表示が異なる入力を一つ具体的に与えます。次に原子型を一元型へ変えると、構文の異なる項が同じ関数を表す場合を探してください。この対比により、一つのモデルで等しいことは構文的等式の証明にならないが、一つのモデルで異なることは全モデルに対する等式の反例になる、と量化の向きを説明します。各項の型、区別に使う入力、Leanで検査した不等式、二種類の量化を明記できれば完了です。

ヒント

候補等式が全デカルト閉圏で成立するか、有限集合モデルなどで反例を探します。

解答

βη等式と積の法則はすべてのデカルト閉圏モデルで成立します。例えば異なる自由変数x,yを無条件に同一視する等式は、 Type でBoolを解釈しx=true,y=falseとすれば失敗します。自然数定数など追加構造の等式は、その構造の公理を持つモデルだけで検査します。あるモデルで意味が異なれば構文理論から導出不能ですが、あるモデルで一致するだけでは導出可能性は証明できません。

健全性で反例モデルを導出不能性へ使い、完全性がある場合だけ全モデル妥当性から導出を回収します。

Lean検査済みL359–380

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

問題3構文圏の対象・射・合成を設計する

Problem

問題

対象を単純型、射 A→B を一変数文脈の項 A⊢t:B のβη同値類として定義してください。恒等射を変数、合成を代入で作り、well-definednessと圏法則に必要な補題を列挙します。積と指数対象の候補を構成し、この圏が原子型一つ上の自由デカルト閉圏になるという普遍性を正確に述べられれば完了です。

ヒント

対象を型、射A→Bを一変数文脈 x:A⊢t:B のβη同値類とします。

解答

恒等射は変数項x、合成は項代入です。代入の単位・結合性が同値類上の圏法則を与えます。積対象は積型、終対象はUnit、指数対象は関数型で、構文的組・射影・ラムダ・適用が普遍射になります。βη等式により普遍性の逆法則が成立します。この構文圏から任意のモデルへの構造保存関手は型・定数の解釈により一意で、構文圏の初期性を表します。

構文圏を自由な意味論的構造として作ると、再帰的な解釈定義と健全性を普遍性へまとめられます。

問題4構造規則が意味射のどこに現れるかを追跡する

Problem

問題

弱化を snd≫f、縮約を対角射、交換を積の対称性として書いてください。interpretApplication が同じ文脈を関数と引数の双方へ渡す際に縮約を使うことを図式で示します。これらの射を持たないモノイダル閉圏へ移したとき、通常のSTLCのどの項が解釈できなくなるかを K・W combinatorで検査できれば完了です。

ヒント

弱化は終対象への射、縮約は対角射、交換は積の対称性として文脈射を作ります。

解答

変数を使わない弱化は Γ×A→Γ という射影、またはAから終対象への一意射で成分を捨てる操作です。同じ変数を二回使う縮約は Γ→Γ×Γ の対角射。変数順の交換は積の対称同型です。結合的な文脈再括弧付けは積の結合同型に対応します。これらがデカルト構造から自然に得られるため、通常のSTLCでは構造規則を自由に使えます。

線形論理では対応射を一般には持たないモノイダル圏を選び、資源使用制約を意味論に反映します。

第72章

スライス圏・添字圏・ファイブレーション——変化する文脈の上で対象を運ぶ

問題1`Type` の引戻しの普遍性を同値としてまとめる

Problem

問題

TypePullback f p からの関数と、f∘q=p∘r を満たす関数対 (q,r) の間の同値を構成してください。 typePullbackLift を一方向、二射影を逆方向とし、typePullbackLift_unique で一方の逆法則を証明します。もう一方は関数外延性と部分型の外延性で示します。可換条件をデータとして持つ場合と命題として外に置く場合で、同値の型がどう変わるかも記述できれば完了です。

ヒント

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スライス圏の射を手で合成する

Problem

問題

p:E⟶I, q:F⟶I, r:G⟶I と可換三角形 h:E⟶F, k:F⟶G を取り、 sliceMorphism h と sliceMorphism k の合成を作ってください。その left が h≫k であることと、終域 I への三角形が可換であることをLeanで示します。次に三角形の仮定を一つ削り、Over.homMk を構成できない具体例を Type で与えます。対象、射、保存すべき構造をそれぞれ特定できれば完了です。

ヒント

Γ上の対象 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。圏法則は基礎圏の法則を継承し、可換証明は命題成分なので射の等しさは基礎射の等しさへ還元できます。

文脈Γ上の型を表示射として扱い、型間の写像を文脈を変えないスライス射として表します。

Lean検査済みL386–412

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

問題3二回の再添字付けを一回の再添字付けと比較する

Problem

問題

f:I⟶J, g:J⟶K に沿う選ばれた引戻しについて、(g≫f)⁎ ではなく合成順を正しく追い、 ChosenPullbacksAlong.pullbackComp が与える自然同型の両辺を書き下してください。Type の明示的な引戻しでは対応する全単射を構成し、なぜ一般圏では定義的等号を要求しないのかを説明します。恒等射の場合も pullbackId と比較し、擬関手の二つの単位・合成制約を復元できれば完了です。

ヒント

型族P:Γ→Typeを f:Δ→Γ、g:Θ→Δ に沿って前合成します。

解答

集合族では g*(f*P)(θ)=f*P(gθ)=P(f(gθ))=((f∘g)*P)(θ) なので定義的に一致します。表示射の引戻しとして構成すると、二段引戻しと合成に沿う一段引戻しは一般に標準同型であり、選んだ引戻しによって定義的等号とは限りません。この同型は恒等再添字付けと合成についてcoherenceを満たし、擬関手構造を作ります。

証明支援系の置換を厳密に結合的にするstrictificationと、同型を追跡する設計を比較します。

問題4Cartesian持ち上げの一意性を図式で証明する

Problem

問題

同じ基底射 f:R⟶S と同じ終域 a に対する二つのCartesian射 φ:b⟶a, ψ:c⟶a を仮定します。各普遍性から垂直比較射 b⟶c, c⟶b を作り、その合成が恒等射になることを一意性で証明してください。得られるのは全圏での任意の同型ではなく、基底の恒等射上にある垂直同型です。mathlibの Functor.IsCartesian.domainUniqueUpToIso と照合し、どの仮定が各逆法則に使われたかを示せれば完了です。

ヒント

同じ基底射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普遍性から得る標準同型で交換できます。

問題5Grothendieck構成の射を依存対として読む

Problem

問題

反変擬関手 F:Bᵒᵖ→Cat に対する ∫F の対象と射を、基底成分とファイバー成分へ分解して書いてください。恒等射と合成で擬関手の単位・合成同型が必要になる箇所を追跡します。その後、射影がCartesian持ち上げを持つことを単位ファイバー射から説明し、Pseudofunctor.CoGrothendieck.cartesianLift と比較してください。厳密関手だけを使った場合に消える輸送と、擬関手の場合に残る整合条件を区別できれば完了です。

ヒント

擬関手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二つの型族随伴の自然性を証明する

Problem

問題

sigmaReindexEquiv と reindexPiEquiv が単なる型ごとの全単射ではなく、両方の型族変数について自然であることを証明してください。前合成と後合成に対して各図式を書き、関数外延性で示します。どの等式が rfl で、どこで添字等式による輸送が必要かを記録し、随伴のhom同値として必要な自然性を全て列挙できれば完了です。

ヒント

Σ_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空ファイバーと多元ファイバーで依存積を計算する

Problem

問題

f:Bool→Unit と具体的な型族 B:Bool→Type を取り、piFamily f B () が B false×B true と同じ情報を持つことを相互の関数で示してください。次に空型から Unit への関数を使い、逆像が空のとき依存積が一元型になることを示します。同じ例で sigmaFamily も計算し、空和・二項和との違いを説明できれば完了です。

ヒント

(Π_f A)(γ)=Π_{δ:fδ=γ}Aδ の添字型の要素数を場合分けします。

解答

γ上のfのファイバーが空なら、空族への依存関数は一つだけなので (Π_f A)(γ) はUnitに同型です。一要素なら対応する Aδ、多要素なら各δのAδの積になります。対してΣ_fは空ファイバーでEmpty、多要素で直和です。零項積が終対象、零項和が始対象になる一般則がファイバーごとに現れます。

データベースのgroup-byで、キーごとの行集合上の全称制約・集約を依存積として読めます。

問題3通常のカリー化を依存カリー化から回収する

Problem

問題

終対象への射 A⟶1 に沿う引戻しを考え、C/1 と C の同値を通じて Π_f が指数対象 (-)^A に対応することを図式で示してください。Type では定数族を用いて reindexPiEquiv を通常の (A×X→B)≃(X→A→B) と比較します。スライス同値、引戻し、hom同値の三段階を明記できれば完了です。

ヒント

射影 π:Γ×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合成に沿う依存積の比較同型を追跡する

Problem

問題

指数化可能な f:I⟶J, g:J⟶K について Π_{f≫g} と Π_g∘Π_f の向きを確認し、mathlibの pushforwardComp f g の型を書き下してください。この同型が右随伴の一意性から得られる証明を再構成し、対応する左随伴側の pullbackComp がどこで使われるかを示します。等号ではなく自然同型で十分な理由も説明してください。

ヒント

f:Δ→Γ,g:Θ→Δ に対し、右随伴の合成が合成再添字付けの右随伴になることを使います。

解答

再添字付けは (f∘g)*≅g*∘f*。右随伴は順を反転して Π_{f∘g}≅Π_f∘Π_g になります。両者が同じ関手の右随伴であるため、随伴の一意性から標準自然同型が得られます。型族では、合成写像のファイバー上の依存関数と、まずgのファイバー、次にfのファイバーでカリー化した関数が対応します。

多重Σ・ΠのFubini則や量化子の入れ子変更を、随伴の一意性で導きます。

問題5局所デカルト閉性の二つの定義を結ぶ

Problem

問題

有限極限を持つ圏について、全スライス C/I がデカルト閉であることから全射の指数化可能性を導く構成と、逆向きの構成を概説してください。各方向で積、引戻し、指数対象、右随伴のどれを使うかを図式にします。証明に必要な有限極限の仮定を曖昧な「十分よい圏」へ隠さず、既知の定理として引用する部分と自分で構成する部分を分けられれば完了です。

ヒント

全スライスがデカルト閉であることと、各fの再添字付けが右随伴Π_fを持つことを往復します。

解答

全スライスがデカルト閉なら、f:Δ→Γに対する再添字付けはスライスの積でfを引き戻す操作と見なせ、その指数構造から右随伴 Π_fを構成できます。逆にすべてのf*が右随伴を持てば、スライスC/ΓでA→Γとの積はAへの再添字付けを含む合成で表され、 Πを使って指数対象を構成できます。有限極限がスライスと引戻しを支える共通前提です。

局所デカルト閉圏を依存積型の意味論と見る際、採用する同値な定義と必要な有限極限を明記します。

第74章

依存型理論の圏論的意味論——文脈・型・項・代入を再構成する

問題1`Type` モデルをcategory with familiesの法則として整理する

Problem

問題

SemanticContext, SemanticType, SemanticTerm, extendContext を用い、CwFの基礎データを一つの構造体へまとめてください。型・項の恒等置換と合成置換、文脈拡張の射影・変数・対形成について必要な法則を全て列挙します。本章の rfl で済む法則と関数外延性を要する法則を分類し、構文に近い厳密モデルになっている理由を説明できれば完了です。

ヒント

文脈を型Γ、型を族A:Γ→Type、項を切断、代入を関数として各操作を列挙します。

解答

文脈圏はTypeと関数です。Γ上の型はA:Γ→Type、項は a:Πγ,Aγ。代入 σ:Δ→Γ に沿う再添字付けは A[σ](δ)=A(σδ)、項は a[σ](δ)=a(σδ)。文脈拡張は Γ.A=Σγ,Aγ、射影pは第一射影、標準項qは第二射影です。組 ⟨σ,a⟩:Δ→Γ.A は (σδ,aδ)。恒等・合成置換、p/qのβ則、組のη則はいずれも関数計算です。

抽象モデルでは同じインターフェースを保ち、定義的等号が同型になる箇所だけcoherenceとして分離します。

問題2項と表示射の切断の同値を証明する

Problem

問題

Type で型族 A:Γ→Type を全空間射 Sigma.fst:Σγ,Aγ→Γ に変換してください。依存項 t:∀γ,Aγ から切断 γ↦(γ,tγ) を作り、逆に切断から第二成分を回収します。二操作が互いに逆であることを示し、切断条件が項の型付けをどのように保証するかを一般圏の CategoricalTerm と比較できれば完了です。

ヒント

項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依存積のβη則を随伴の三角恒等式へ翻訳する

Problem

問題

dependent_beta と dependent_eta を、p_A⁎⊣Π_{p_A} の単位・余単位を用いる可換図式へ翻訳してください。抽象、適用、本体、引数がどのスライス圏のどの射になるかを明記します。第73章の pushforwardCurry と pushforwardUncurry を使い、二つの逆法則がどの三角恒等式に対応するかを追跡できれば完了です。

ヒント

表示射p:Γ.A→Γに沿う再添字付け p* と右随伴Π_pを使います。

解答

依存ラムダ抽象はhom同型 Hom_{Γ.A}(p*X,B)≅Hom_Γ(X,Π_pB) の転置、適用は逆転置です。抽象後に適用すると元の射へ戻るβ則、関数を適用形へして再抽象すると元へ戻るη則は、hom同型の二逆法則です。単位・余単位表示では随伴の二つの三角恒等式になります。置換に対する安定性はこのhom同型の自然性に対応します。

Σ型・同一性型についても、導入除去規則を普遍性と計算則へ分解して意味づけます。

問題4置換のcoherence問題を具体例で示す

Problem

問題

選ばれた引戻しについて (σ≫τ)⁎A と τ⁎(σ⁎A) を比較し、自然同型はあるが定義的等号とは限らないことを示してください。対照として Type モデルの substituteType_comp が rfl になる理由を展開します。型理論の変換規則が判断的等しさを要求する場合に、同型だけのモデルをそのまま使えない箇所を一つ特定できれば完了です。

ヒント

二段引戻し (fg)*A と g*(f*A) が選択した引戻しでは等しくなく同型だけになる例を考えます。

解答

抽象圏で各引戻しを個別に選ぶと、合成射に沿って直接選んだ対象と二回引き戻して得た対象は普遍性により標準同型ですが、同じ対象として定義されるとは限りません。すると構文の厳密な式 A[f][g]=A[f∘g] はモデルで同型としてしか成立せず、三重置換では比較同型同士の五角形的coherenceも必要です。split fibrationや局所宇宙構成で選択を厳密化できます。

定義等式を意味づける際は「同型を除いて」だけでは不十分で、厳密化またはcoherence定理を用意します。

問題5外延的同一性型と内包的同一性型を分離する

Problem

問題

LCCCの対角射による外延的解釈を図示し、反射、J、等式反映のうち何が成立するかを調べてください。次に複数の経路を持つ群oidまたは位相的な例を挙げ、対角部分対象だけでは失われる情報を説明します。必要な追加構造を「よい経路対象」のような曖昧語で済ませず、少なくとも因子分解、安定性、除去則の解釈に分けて述べてください。

ヒント

反射規則・J消去に加え、等式反映と証明無関連性を持つか比較します。

解答

内包的同一性型は項 p:Id_A(a,b) をデータとして保持し、Jによりreflの場合へ帰納しますが、pの存在からaとbが定義的に同じとはしません。外延的体系では等式反映によりpから判断的等式a≡bを得るため、型検査の変換可能性へ証明探索が入り得ます。圏論モデルでは対角射の因子化やpath objectが内包的構造を、対角部分対象に近い厳格な解釈が外延的構造を表します。

モデルの同一性型を述べるとき、反射・J・計算則・η・等式反映のどこまでを検証したか明記します。

問題6構文モデルの初期性を正確に述べる

Problem

問題

対象を文脈、射を代入とする構文圏を設計し、型と項をどの同値関係で割るかを指定してください。Π・Σ・同一性型を保つモデル射の定義を与え、その圏で構文モデルが初期であるという定理を量化記号つきで述べます。健全性と完全性が初期性のどの部分から従うかを区別し、証明に必要な置換補題を列挙できれば完了です。