import FormalLab.Bridges.LocallyCartesianClosedCategories
import FormalLab.TypeTheory.IdentityTypes

/-!
# 第74章：依存型理論の圏論的意味論——文脈・型・項・代入を再構成する

単純型付きラムダ計算では、型を対象、文脈を有限積、項判断 `Γ⊢t:A` を射 `Γ→A` として解釈しました。
依存型理論では型 `A` 自身が文脈 `Γ` に依存します。したがって `A` を圏の一対象へ送るだけでは、代入によって
`A[σ]` が変わることも、項 `t` が各文脈値に応じて適切なファイバーへ入ることも記録できません。

本章では最初に `Type` の標準モデルを作り、次の四判断を区別します。

$$
\Gamma\;\mathsf{ctx},
\qquad
\Gamma\vdash A\;\mathsf{type},
\qquad
\Delta\vdash\sigma:\Gamma,
\qquad
\Gamma\vdash t:A.
$$

次に一般圏で、文脈を対象、文脈上の型をスライス対象 `p_A:Γ.A→Γ`、項を `p_A` の切断、代入を引戻しとして
読み直します。依存和と依存積は第73章の三随伴へ接続します。同一性型については、局所デカルト閉性だけで得る
外延的解釈と、内包的な経路情報を保持するモデルを分けます。

## `Type` の標準モデルで四判断を分ける

文脈を型、代入を関数、文脈 `Γ` 上の型を型族 `Γ→Type`、項を各ファイバーの値を選ぶ依存関数とします。

$$
\llbracket\Gamma\vdash A\;\mathsf{type}\rrbracket:
\llbracket\Gamma\rrbracket\to\mathsf{Type},
\qquad
\llbracket\Gamma\vdash t:A\rrbracket:
\prod_{\gamma:\llbracket\Gamma\rrbracket}\llbracket A\rrbracket(\gamma).
$$
-/

namespace FormalLab.Bridges.DependentTypeCategoricalSemantics

universe u

abbrev SemanticContext := Type u

abbrev SemanticSubstitution (Δ Γ : SemanticContext) := Δ → Γ

abbrev SemanticType (Γ : SemanticContext) := Γ → Type u

abbrev SemanticTerm (Γ : SemanticContext) (A : SemanticType Γ) := (γ : Γ) → A γ

def identitySubstitution (Γ : SemanticContext) : SemanticSubstitution Γ Γ := id

def composeSubstitution {Γ Δ Θ : SemanticContext}
    (σ : SemanticSubstitution Δ Γ) (τ : SemanticSubstitution Θ Δ) :
    SemanticSubstitution Θ Γ :=
  σ ∘ τ

def substituteType {Γ Δ : SemanticContext} (σ : SemanticSubstitution Δ Γ)
    (A : SemanticType Γ) : SemanticType Δ :=
  A ∘ σ

def substituteTerm {Γ Δ : SemanticContext} {A : SemanticType Γ}
    (σ : SemanticSubstitution Δ Γ) (t : SemanticTerm Γ A) :
    SemanticTerm Δ (substituteType σ A) :=
  fun δ => t (σ δ)

theorem substituteType_id {Γ : SemanticContext} (A : SemanticType Γ) :
    substituteType (identitySubstitution Γ) A = A := rfl

theorem substituteType_comp {Γ Δ Θ : SemanticContext}
    (σ : SemanticSubstitution Δ Γ) (τ : SemanticSubstitution Θ Δ) (A : SemanticType Γ) :
    substituteType τ (substituteType σ A) = substituteType (composeSubstitution σ τ) A := rfl

theorem substituteTerm_id {Γ : SemanticContext} {A : SemanticType Γ}
    (t : SemanticTerm Γ A) :
    substituteTerm (identitySubstitution Γ) t = t := by
  funext γ
  rfl

