import FormalLab.CategoryTheory.InitialAlgebras
import FormalLab.Mathematics.NaturalNumberInduction
import FormalLab.TypeTheory.GeneralInductiveFamilies

/-!
# 第66章：帰納型・帰納法・始代数——三つの生成原理を接続する

自然数は `0` と後者から作られる帰納型です。関数を定義するときには基底値と一段の演算を与える再帰原理を
使い、全ての自然数について命題を証明するときには基底証明と帰納段階を与える帰納原理を使います。一方、
圏論では自然数を自己関手 `F(X)=1+X` の始代数として特徴づけ、任意の `F`-代数への一意な準同型を得ます。

三者は密接ですが、同じ定義ではありません。帰納型の除去原理は結果が入力に依存でき、始代数から直接得る
foldの終域は一つの固定対象です。始代数の構造射が同型であることも、帰納法より弱い不動点情報にすぎません。
本章では自然数という一つの対象について、構成子、非依存再帰、依存帰納、始代数の普遍性を順に対応させます。
さらに述語を全空間へ束ねることで、`Type` において非依存foldから依存帰納を回収する仕組みを構成します。

## 一層の形は `1+X` で記述できる

自然数の構成子を一段だけ観察すると、零には再帰的な引数がなく、後者には自然数が一つ入ります。従って一層の
形は余積 `1+X` です。

$$
\frac{\mathsf{zero}:1\to\mathbb N
\qquad\mathsf{succ}:\mathbb N\to\mathbb N}
{[\mathsf{zero},\mathsf{succ}]:1+\mathbb N\to\mathbb N}.
$$

この余対射は自己関手 `F(X)=1+X` の代数構造です。
-/

namespace FormalLab.Bridges.InductionAndInitialAlgebras

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open _root_.CategoryTheory.Limits
open FormalLab.CategoryFoundations.InitialAlgebras

universe u

example : Type u ⥤ Type u := onePlusFunctor

example : Unit ⊕ Nat → Nat := natStructure

example : Algebra onePlusFunctor := natAlgebra

example : natStructure (.inl ()) = 0 := rfl
example (n : Nat) : natStructure (.inr n) = n + 1 := rfl

/-!
`Unit⊕Nat` と `Nat` が同じ濃度であることだけでは、零と後者による生成を表しません。重要なのは、どの同型でも
よいのではなく構成子をまとめた特定の構造射を持つことです。それでも代数であるだけでは、到達不能な要素や
構造方程式を保つ複数の関数を排除できません。次に始性が必要になります。

## 非依存再帰は代数準同型として表せる

型 `A`、基底値 `z:A`、一段の演算 `s:A→A` を固定します。これらは `1+A→A` という代数構造にまとまります。
-/

def algebraOfSteps (A : Type u) (z : A) (s : A → A) : Algebra onePlusFunctor where
  a := A
  str := ↾fun
    | .inl _ => z
    | .inr a => s a

def recFromInitial (z : A) (s : A → A) : Nat → A :=
  fold (algebraOfSteps A z s)

example (z : A) (s : A → A) : recFromInitial z s 0 = z := rfl

example (z : A) (s : A → A) (n : Nat) :
    recFromInitial z s (n + 1) = s (recFromInitial z s n) := rfl

/-!
この二式はLeanの `Nat.rec` の計算規則と同じ形です。圏論側では、同じ関数が代数準同型

$$
(\mathbb N,[\mathsf{zero},\mathsf{succ}])
\longrightarrow(A,[z,s]).
$$

として得られます。準同型条件を余積の左右で評価すると、基底方程式と再帰方程式になります。
-/

example (A : Algebra onePlusFunctor) : natAlgebra ⟶ A := foldHom A

example (A : Algebra onePlusFunctor) :
    onePlusFunctor.map (foldHom A).f ≫ A.str =
      natAlgebra.str ≫ (foldHom A).f :=
  (foldHom A).h

/-!
## 始性は再帰方程式を満たす関数を一意にする

`natAlgebra` が始対象であるとは、全ての `1+X`-代数へ代数準同型がただ一つ存在することです。
-/

example : IsInitial natAlgebra := natIsInitial

example (A : Algebra onePlusFunctor) (f : natAlgebra ⟶ A) :
    f = foldHom A :=
  fold_unique A f

/-!
再帰関数を一つ構成できるだけでは始性になりません。同じ基底方程式と再帰方程式を満たす別の関数が存在しない
ことまで必要です。自然数の場合、この一意性は自然数帰納法で証明されます。従って既存の第55章のLean証明は、
帰納原理を使って始代数性を確立する向きになっています。

$$
\begin{aligned}
\text{帰納型の再帰子}&\Longrightarrow\text{foldの存在},\\
\text{帰納法}&\Longrightarrow\text{foldの一意性},\\
\text{存在と一意性}&\Longrightarrow\text{始代数性}.
\end{aligned}
$$

