import FormalLab.Bridges.InductionAndInitialAlgebras
import FormalLab.TypeTheory.WTypes

/-!
# 第67章：W型・多項式関手・自由代数——形と位置から帰納構造を作る

自然数の一層は `1+X` でした。リストなら `1+A×X`、二分木なら `1+X²` です。これらの式は、構成子を
選ぶことと、その構成子が要求する再帰的な引数を埋めることに分解できます。形の型を `A`、形 `a` の
位置の型を `B(a)` とすれば、一層全体は

$$
P(X)=\sum_{a:A}X^{B(a)}
=\sum_{a:A}(B(a)\to X).
$$

です。この形の自己関手を多項式関手と呼びます。本章では第37章で定義したW型をこの関手の始代数として
構成します。次に変数を葉として加えた木を作り、それが指定した生成元上の自由代数になることを証明します。

不動点、始代数、自由代数は順に要求が強くなるという単純な序列ではありません。始代数は生成元を持たない
普遍対象であり、自由代数は指定した型から代数へ入る写像を普遍化します。自由代数は、変数を定数項として
加えた別の自己関手の始代数として表せます。この二つの見方を同じLean定義で照合します。

## 多項式は形の和と位置の積からできる

`P(X)=Σa.B(a)→X` の要素は、形 `a` と、各位置へ `X` の要素を置く関数の対です。通常の一変数多項式
`Σₙ Aₙ×Xⁿ` では次数 `n` が位置数を表します。依存する位置型 `B(a)` を使う表現は、形ごとに異なる
分岐を一つの式へまとめます。
-/

namespace FormalLab.Bridges.PolynomialFunctorsAndWTypes

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open _root_.CategoryTheory.Limits
open FormalLab.TypeTheory.WTypes

universe u

def polynomialFunctor (A : Type u) (B : A → Type u) : Type u ⥤ Type u where
  obj X := Layer A B X
  map f := ↾fun layer => ⟨layer.1, fun position => f (layer.2 position)⟩
  map_id X := by
    ext layer
    cases layer
    rfl
  map_comp f g := by
    ext layer
    cases layer
    rfl

example (A : Type u) (B : A → Type u) (X : Type u) :
    (polynomialFunctor A B).obj X = Layer A B X := rfl

example (A : Type u) (B : A → Type u) {X Y : Type u} (f : X → Y)
    (shape : A) (branches : B shape → X) :
    (polynomialFunctor A B).map (↾f) ⟨shape, branches⟩ =
      ⟨shape, fun position => f (branches position)⟩ := rfl

/-!
関手の射作用は形を変えず、各位置の値だけを `f` で写します。`map_id` と `map_comp` は、位置ごとの
恒等写像と関数合成の法則です。式が対象について多項式らしく見えるだけでは関手になりません。射への作用と
二つの関手法則までが必要です。

## W型の構成子は多項式代数の構造射である

W型 `W A B` の構成子 `sup` は、一層の形 `P(W A B)` を一つの木へ畳みます。従って構造射

$$
\mathsf{sup}:P(W_{a:A}B(a))\longrightarrow W_{a:A}B(a)
$$

を持つ `P`-代数になります。
-/

def wAlgebra (A : Type u) (B : A → Type u) : Algebra (polynomialFunctor A B) where
  a := W A B
  str := ↾roll

def wFold {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) : W A B → C.a :=
  fold fun shape results => C.str ⟨shape, results⟩

theorem wFold_sup {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) (shape : A) (branches : B shape → W A B) :
    wFold C (.sup shape branches) =
      C.str ⟨shape, fun position => wFold C (branches position)⟩ := rfl

def wFoldHom {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) : wAlgebra A B ⟶ C where
  f := ↾wFold C
  h := by
    ext layer
    cases layer
    rfl

/-!
準同型条件はfoldの計算規則を可換正方形として書いたものです。各子を先にfoldしてから `C` の構造射で
一層を解釈する経路と、先にW木を一節点へ畳んでから全体をfoldする経路が一致します。

## W帰納法がfoldの一意性を与える

始性にはfoldの存在だけでなく一意性が必要です。任意の代数準同型 `f` は構造射を保存するので、根における
値は子における値から決まります。全ての子で `f` とfoldが一致すると仮定し、W帰納法で木全体の一致を示します。
-/

theorem wFold_unique {A : Type u} {B : A → Type u}
    (C : Algebra (polynomialFunctor A B)) (f : wAlgebra A B ⟶ C) :
    f = wFoldHom C := by
  apply Algebra.ext
  ext tree
  induction tree with
  | sup shape branches ih =>
      have h := types_congr_hom f.h ⟨shape, branches⟩
      change C.str ⟨shape, fun position => f.f (branches position)⟩ =
        f.f (.sup shape branches) at h
      change f.f (.sup shape branches) =
        C.str ⟨shape, fun position => wFold C (branches position)⟩
      rw [← h]
      congr 2
      funext position
      exact ih position

def wIsInitial (A : Type u) (B : A → Type u) : IsInitial (wAlgebra A B) :=
  IsInitial.ofUniqueHom (fun C => wFoldHom C) (fun C f => wFold_unique C f)

