import Mathlib.CategoryTheory.Monoidal.Closed.Types
import FormalLab.CategoryTheory.Products
import FormalLab.CategoryTheory.RepresentableFunctors

/-!
# 第70章：デカルト閉圏——積・指数対象・カリー化

積対象 `A×X` は二つの値を同時に保持します。しかし、そこから関数型 `A→B` が圏の内部に存在することは
従いません。関数型を対象として扱うには、二変数の射 `A×X→B` を一変数の射 `X→B^A` へ一意に移す
普遍性が必要です。この `B^A` を指数対象と呼びます。

有限積を持ち、全ての対象 `A,B` に指数対象 `B^A` を持つ圏がデカルト閉圏です。本章では型と関数の圏で
評価とカリー化を計算し、β則とη則が二つの逆法則であることを証明します。その後、一般の圏で指数対象を
hom型の自然な同値、随伴、表現可能性という三つの同値な形式へ移します。

第43章の積は、共通始域からの二本の射を一本へ束ねました。指数対象は、積を始域に持つ一本の射を内部homへの
一本の射へ束ねます。どちらも内部表現ではなく、全ての試験対象 `X` に対する一意な媒介射で特徴づけられます。

## 型の圏では関数型が指数対象になる

型 `A,X,B` を固定します。関数 `f:A×X→B` の第一引数を後から受け取る形へ移すと、

$$
\mathsf{curry}(f):X\longrightarrow(A\to B),
\qquad
\mathsf{curry}(f)(x)(a)=f(a,x).
$$

を得ます。逆に `g:X→(A→B)` を対へ適用すれば `A×X→B` に戻せます。
-/

namespace FormalLab.Bridges.CartesianClosedCategories

open FormalLab.CategoryTheory.Products

universe u v w

def typeCurry {A : Type u} {X : Type v} {B : Type w}
    (f : A × X → B) : X → A → B :=
  fun x a => f (a, x)

def typeUncurry {A : Type u} {X : Type v} {B : Type w}
    (g : X → A → B) : A × X → B :=
  fun pair => g pair.2 pair.1

theorem typeUncurry_typeCurry {A : Type u} {X : Type v} {B : Type w}
    (f : A × X → B) : typeUncurry (typeCurry f) = f := by
  funext pair
  cases pair
  rfl

theorem typeCurry_typeUncurry {A : Type u} {X : Type v} {B : Type w}
    (g : X → A → B) : typeCurry (typeUncurry g) = g := by
  funext x a
  rfl

def typeExponentialEquiv {A : Type u} {X : Type v} {B : Type w} :
    FunctionEquiv (A × X → B) (X → A → B) where
  toFun := typeCurry
  invFun := typeUncurry
  leftInverse := typeUncurry_typeCurry
  rightInverse := typeCurry_typeUncurry

/-!
第一の逆法則は、カリー化してから対へ適用すると元の関数へ戻るβ則です。第二の逆法則は、関数を全引数へ
適用してから再び抽象すると元の関数へ戻るη則です。βだけではカリー化が全射とは限らず、ηだけでは単射とは
限りません。二つを合わせてhom型の全単射になります。

## 評価射が全ての適用を代表する

指数対象には評価射

$$
\mathsf{ev}:A\times(A\to B)\longrightarrow B,
\qquad
\mathsf{ev}(a,g)=g(a).
$$

があります。任意の `f:A×X→B` は、`typeCurry f:X→A→B` を第二成分へ入れ、評価することで一意に復元されます。
-/

def typeEvaluation {A : Type u} {B : Type v} : A × (A → B) → B :=
  fun pair => pair.2 pair.1

theorem typeUncurry_id_eq_evaluation {A : Type u} {B : Type v} :
    typeUncurry (id : (A → B) → (A → B)) = typeEvaluation := rfl

theorem type_beta {A : Type u} {X : Type v} {B : Type w}
    (f : A × X → B) (a : A) (x : X) :
    typeEvaluation (a, typeCurry f x) = f (a, x) := rfl