theorem substituteTerm_comp {Γ Δ Θ : SemanticContext} {A : SemanticType Γ}
    (σ : SemanticSubstitution Δ Γ) (τ : SemanticSubstitution Θ Δ) (t : SemanticTerm Γ A) :
    substituteTerm τ (substituteTerm σ t) =
      substituteTerm (composeSubstitution σ τ) t := by
  funext θ
  rfl

/-!
型の代入と項の代入はどちらも関数合成ですが、結果の種類が違います。`substituteType σ A` は新しい型族、
`substituteTerm σ t` はその型族の各ファイバーに入る項です。二つを一つの「置換関数」として扱うと、項の結果型が
型の置換と同期して変わる条件を失います。

`Type` モデルでは恒等則と合成則が `rfl` です。一般の選ばれた引戻しでは自然同型を介する場合があり、この差が
モデルのcoherence問題につながります。

## 文脈拡張は型族の全空間である

`Γ` 上の型 `A` を文脈へ加えた `Γ.A` は依存和 `Σγ:Γ,A(γ)` です。第一射影が文脈射影
`p_A:Γ.A→Γ`、第二成分が拡張文脈で利用できる最新変数になります。
-/

def extendContext {Γ : SemanticContext} (A : SemanticType Γ) : SemanticContext :=
  Sigma A

def contextProjection {Γ : SemanticContext} {A : SemanticType Γ} :
    SemanticSubstitution (extendContext A) Γ :=
  Sigma.fst

def contextVariable {Γ : SemanticContext} {A : SemanticType Γ} :
    SemanticTerm (extendContext A) (substituteType contextProjection A) :=
  Sigma.snd

def contextPairing {Γ Δ : SemanticContext} {A : SemanticType Γ}
    (σ : SemanticSubstitution Δ Γ) (t : SemanticTerm Δ (substituteType σ A)) :
    SemanticSubstitution Δ (extendContext A) :=
  fun δ => ⟨σ δ, t δ⟩

theorem contextProjection_pairing {Γ Δ : SemanticContext} {A : SemanticType Γ}
    (σ : SemanticSubstitution Δ Γ) (t : SemanticTerm Δ (substituteType σ A)) :
    contextProjection ∘ contextPairing σ t = σ := rfl

theorem contextVariable_pairing {Γ Δ : SemanticContext} {A : SemanticType Γ}
    (σ : SemanticSubstitution Δ Γ) (t : SemanticTerm Δ (substituteType σ A)) :
    (fun δ => contextVariable (contextPairing σ t δ)) = t := rfl

theorem contextPairing_eta {Γ : SemanticContext} {A : SemanticType Γ} :
    contextPairing contextProjection contextVariable =
      (identitySubstitution (extendContext A)) := by
  funext extended
  cases extended
  rfl

/-!
二つのβ則は、対を作ってから第一成分または第二成分を読む計算です。η則は、射影と最新変数から拡張文脈の値を
完全に復元できることを述べます。したがって文脈拡張は単なる二項積ではなく、第二成分の型が第一成分に依存する
普遍的な対です。

## 依存和を文脈の中で解釈する

`A` が `Γ` 上の型、`B` が拡張文脈 `Γ.A` 上の型なら、`Σ_A B` の `γ` 上の要素は
`a:A(γ)` と `b:B(γ,a)` の依存対です。
-/

def sigmaType {Γ : SemanticContext} (A : SemanticType Γ)
    (B : SemanticType (extendContext A)) : SemanticType Γ :=
  fun γ => Σ a : A γ, B ⟨γ, a⟩

def sigmaPair {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)}
    (a : SemanticTerm Γ A)
    (b : (γ : Γ) → B ⟨γ, a γ⟩) : SemanticTerm Γ (sigmaType A B) :=
  fun γ => ⟨a γ, b γ⟩

def sigmaFirst {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)}
    (pair : SemanticTerm Γ (sigmaType A B)) : SemanticTerm Γ A :=
  fun γ => (pair γ).1

def sigmaSecond {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)}
    (pair : SemanticTerm Γ (sigmaType A B)) :
    (γ : Γ) → B ⟨γ, sigmaFirst pair γ⟩ :=
  fun γ => (pair γ).2