example (A : Type u) (B : A → Type u) : IsIso (wAlgebra A B).str :=
  Algebra.Initial.str_isIso (wIsInitial A B)

/-!
これで第37章では保留した主張が完成しました。`roll` と `unroll` の逆法則はW型が `P` の不動点であることを
示します。`wIsInitial` はさらに、任意の `P`-代数への準同型が存在して一意であることを示します。証明の
追加部分はW帰納法による一意性です。

## 生成元を加えると自由代数になる

型 `X` の各要素を変数として持つ木を考えます。変数は子を持たない葉ですが、署名 `A,B` の定数構成子とは
区別します。
-/

inductive FreeTree (A : Type u) (B : A → Type u) (X : Type u) : Type u where
  | var : X → FreeTree A B X
  | sup : (shape : A) → (B shape → FreeTree A B X) → FreeTree A B X

def freeAlgebra (A : Type u) (B : A → Type u) (X : Type u) :
    Algebra (polynomialFunctor A B) where
  a := FreeTree A B X
  str := ↾fun layer => .sup layer.1 layer.2

def generator {A : Type u} {B : A → Type u} {X : Type u} :
    X → (freeAlgebra A B X).a :=
  FreeTree.var

def freeFold {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) : FreeTree A B X → C.a
  | .var x => η x
  | .sup shape branches =>
      C.str ⟨shape, fun position => freeFold C η (branches position)⟩

def freeFoldHom {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) :
    freeAlgebra A B X ⟶ C where
  f := ↾freeFold C η
  h := by
    ext layer
    cases layer
    rfl

theorem freeFoldHom_generator {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) (x : X) :
    (freeFoldHom C η).f (generator x) = η x := rfl

/-!
写像 `η:X→C` は生成元を代数 `C` でどう解釈するかを指定します。`freeFoldHom C η` は構成子を保つ代数準同型へ
一意に延長されます。ここでの一意性は、変数の場合には延長条件を、節点の場合には準同型条件と帰納仮定を
使います。
-/

theorem freeFoldHom_unique {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a)
    (f : freeAlgebra A B X ⟶ C)
    (hExt : ∀ x, f.f (generator x) = η x) :
    f = freeFoldHom C η := by
  apply Algebra.ext
  ext tree
  induction tree with
  | var x => exact hExt x
  | sup shape branches ih =>
      have h := types_congr_hom f.h ⟨shape, branches⟩
      change C.str ⟨shape, fun position => f.f (branches position)⟩ =
        f.f (.sup shape branches) at h
      change f.f (.sup shape branches) =
        C.str ⟨shape, fun position => freeFold C η (branches position)⟩
      rw [← h]
      congr 2
      funext position
      exact ih position

theorem freeUniversalProperty {A : Type u} {B : A → Type u} (X : Type u)
    (C : Algebra (polynomialFunctor A B)) (η : X → C.a) :
    ∃! f : freeAlgebra A B X ⟶ C, ∀ x, f.f (generator x) = η x := by
  refine ⟨freeFoldHom C η, freeFoldHom_generator C η, ?_⟩
  intro f hExt
  exact freeFoldHom_unique C η f hExt

/-!
これは「`FreeTree A B X` は `X` 上の自由 `P`-代数である」という主張です。自由とは要素を好きに選べるという
意味ではなく、生成元の写像 `η` が代数準同型へただ一通り延長されるという普遍性を指します。

## 自由代数は変数を加えた関手の始代数でもある

変数を零項構成子として一層へ組み込むと、自己関手

$$
Q_X(Y)=X+P(Y).
$$

を得ます。`FreeTree A B X` の二構成子は、ちょうど `Q_X` の構造射を与えます。
-/

def polynomialWithVariables (A : Type u) (B : A → Type u) (X : Type u) :
    Type u ⥤ Type u where
  obj Y := X ⊕ Layer A B Y
  map f := ↾fun
    | .inl x => .inl x
    | .inr layer => .inr ⟨layer.1, fun position => f (layer.2 position)⟩
  map_id Y := by
    ext value
    cases value with
    | inl x => rfl
    | inr layer => cases layer; rfl
  map_comp f g := by
    ext value
    cases value with
    | inl x => rfl
    | inr layer => cases layer; rfl

def freeTreeAsAlgebra (A : Type u) (B : A → Type u) (X : Type u) :
    Algebra (polynomialWithVariables A B X) where
  a := FreeTree A B X
  str := ↾fun
    | .inl x => .var x
    | .inr layer => .sup layer.1 layer.2

def freeTreeInitialFold {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialWithVariables A B X)) : FreeTree A B X → C.a
  | .var x => C.str (.inl x)
  | .sup shape branches =>
      C.str (.inr ⟨shape, fun position => freeTreeInitialFold C (branches position)⟩)

def freeTreeInitialHom {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialWithVariables A B X)) : freeTreeAsAlgebra A B X ⟶ C where
  f := ↾freeTreeInitialFold C
  h := by
    ext value
    cases value with
    | inl x => rfl
    | inr layer => cases layer; rfl

