import Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
import FormalLab.Bridges.CartesianClosedCategories
import FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations

/-!
# 第73章：局所デカルト閉圏——依存積を再添字付けの右随伴として捉える

デカルト閉圏では、固定した型 `A` を文脈へ加える関手 `A×-` に右随伴 `A⇒-` がありました。依存型では、
追加する型が文脈の値によって変わります。したがって一つの積関手だけでなく、全ての文脈写像 `f:I→J` に沿う
再添字付け `f⁎` と、その右随伴を同時に扱う必要があります。

局所デカルト閉圏（locally cartesian closed category）は、各スライス圏 `C/I` がデカルト閉圏である圏です。
同じ条件は、適切な引戻しの仮定の下で、全ての射 `f:I⟶J` に沿う引戻し関手

$$
f^*:\mathcal C/J\longrightarrow\mathcal C/I
$$

が右随伴 `Π_f : C/I→C/J` を持つこととして読めます。本章では `Type` 上の型族で
`Σ_f ⊣ f⁎ ⊣ Π_f` を要素ごとに構成し、一般圏の随伴と比較します。

## 型族の間の射

同じ添字型 `I` 上の型族 `A,B:I→Type` の間の射を、各ファイバーの関数族
`∀i,A(i)→B(i)` とします。これは `Type/I` の射を型族表示へ移したものです。
-/

namespace FormalLab.Bridges.LocallyCartesianClosedCategories

universe u

abbrev Family (I : Type u) := I → Type u

abbrev FamilyHom {I : Type u} (A B : Family I) := ∀ i, A i → B i

def reindexFamily {I J : Type u} (f : I → J) (A : Family J) : Family I :=
  fun i => A (f i)

theorem reindexFamily_id {I : Type u} (A : Family I) :
    reindexFamily id A = A := rfl

theorem reindexFamily_comp {I J K : Type u} (f : I → J) (g : J → K) (A : Family K) :
    reindexFamily f (reindexFamily g A) = reindexFamily (g ∘ f) A := rfl

/-!
再添字付けは型族を関数と合成するだけなので、恒等と合成を定義的に保ちます。一般圏で選んだ引戻しを使う場合は、
この二法則が自然同型になることを第72章で確認しました。`Type` のこの厳密な表示を、一般の場合へ無条件に
持ち込んではいけません。

## 依存和は再添字付けの左随伴である

`f:I→J` と `B:I→Type` に対し、`Σ_f B` の `j` 上の要素は、`f(i)=j` となる添字 `i`、その等式、
要素 `b:B(i)` の組です。
-/

structure SigmaFiber {I J : Type u} (f : I → J) (B : Family I) (j : J) where
  index : I
  value : B index
  equation : f index = j

def sigmaFamily {I J : Type u} (f : I → J) (B : Family I) : Family J :=
  fun j => SigmaFiber f B j

def transportFamily {I : Type u} {A : Family I} {i : I} :
    ∀ {j : I}, i = j → A i → A j
  | _, rfl => id