theorem sigma_eta {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)} (pair : SemanticTerm Γ (sigmaType A B)) :
    sigmaPair (sigmaFirst pair) (sigmaSecond pair) = pair := by
  funext γ
  change ⟨(pair γ).1, (pair γ).2⟩ = pair γ
  exact Sigma.eta (pair γ)

/-!
`sigmaSecond` の結果型には `sigmaFirst pair γ` が現れます。第一射影と第二射影を独立な通常関数として定義すると、
この依存関係を表せません。Leanの型が、第二成分をどのファイバーから取り出したかを保持します。

## 依存積を抽象と適用で解釈する

同じ `A` と `B` に対し、`Π_A B` の `γ` 上の要素は全ての `a:A(γ)` へ `B(γ,a)` の値を返す依存関数です。
-/

def piType {Γ : SemanticContext} (A : SemanticType Γ)
    (B : SemanticType (extendContext A)) : SemanticType Γ :=
  fun γ => (a : A γ) → B ⟨γ, a⟩

def dependentLambda {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)} (body : SemanticTerm (extendContext A) B) :
    SemanticTerm Γ (piType A B) :=
  fun γ a => body ⟨γ, a⟩

def dependentApplication {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)}
    (function : SemanticTerm Γ (piType A B)) (argument : SemanticTerm Γ A) :
    (γ : Γ) → B ⟨γ, argument γ⟩ :=
  fun γ => function γ (argument γ)

theorem dependent_beta {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)} (body : SemanticTerm (extendContext A) B)
    (argument : SemanticTerm Γ A) :
    dependentApplication (dependentLambda body) argument =
      fun γ => body ⟨γ, argument γ⟩ := rfl

theorem dependent_eta {Γ : SemanticContext} {A : SemanticType Γ}
    {B : SemanticType (extendContext A)} (function : SemanticTerm Γ (piType A B)) :
    dependentLambda (fun extended => function extended.1 extended.2) = function := by
  funext γ a
  rfl

/-!
β則は抽象した本体へ引数を代入する計算、η則は依存関数が全ての適用結果から復元されることです。通常の関数型は
`B(γ,a)` が `a` に依存しない場合として回収されます。

## 同一性型はファイバー内の等式を分類する

`A` の二項 `a,b` に対し、標準 `Type` モデルでは `Id_A(a,b)` を各 `γ` でのLeanの等式
`a(γ)=b(γ)` として解釈できます。本章の型族は `Type` 値なので、`Prop` に属する等式を `PLift` で
持ち上げます。これは論理内容を変えずにsortを合わせる操作です。反射項と輸送は第32章の同一性型規則に対応します。
-/

def identityType {Γ : SemanticContext} {A : SemanticType Γ}
    (a b : SemanticTerm Γ A) : SemanticType Γ :=
  fun γ => PLift (a γ = b γ)

def reflexivityTerm {Γ : SemanticContext} {A : SemanticType Γ}
    (a : SemanticTerm Γ A) : SemanticTerm Γ (identityType a a) :=
  fun _ => ⟨rfl⟩

def transportTerm {Γ : SemanticContext} {A : SemanticType Γ}
    (B : (γ : Γ) → A γ → Type u)
    {a b : SemanticTerm Γ A} (path : SemanticTerm Γ (identityType a b))
    (value : (γ : Γ) → B γ (a γ)) : (γ : Γ) → B γ (b γ) :=
  fun γ => (path γ).down ▸ value γ

theorem transportTerm_refl {Γ : SemanticContext} {A : SemanticType Γ}
    (B : (γ : Γ) → A γ → Type u) (a : SemanticTerm Γ A)
    (value : (γ : Γ) → B γ (a γ)) :
    transportTerm B (reflexivityTerm a) value = value := by
  funext γ
  rfl

/-!
このモデルの等式はLeanの `Prop` に入り、証明無関連です。したがって高次経路をデータとして保持する内包的
同一性型やHoTTのモデルを、この定義から得たとはいえません。標準集合的モデルが検査する規則と、対象理論の
同一性証拠が持ちうる高次構造を区別します。