theorem freeTreeInitialHom_unique {A : Type u} {B : A → Type u} {X : Type u}
    (C : Algebra (polynomialWithVariables A B X))
    (f : freeTreeAsAlgebra A B X ⟶ C) : f = freeTreeInitialHom C := by
  apply Algebra.ext
  ext tree
  induction tree with
  | var x =>
      have h := types_congr_hom f.h (Sum.inl x)
      exact h.symm
  | sup shape branches ih =>
      have h := types_congr_hom f.h (Sum.inr ⟨shape, branches⟩)
      change C.str (.inr ⟨shape, fun position => f.f (branches position)⟩) =
        f.f (.sup shape branches) at h
      change f.f (.sup shape branches) =
        C.str (.inr ⟨shape, fun position => freeTreeInitialFold C (branches position)⟩)
      rw [← h]
      congr 3
      funext position
      exact ih position

def freeTreeIsInitial (A : Type u) (B : A → Type u) (X : Type u) :
    IsInitial (freeTreeAsAlgebra A B X) :=
  IsInitial.ofUniqueHom (fun C => freeTreeInitialHom C)
    (fun C f => freeTreeInitialHom_unique C f)

/-!
二つの普遍性は同じ再帰計算を別の圏で述べます。`freeUniversalProperty` は `P`-代数と生成元写像の組への
一意な準同型を述べます。`freeTreeIsInitial` は生成元を `Q_X` の定数構成子へ移し、通常の始対象の言葉で
述べます。この翻訳を介さず「始代数だから自由代数」とだけ言うと、何の上で自由なのかが消えてしまいます。

## 要点

* 多項式関手 `P(X)=Σa.B(a)→X` は形を保存し、各位置の値を射で写す。
* W型の構成子は `P(W)→W` という代数構造であり、W帰納法がfoldの一意性を与える。
* 不動点同型に一意な代数準同型を加えたものがW型の始代数性である。
* 変数を葉として持つ `FreeTree A B X` は、生成元写像を一意に延長する `X` 上の自由 `P`-代数である。
* 同じ自由代数は、変数を定数項として加えた自己関手 `Q_X(Y)=X+P(Y)` の始代数としても表せる。
* 「自由」は生成元の型と忘却先を指定した普遍性であり、始代数という語だけではその基底を表せない。

## 研究史と文献案内

Martin-Löf型理論におけるW型は [ML84]、帰納族への一般化は [DYB94] を参照してください。始代数意味論を
プログラム意味論と結ぶ研究は [GTWW77] に遡ります。Gambino–Hyland [GH04] はW型と依存多項式関手を
局所デカルト閉圏で研究し、広い関手類の始代数との関係を示しました。本章は `Type` 上の非依存な一変数
多項式関手に範囲を限定しており、[GH04] の依存多項式関手全体を形式化したものではありません。
Leanコードは教育用の `W` とmathlibの `Endofunctor.Algebra` を接続します。mathlib固有の現行APIは
[MATHLIB] に従い、組込み帰納型の内部表現に関する主張は行いません。

## 問題

### 自然数とリストの多項式を回収する

第37章の `NatPositions` と `ListPositions` を `polynomialFunctor` へ代入してください。自然数では
`Σb:Bool.NatPositions(b)→X` が `1+X`、リストでは `Σo:Option A.ListPositions(o)→X` が
`1+A×X` と同値であることを、両方向の関数と逆法則で示します。同値が対象ごとにあるだけでなく、射の作用と
可換して自然同型になるために必要な式も書き、単なる要素数の一致との差を説明できれば完了です。

### W型の始性証明を可換図式から再構成する

任意の `P`-代数 `C` に対する `wFoldHom C` の準同型条件を、形と位置関数を明示した等式へ展開してください。
次に別の準同型 `f` をW帰納法で比較します。帰納仮定が一つの値ではなく `∀b:B(a)` という族になる理由を
構成子の型から説明し、関数外延性を適用する正確な位置をLean証明と数式の双方で特定できれば完了です。

### 自由代数の二つの普遍性を往復する

`freeUniversalProperty` から `freeTreeIsInitial` を導くため、`Q_X`-代数から `P`-代数と生成元写像を取り出して
ください。逆に `P`-代数 `C` と `η:X→C` から `Q_X`-代数を作ります。二つの変換が準同型条件を保存し、
一意性の主張を対応させることを示します。どの圏の始対象を述べているかを各段階で明記できれば完了です。

### 多項式ではない厳密正値関手との境界を調べる

本章の表示 `Σa.B(a)→X` が和・積・冪をどのように表すかを整理し、商や関数空間の共変な組合せを含む
厳密正値関手が同じ表示を持つか検討してください。表示可能性、関手性、始代数の存在を別々の主張として扱い、
一つが失敗しても他の二つが直ちに否定されない例を挙げます。Leanの正値性検査と圏論的な多項式関手の定義を
同一視できない理由を、受理条件と普遍性の差から説明できれば完了です。
-/

end FormalLab.Bridges.PolynomialFunctorsAndWTypes