def sigmaToReindex {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (h : FamilyHom (sigmaFamily f B) A) : FamilyHom B (reindexFamily f A) :=
  fun i b => h (f i) ⟨i, b, rfl⟩

def reindexToSigma {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (k : FamilyHom B (reindexFamily f A)) : FamilyHom (sigmaFamily f B) A :=
  fun _ x => transportFamily x.equation (k x.index x.value)

theorem sigma_reindex_left_inv {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (h : FamilyHom (sigmaFamily f B) A) :
    reindexToSigma (sigmaToReindex h) = h := by
  funext j x
  rcases x with ⟨i, b, equality⟩
  cases equality
  rfl

theorem sigma_reindex_right_inv {I J : Type u} {f : I → J} {B : Family I} {A : Family J}
    (k : FamilyHom B (reindexFamily f A)) :
    sigmaToReindex (reindexToSigma k) = k := by
  funext i b
  simp [sigmaToReindex, reindexToSigma, transportFamily]

def sigmaReindexEquiv {I J : Type u} (f : I → J) (B : Family I) (A : Family J) :
    FamilyHom (sigmaFamily f B) A ≃ FamilyHom B (reindexFamily f A) where
  toFun := sigmaToReindex
  invFun := reindexToSigma
  left_inv := sigma_reindex_left_inv
  right_inv := sigma_reindex_right_inv

/-!
この同値は

$$
\operatorname{Hom}_{\mathcal C/J}(\Sigma_fB,A)
\cong\operatorname{Hom}_{\mathcal C/I}(B,f^*A).
$$

を与えるので `Σ_f⊣f⁎` です。等式証明を要素に含めたのは、`f` が単射とも全射とも限らないからです。
`Σ_f B(j)` は単に一つの `B(i)` を選ぶ型ではなく、`j` へ写る全てのファイバーを依存和で集めます。

## 依存積は再添字付けの右随伴である

同じ `f:I→J` と `B:I→Type` に対し、`Π_f B(j)` は `f(i)=j` となる全ての `i` について `B(i)` の要素を
選ぶ族です。
-/

def piFamily {I J : Type u} (f : I → J) (B : Family I) : Family J :=
  fun j => ∀ i, f i = j → B i

def reindexToPi {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (h : FamilyHom (reindexFamily f A) B) : FamilyHom A (piFamily f B) :=
  fun _ a i equality => h i (transportFamily (A := A) equality.symm a)

def piToReindex {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (k : FamilyHom A (piFamily f B)) : FamilyHom (reindexFamily f A) B :=
  fun i a => k (f i) a i rfl

theorem pi_reindex_left_inv {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (h : FamilyHom (reindexFamily f A) B) :
    piToReindex (reindexToPi h) = h := by
  funext i a
  simp [piToReindex, reindexToPi, transportFamily]

theorem pi_reindex_right_inv {I J : Type u} {f : I → J} {A : Family J} {B : Family I}
    (k : FamilyHom A (piFamily f B)) :
    reindexToPi (piToReindex k) = k := by
  funext j a i equality
  cases equality
  simp [piToReindex, reindexToPi, transportFamily]

def reindexPiEquiv {I J : Type u} (f : I → J) (A : Family J) (B : Family I) :
    FamilyHom (reindexFamily f A) B ≃ FamilyHom A (piFamily f B) where
  toFun := reindexToPi
  invFun := piToReindex
  left_inv := pi_reindex_left_inv
  right_inv := pi_reindex_right_inv

/-!
したがって

$$
\operatorname{Hom}_{\mathcal C/I}(f^*A,B)
\cong\operatorname{Hom}_{\mathcal C/J}(A,\Pi_fB).
$$

すなわち `f⁎⊣Π_f` です。`Π_f B(j)` は逆像ファイバー上の積です。逆像が空なら空積として一元型になり、
複数の添字が `j` へ写れば各添字に対する成分を全て要求します。存在を集める `Σ_f` と、全ての選択を要求する
`Π_f` の量化方向がここに現れます。

## 三随伴を一列に並べる

二つの同値を合わせると

$$
\Sigma_f\dashv f^*\dashv\Pi_f.
$$

を得ます。左随伴 `Σ_f` は生成された要素をまとめ、中央の `f⁎` は添字を置換し、右随伴 `Π_f` は逆像上の
整合する選択を集めます。同じ `f⁎` を共有していることが、依存和と依存積を別々の型構成子として暗記するより
重要です。

## 一般圏では射が指数化可能であることを問う

圏 `C` に選ばれた引戻しがあり、`f:I⟶J` とします。後合成 `Σ_f=Over.map f` の右随伴が引戻し `f⁎` でした。
さらに `f⁎` が右随伴を持つとき、`f` を指数化可能な射と呼び、その右随伴を `Π_f` と呼びます。

$$
\mathsf{Over.map}(f)
\dashv\mathsf{pullback}(f)
\dashv\mathsf{pushforward}(f).
$$

mathlibの `ExponentiableMorphism f` は、選ばれた `pullback f` と右随伴 `pushforward f` を保持します。
-/

open _root_.CategoryTheory
open ChosenPullbacksAlong
open ExponentiableMorphism

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable {I J : C} (f : I ⟶ J)
variable [ChosenPullbacksAlong f] [ExponentiableMorphism f]

def dependentProductFunctor : Over I ⥤ Over J := pushforward f

example : Over.map f ⊣ pullback f := mapPullbackAdj f

example : pullback f ⊣ dependentProductFunctor f := pullbackPushforwardAdj f

/-!
`pushforward` というAPI名は基底方向 `I→J` へ進むことを表しますが、随伴上の役割は依存積 `Π_f` です。
同じ向きの `Over.map f` も存在するため、名前の向きだけで両者を同一視してはいけません。前者は `f⁎` の右随伴、
後者は `f⁎` の左随伴です。

## 依存カリー化と評価

通常の指数対象では `Hom(A×X,B)≃Hom(X,B^A)` がカリー化を与えました。指数化可能な射では

$$
\operatorname{Hom}_{\mathcal C/I}(f^*A,X)
\cong\operatorname{Hom}_{\mathcal C/J}(A,\Pi_fX).
$$

が依存カリー化です。mathlibは順方向を `pushforwardCurry`、逆方向を `pushforwardUncurry` として公開します。
-/

variable {A : Over J} {X : Over I}

def dependentCurry (u : (pullback f).obj A ⟶ X) :
    A ⟶ (dependentProductFunctor f).obj X :=
  pushforwardCurry u

def dependentUncurry (v : A ⟶ (dependentProductFunctor f).obj X) :
    (pullback f).obj A ⟶ X :=
  pushforwardUncurry v

theorem dependent_uncurry_curry (u : (pullback f).obj A ⟶ X) :
    dependentUncurry f (dependentCurry f u) = u :=
  pushforward_uncurry_curry u

theorem dependent_curry_uncurry (v : A ⟶ (dependentProductFunctor f).obj X) :
    dependentCurry f (dependentUncurry f v) = v :=
  pushforward_curry_uncurry v

/-!
随伴の余単位 `ev : Π_f X` を `f` に沿って引き戻して `X` へ評価する射であり、単位 `coev` は依存関数を
作る前のデータを依存積へ送ります。二つの三角恒等式 `ev_coev` と `coev_ev` が、上のカリー化と逆カリー化の
逆法則を保証します。

## 「局所」の意味

デカルト閉圏が `C` 自身の積と指数対象を要求するのに対し、局所デカルト閉圏は全ての `I:C` について
スライス `C/I` がデカルト閉であることを要求します。「局所」は位相的な近傍を意味せず、各基底対象の上で
閉構造を見ることを指します。

有限極限を持つ圏では、全ての射が指数化可能であることと全スライスのデカルト閉性を対応させられます。
終対象 `1` 上のスライス `C/1` は `C` と同値なので、局所デカルト閉性から通常のデカルト閉性も従います。
逆は一般に成り立ちません。`C` に指数対象があるだけでは、全ての文脈 `I` の上で依存積を作れるとは限りません。

## 現行mathlibが形式化する境界

現行mathlibは、圏全体に対する単一の `LocallyCartesianClosed` 型クラスではなく、射ごとの
`ChosenPullbacksAlong f` と `ExponentiableMorphism f` を中心に構成します。この表現は局所デカルト閉圏の
定義を変更するものではありません。どの射についてどの引戻しと右随伴を選んだかを、Leanのインスタンスとして
明示する実装上の分解です。

また `pushforwardComp` は、合成射に沿う依存積と二つの依存積の合成を自然同型で比較します。右随伴の一意性から
得る同型であり、定義的等号ではありません。依存型の代入則を厳密な計算則として要求するモデルでは、この
coherenceをどう厳密化するかが別の設計問題になります。

## 要点

* 局所デカルト閉圏とは、全てのスライス圏がデカルト閉である圏である。
* 型族では再添字付け `f⁎` の左随伴が依存和 `Σ_f`、右随伴が依存積 `Π_f` である。
* 一般圏では `Σ_f=Over.map f ⊣ pullback f=f⁎ ⊣ pushforward f=Π_f` という三随伴になる。
* 射 `f` が指数化可能であるとは、`f` に沿う引戻し関手が右随伴を持つことである。
* 依存カリー化は異なる二つのスライス圏のhom集合を結ぶ随伴同値である。
* 通常のデカルト閉性だけでは、全スライスで必要な依存積の存在は保証されない。

## 研究史と文献案内

Seely [SEE84] は局所デカルト閉圏とMartin-Löf型理論の関係を体系的に扱った一次論文です。同論文の対応を読む際は、
後続研究で明確化された厳密な等価と双圏同値、および代入の厳密性に関する条件を区別する必要があります。
ファイブレーションを基盤に依存和・依存積・論理を統一する現代的な定式化には Jacobs [JAC99] を参照してください。

W型と依存多項式関手への展開は Gambino–Hyland [GH04] が扱います。本章は各射の依存積随伴を形式化しますが、
局所デカルト閉圏におけるW型の存在や多項式関手の始代数を自動的に導きません。Lean宣言は [MATHLIB] の現行API、
とくに `ExponentiableMorphism.lean` に従います。

## 問題

### 二つの型族随伴の自然性を証明する

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

### 空ファイバーと多元ファイバーで依存積を計算する

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

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

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

### 合成に沿う依存積の比較同型を追跡する

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

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

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

end FormalLab.Bridges.LocallyCartesianClosedCategories