これは始代数から帰納法を導く逆向きの議論とは別です。循環を避けるには、どちらを既知としてどちらを構成して
いるかを明示しなければなりません。

## 帰納法は終域が入力に依存する

非依存再帰では結果型 `A` は全ての入力で同じです。帰納法では述語または型族 `P:Nat→Type` を取り、結果が
`P(n)` に属します。

$$
\frac{p_0:P(0)
\qquad p_s:\prod_{n:\mathbb N}P(n)\to P(n+1)}
{\mathsf{ind}_P:\prod_{n:\mathbb N}P(n)}.
$$

固定対象 `A` へのfoldだけを見ると、この依存は型に現れません。始代数と依存帰納の間には、型族を一つの対象へ
束ね、元の自然数への射影を追跡する構成が必要です。

## 型族の全空間は依存するファイバーを一対象へ束ねる

型族 `P:Nat→Type` の全空間を従属和 `Σn,P(n)` とします。基底証明 `p₀` と帰納段階 `pₛ` から、この全空間に
`1+X`-代数構造を入れられます。
-/

def totalAlgebra (P : Nat → Type u) (p₀ : P 0)
    (pₛ : ∀ n, P n → P (n + 1)) : Algebra onePlusFunctor where
  a := Sigma P
  str := ↾fun
    | .inl _ => ⟨0, p₀⟩
    | .inr ⟨n, proof⟩ => ⟨n + 1, pₛ n proof⟩

def totalFold (P : Nat → Type u) (p₀ : P 0)
    (pₛ : ∀ n, P n → P (n + 1)) : Nat → Sigma P :=
  fold (totalAlgebra P p₀ pₛ)

example (P : Nat → Type u) (p₀ : P 0) (pₛ : ∀ n, P n → P (n + 1)) :
    totalFold P p₀ pₛ 0 = ⟨0, p₀⟩ := rfl

example (P : Nat → Type u) (p₀ : P 0) (pₛ : ∀ n, P n → P (n + 1)) (n : Nat) :
    totalFold P p₀ pₛ (n + 1) =
      ⟨(totalFold P p₀ pₛ n).1 + 1, pₛ _ (totalFold P p₀ pₛ n).2⟩ := rfl

/-!
foldの値は対 `⟨k,proof:P(k)⟩` です。欲しいのは入力 `n` と第一成分 `k` が等しいことです。これはfoldの
計算規則に沿う帰納法で示せます。
-/

theorem totalFold_fst (P : Nat → Type u) (p₀ : P 0)
    (pₛ : ∀ n, P n → P (n + 1)) (n : Nat) :
    (totalFold P p₀ pₛ n).1 = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      change (totalFold P p₀ pₛ n).1 + 1 = n + 1
      exact congrArg (fun k => k + 1) ih

def inductionFromInitial (P : Nat → Type u) (p₀ : P 0)
    (pₛ : ∀ n, P n → P (n + 1)) (n : Nat) : P n :=
  cast (congrArg P (totalFold_fst P p₀ pₛ n)) (totalFold P p₀ pₛ n).2

example (P : Nat → Type u) (p₀ : P 0)
    (pₛ : ∀ n, P n → P (n + 1)) : ∀ n, P n :=
  inductionFromInitial P p₀ pₛ

/-!
`totalFold` は非依存foldですが、終域 `Σn,P(n)` の内部に添字を保存しています。第一成分が入力と一致する証明で
第二成分を輸送すると `P(n)` の値を得ます。ここで必要なのは始代数だけではありません。型族の従属和、射影、
等式に沿う輸送が使える `Type` の構造も必要です。一般の圏で同じ議論を行うには、ファイブレーション、
comprehension、または関手の述語持ち上げに相当する追加構造を指定します。

## 証明が命題に値が型に属する場合

`P:Nat→Prop` なら `inductionFromInitial` の値は各命題の証明です。Leanでは証明無関連性により、同じ `P(n)` の
二証明は区別されません。一方 `P:Nat→Type` の場合は、帰納原理が計算データを返せます。帰納法を命題だけに
限定すると、依存除去原理の計算的な強さを見落とします。

## 厳密正値性は一層関手を作る前段階にある

`F(X)=1+X` では再帰変数 `X` は余積の正の位置に現れます。このため射 `f:X→Y` を `id+f:1+X→1+Y` へ写せて、
自己関手を構成できます。一般の帰納型でも、再帰出現が厳密に正であることは一層の形を関手として作用させる
ための基本条件です。

ただしLeanの厳密正値性検査を通ることから、対応する始代数が任意の圏で存在すると結論してはいけません。
正値性は構文的な帰納宣言と停止する除去子を受理する条件です。圏論側の始代数の存在は、対象となる圏と関手の
連続性、アクセス可能性、必要な余極限など別の仮定に依存します。