theorem type_eta {A : Type u} {B : Type v} (g : A → B) :
    typeCurry typeEvaluation g = g := rfl

/-!
評価射を単に一つ選ぶだけでは指数対象になりません。全ての `X` と `f:A×X→B` に対し、評価を経由する
`X→A→B` が存在し、その条件を満たす射が一意であることが普遍性です。`typeExponentialEquiv` の二逆法則が
存在と一意性を同時に記録します。

## 一般の圏では指数対象をhom同値で定義する

有限積を持つ圏 `C` で、対象 `A,B` の指数対象 `B^A` は全ての `X` について自然な同値

$$
\operatorname{Hom}_{\mathcal C}(A\times X,B)
\cong
\operatorname{Hom}_{\mathcal C}(X,B^A).
$$

を与える対象です。左辺で `A` と `X` の順を採用するのは、mathlibの左テンソル関手 `A⊗-` に合わせるためです。
デカルト積の対称性を使えば `X×A` の規約へ移れます。
-/

open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.MonoidalClosed

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable [CartesianMonoidalCategory C] [MonoidalClosed C]
variable {A X B : C}

example (f : A ⊗ X ⟶ B) : X ⟶ A ⟶[C] B := curry f

example (g : X ⟶ A ⟶[C] B) : A ⊗ X ⟶ B := uncurry g

example : (A ⊗ X ⟶ B) ≃ (X ⟶ A ⟶[C] B) :=
  (ihom.adjunction A).homEquiv X B

example (f : A ⊗ X ⟶ B) : uncurry (curry f) = f :=
  uncurry_curry f

example (g : X ⟶ A ⟶[C] B) : curry (uncurry g) = g :=
  curry_uncurry g

/-!
Leanの `A ⟶[C] B` は対象 `C` の内部homであり、外部の射型 `A ⟶ B` とは異なります。外部homはLeanの
型としてメタ理論側にあり、内部homは圏 `C` の対象です。豊穣圏のhom対象とも関連しますが、本章では
デカルト積との随伴によって選ばれた内部homを扱います。

## 評価は随伴の余単位である

対象 `A` との積を取る関手 `A×-` の右随伴が内部hom関手 `A⇒-` です。
-/

example : tensorLeft A ⊣ ihom A := ihom.adjunction A

example : A ⊗ (A ⟶[C] B) ⟶ B := (ihom.ev A).app B

example (f : A ⊗ X ⟶ B) :
    A ◁ curry f ≫ (ihom.ev A).app B = f :=
  whiskerLeft_curry_ihom_ev_app A B f

/-!
最後の等式は一般圏におけるβ則です。カリー化した射を `A` と組にし、評価射へ合成すると元の射へ戻ります。
η則は `curry_uncurry` です。随伴の三角恒等式がβ・ηの統一的な根拠になります。

「各 `A,B` にたまたま対象 `B^A` がある」だけでは不十分です。`B` の射に沿って内部homが関手的に動き、
hom同値が `X` と `B` の双方について自然である必要があります。随伴として束ねると、この自然性が構造の一部に
なります。

## デカルト閉性は有限積と閉性を組み合わせる

終対象と二項積があれば、空積と有限個の積を構成できます。これが有限積です。各 `A` について `A×-` が
右随伴を持てば、全ての指数対象が関手的に選ばれます。従ってデカルト閉圏のデータは

$$
\text{有限積}
\quad+\quad
\bigl(A\times-\dashv A\Rightarrow-\bigr)
\quad\text{for every }A.
$$

と整理できます。

mathlibの現行APIでは、有限積の選択を `CartesianMonoidalCategory C`、全対象の閉性を `MonoidalClosed C` で
表します。以前の独立した `CartesianClosed` 名は非推奨です。これはライブラリ上の表現変更であり、デカルト閉圏の
数学的定義がモノイダル閉圏一般と同じになったという意味ではありません。テンソルがデカルト積であるという
前半の構造が不可欠です。
-/