## 一般圏では型は表示射、項は切断になる

圏 `C` の対象 `Γ` を文脈とします。`Γ` 上の型はスライス圏 `C/Γ` の対象、すなわち表示射
`p_A:Γ.A⟶Γ` です。項は `p_A` の切断 `s:Γ⟶Γ.A` で `s≫p_A=𝟙Γ` を満たすものです。

$$
p_A:\Gamma.A\to\Gamma,
\qquad
s_t:\Gamma\to\Gamma.A,
\qquad
s_t;p_A=\mathrm{id}_\Gamma.
$$

mathlibでは恒等射をスライス対象にした `Over.mk (𝟙 Γ)` から `A:Over Γ` への射が、まさにその切断を表します。
-/

open _root_.CategoryTheory

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable {Γ Δ : C}

abbrev CategoricalType (Γ : C) := Over Γ

abbrev CategoricalTerm {Γ : C} (A : CategoricalType Γ) :=
  Over.mk (𝟙 Γ) ⟶ A

def termSection {A : CategoricalType Γ} (t : CategoricalTerm A) : Γ ⟶ A.left :=
  t.left

theorem termSection_fac {A : CategoricalType Γ} (t : CategoricalTerm A) :
    termSection t ≫ A.hom = 𝟙 Γ :=
  Over.w t

def termFromSection {A : CategoricalType Γ} (s : Γ ⟶ A.left)
    (fac : s ≫ A.hom = 𝟙 Γ) : CategoricalTerm A :=
  Over.homMk s fac

/-!
`CategoricalTerm A` の型そのものが可換三角形を要求するため、任意の射 `Γ→Γ.A` を項とは呼べません。表示射との
合成が恒等射になることが、各 `γ` に対して結果が `A(γ)` のファイバーへ入るという型付け条件です。

## 型の代入は表示射の引戻しである

代入 `σ:Δ⟶Γ` に沿う型 `A[σ]` は、表示射 `p_A` を `σ` に沿って引き戻した `Δ` 上の対象です。
-/

open ChosenPullbacksAlong

def categoricalSubstituteType (σ : Δ ⟶ Γ) [ChosenPullbacksAlong σ]
    (A : CategoricalType Γ) : CategoricalType Δ :=
  (pullback σ).obj A

/-!
引戻し正方形は、拡張文脈と代入が両立することを表します。項の代入は切断をこの正方形へ持ち上げて得られます。
選ばれた引戻しでは恒等・合成との両立が一般に自然同型なので、構文の厳密な置換則と意味論の同型による置換則の間に
coherence問題が生じます。CwFやcontextual categoryは、この文脈依存データを構文に近い厳密さで編成する枠組みです。

## 依存和は表示射の合成、依存積は右随伴である

`A:Over Γ` と `B:Over A.left` を取ります。依存和 `Σ_A B` の表示射は `B.hom≫A.hom`、すなわち二つの
文脈拡張の合成です。依存積 `Π_A B` は `A.hom` に沿う引戻しの右随伴で作ります。
-/

def categoricalSigma (A : CategoricalType Γ) (B : CategoricalType A.left) :
    CategoricalType Γ :=
  (Over.map A.hom).obj B

open ExponentiableMorphism

def categoricalPi (A : CategoricalType Γ) (B : CategoricalType A.left)
    [ChosenPullbacksAlong A.hom] [ExponentiableMorphism A.hom] : CategoricalType Γ :=
  (pushforward A.hom).obj B

/-!
この二構成は `Σ_{p_A}⊣p_A⁎⊣Π_{p_A}` の両端です。依存積の導入・除去・βη則は随伴のhom同値と三角恒等式へ
移ります。依存和の対形成と除去は、表示射の合成とスライス圏の普遍性から読み取ります。

## 同一性型に必要な構造を分ける