## 不動点同型は生成原理の一部しか持たない

Lambekの補題から始代数の構造射 `F(μF)→μF` は同型になります。しかし同型 `F(X)≅X` だけでは、任意の代数への
foldも、その一意性も、依存帰納も得られません。

$$
\text{始代数性}
\Longrightarrow\text{foldの存在と一意性}
\Longrightarrow\text{構造射の同型}.
$$

矢印を逆向きに読むことはできません。帰納型を単に再帰方程式の解と説明すると、生成されない余分な要素を排除する
最小性と、関数を定める普遍性が失われます。

## 四つの原理の対応表

| 観点 | 与えるもの | 結果 | 固有の条件 |
|---|---|---|---|
| 帰納型の形成・導入 | 型と構成子 | 値を作る | 厳密正値性など |
| 非依存再帰 | 基底値と一段演算 | `Nat→A` | 構成子ごとの計算規則 |
| 依存帰納 | 基底証明と依存段階 | `∀n,P(n)` | motiveと輸送 |
| 始代数 | 任意の代数 | 一意な準同型 | 代数圏での始性 |

この表は四者を分断するためではなく、正確に接続するためのものです。自然数では一つの帰納宣言から再帰子と
帰納原理が生成され、帰納法でfoldの一意性を証明して始代数を得られます。逆に `Type` の従属和を使えば、始代数の
foldから依存帰納を再構成できます。対応の各向きが使う追加構造を記録することが重要です。

## 要点

* 自然数の構造射 `[zero,succ]:1+Nat→Nat` は構成子を一つの `1+X`-代数へまとめる。
* 始代数から得る一意な代数準同型は、固定した終域への非依存再帰である。
* 自然数ではfoldの存在を再帰子で、foldの一意性を帰納法で証明して始代数性を得られる。
* 依存帰納は型族の全空間へfoldし、射影が入力添字を保存することを示して第二成分を輸送すると回収できる。
* この逆構成は従属和と等式輸送を使い、任意の圏の始代数だけからは自動的に従わない。
* 厳密正値性、不動点同型、始代数性、依存帰納は異なる条件と結論を持つ。

## 研究史と文献案内

Dedekind [DED88] は単純無限系と再帰的定義、Peano [PEA89] は算術公理の中の帰納原理を与えました。両者を現代の
帰納型やLeanの除去子と同一視せず、基礎体系と表現の差を区別します。Lambek [LAM68] は圏論的な不動点定理を
研究しました。Goguen–Thatcher–Wagner–Wright [GTWW77] は、始代数意味論と連続代数をプログラム意味論へ
展開しました。
Martin-Löf型理論の自然数と依存除去は [ML84]、型理論と圏論的論理の接続は [LS86] を参照してください。
本章の具体的な `Type` 上の構成は、これらの文献の単一定理をそのまま転記したものではなく、[MATHLIB] とLeanの
現行APIで対応の仮定を可視化したものです。

## 問題

### 再帰子から始代数性を再構成する

任意の `1+X`-代数 `A` に対し、自然数再帰子から `fold_A` を定義してください。基底・後者の計算規則から
`fold_A` が代数準同型であることを示します。次に任意の準同型 `f` が同じ二方程式を満たすことを構造射の
可換条件から取り出し、自然数帰納法で `f=fold_A` を証明してください。存在と一意性がどの原理を使ったかを
別々に記録できれば完了です。

### 全空間による依存帰納を計算する

`P(n)` を「長さが `n` のリスト」の型とし、空リストと先頭への要素追加を帰納段階に選んでください。
`totalAlgebra` と `totalFold` を計算し、第一成分が入力した自然数、第二成分がその長さのリストになることを
確認します。`cast` がどの等式に沿ってどのファイバー間を移送するかを型まで書き、非依存foldから依存する値が
得られる仕組みを説明してください。

### 不動点・代数・始代数を反例で分ける

恒等関手 `Id` では全対象が不動点同型 `X≅Id(X)` を持ちます。構造射を自己写像として選んだ `Id`-代数を調べ、
全てが始代数ではないことを示してください。次に構造射が同型という条件を加えても一意な準同型が得られない例を
探します。どの反例が存在、一意性、依存帰納のどれを失うかを分類できれば完了です。

### 一般圏で不足する構造を特定する

任意の圏 `C` に始 `F`-代数があると仮定し、`Type` で使った `Σn,P(n)`、第一射影、等式輸送に対応する構造を
列挙してください。述語をスライス圏またはファイブレーションの対象として表し、始代数から依存帰納を得るには
`F` の持ち上げが必要になる理由を説明します。「始代数がある」だけでは書けない式を正確に一つ示せれば完了です。
-/

end FormalLab.Bridges.InductionAndInitialAlgebras