example : CartesianMonoidalCategory (Type u) := inferInstance
example : MonoidalClosed (Type u) := inferInstance

example (A X B : Type u) :
    (A ⊗ X ⟶ B) ≃ (X ⟶ A ⟶[Type u] B) :=
  (ihom.adjunction A).homEquiv X B

/-!
`Type u` ではテンソル積が直積、テンソル単位が `Unit` であり、内部homは関数型と同じ指数普遍性を表します。
mathlibが選ぶ右随伴の対象を関数型と定義的等号で同一視せず、上のhom同値を境界にします。この具体例は
デカルト閉圏の一般定義を実現しますが、任意のデカルト閉圏の対象を型の要素として扱えることは意味しません。

## 指数対象は関手を表現する

`A,B` を固定し、試験対象 `X` を

$$
X\longmapsto\operatorname{Hom}_{\mathcal C}(A\times X,B).
$$

へ送る反変関手を考えます。指数対象 `B^A` は、この関手を `Hom_C(-,B^A)` として表現します。従って
次の三形式は同じ中心構造を異なる方向から述べます。

| 形式 | 中心データ | 一意性の現れ方 |
|---|---|---|
| 指数対象 | `B^A` と評価射 | 評価を経由する射が一意 |
| hom同値 | `Hom(A×X,B)≃Hom(X,B^A)` | 二つの逆法則 |
| 随伴 | `A×- ⊣ A⇒-` | 単位・余単位の三角恒等式 |

表現可能性は「試験対象ごとの同じ要素数」ではなく、前合成に関して自然なhom同値を要求します。ここでも自然性を
落とすと、指数対象の関手的な振舞いを回収できません。

## 閉性だけではデカルト性を含まない

モノイダル閉圏では `A⊗-` が右随伴を持ちますが、テンソル積が圏論的積であるとは限りません。デカルト積には
射影、対化、対角射、終対象への一意射があり、変数の複製と破棄を表せます。一般のテンソル積はこれらを持たない
場合があります。この差が後の線形論理と資源感応型理論の入口になります。

## 要点

* 指数対象 `B^A` は、全ての `X` に対する自然なhom同値 `Hom(A×X,B)≃Hom(X,B^A)` で特徴づけられる。
* 評価射とカリー化のβ・η則は、hom同値の二つの逆法則である。
* 指数対象は関手 `X↦Hom(A×X,B)` の表現対象である。
* `A×- ⊣ A⇒-` と書くと、カリー化の自然性と評価射を一つの随伴へ束ねられる。
* デカルト閉圏は有限積と全対象の閉性を持ち、`Type` では積と関数型がその具体例になる。
* モノイダル閉性だけではテンソルがデカルト積だとは限らず、複製・破棄の構造は別に必要である。

## 研究史と文献案内

Eilenberg–Kelly [EK66] は閉圏と内部homを体系化しました。現在のデカルト閉圏の標準定義を同論文の一節へ単純に
還元せず、有限積、指数対象、随伴の現代的整理には [MAC98] を参照してください。デカルト閉圏と単純型付き
ラムダ計算・高階論理の対応は Lambek–Scott [LS86] が標準文献です。式と型の対応の歴史については
Curry [CUR34] とHoward [HOW80] を参照し、圏論的意味論の成立史と同一視しません。
Leanの `CartesianMonoidalCategory`, `MonoidalClosed`, `ihom`, `curry`, `uncurry` は [MATHLIB] の現行APIに
従います。非推奨名の説明は現在のライブラリ境界であり、過去の版へ遡及して適用しません。

## 問題

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

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

### β則・η則・三角恒等式を対応させる

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

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

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

### デカルト閉圏とモノイダル閉圏の差を射で検査する

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

end FormalLab.Bridges.CartesianClosedCategories