同じ型 `A` の二変数を持つ文脈は引戻し `Γ.A×_ΓΓ.A` で表されます。対角射
`δ:Γ.A→Γ.A×_ΓΓ.A` は反射項の候補です。外延的同一性型では、この対角に対応する表示を使い、等式証拠から
端点の等しさを強く反映させます。

しかし内包的同一性型では、等式証拠は反射だけに潰れず、異なる経路や高次等式を持ちえます。bareな局所デカルト閉圏
だけでは、そのような経路対象と `J` の安定な解釈は指定されません。弱因子分解系、モデル圏、カテゴリー付き族に
追加したidentity-type structureなど、対象とする型理論に応じた構造が必要です。

## 健全性・完全性・初期性

モデルに構文を解釈して各規則が保存されることが健全性です。逆にモデルで成立する等式を構文で導出できることが
完全性です。構文そのものから文脈と代入の圏を作り、それが指定したモデル構造の初期対象になるという主張は、
健全性と完全性を普遍性としてまとめます。

本章のLeanコードは `Type` モデルの基本規則と一般圏での対応対象を形式化します。任意の依存型構文、全ての
置換補題、構文CwFの初期性、LCCCとの双圏同値を証明したものではありません。これらを区別することが、個々の
計算例をメタ理論全体と誤認しないために必要です。

## 対応表

| 依存型理論 | `Type` の標準モデル | 一般圏での意味 |
|---|---|---|
| 文脈 `Γ` | 型 | 対象 `Γ:C` |
| 代入 `Δ⊢σ:Γ` | 関数 `Δ→Γ` | 射 `Δ⟶Γ` |
| 型 `Γ⊢A` | 型族 `Γ→Type` | 表示射 `Γ.A⟶Γ` |
| 項 `Γ⊢t:A` | 依存関数 `∀γ,Aγ` | 表示射の切断 |
| 型の代入 `A[σ]` | 型族の合成 | 表示射の引戻し |
| 文脈拡張 `Γ.A` | `Σγ,Aγ` | 表示射の始域 |
| 依存和 `Σ_A B` | 入れ子のΣ型 | 表示射の合成 |
| 依存積 `Π_A B` | 入れ子のΠ型 | 引戻しの右随伴 |
| 同一性型 | ファイバー内の等式 | 対角・経路対象に追加構造が必要 |

## 要点

* 依存型の意味論では、文脈・型・項・代入を異なる種類のデータとして解釈する。
* 文脈上の型は表示射、項はその切断、型の代入は引戻しになる。
* 文脈拡張は型族の全空間であり、射影・変数・対形成のβη則を持つ。
* 依存和は表示射の合成、依存積は再添字付けの右随伴として解釈される。
* LCCCはΠ・Σを持つ外延的意味論の主要な基盤だが、内包的同一性型の全構造を単独では与えない。
* 健全性、完全性、構文モデルの初期性、モデル概念間の同値は別々に証明すべき定理である。

## 研究史と文献案内

Martin-Löf [ML84] は依存型、Π・Σ・同一性型を判断と規則から与える構文側の基準文献です。Cartmell [CAR78] は
一般化代数理論とcontextual categoryを通じて、文脈と代入の代数的意味論を構成しました。Dybjer [DYB96] の
category with familiesは、文脈・型・項・代入を構文に近いデータとしてまとめます。同論文は、これらを内部化するときの
coherence問題も明示します。

LCCCと型理論の関係には Seely [SEE84] を参照してください。ファイブレーションを基盤とする体系的な扱いは
Jacobs [JAC99] にあります。構文と意味論の比較および外延的・内包的構成の境界は Hofmann [HOF97] が扱います。
本章の `Over`、引戻し、
`ExponentiableMorphism` は [MATHLIB] の現行APIに従います。

## 問題

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

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

### 項と表示射の切断の同値を証明する

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

### 依存積のβη則を随伴の三角恒等式へ翻訳する

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

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

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

### 外延的同一性型と内包的同一性型を分離する

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

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

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

end FormalLab.Bridges.DependentTypeCategoricalSemantics