import FormalLab.CategoryTheory.EndofunctorAlgebras

/-!
# 全問題の解答：米田・随伴・代数と余代数

## 第51章：米田の補題と米田埋め込み

### 問題1：米田の全単射の逆法則を証明する

#### ヒント

自然変換 `α:Hom(A,-)⟶F` を `α_A(𝟙 A)` へ送り、元xからは `f↦F(f)(x)` を作ります。

#### 解答

`Φ(α)=α_A(𝟙 A)`、`Ψ(x)_X(f)=F(f)(x)` とします。`Φ(Ψ(x))=F(𝟙 A)(x)=x` は関手の恒等保存です。逆向きは
自然性を射 `f:A⟶X` へ適用し、`α_X(f)=F(f)(α_A(𝟙 A))` を得るので `Ψ(Φ(α))_X(f)=α_X(f)` です。
成分と関数の外延性から自然変換全体が等しくなります。全単射は評価と自然性だけで構成されます。

反変版では `Hom(-,A)` と前層を用い、合成の向きを型から組み直します。

#### 補足

`Type` で固定した型 `A` を考えると、各関数 `f:A→X` から自然に `X` の元を選ぶ操作は、`A` の一点を `f` で
送る操作に対応します。自然な選択から一点を戻すには恒等関数で評価します。再び任意の `f` へ進む向きで自然性を
本質的に使い、反対向きは恒等関数の法則だけで閉じます。表現可能関手でも恒等射に対応する普遍元を取り、同じ二方向を
区別します。

### 問題2：完全忠実性を米田の補題から導く

#### ヒント

自然変換 `yA⟶yB` を米田の補題でBにおける `yA` の要素へ対応させます。

#### 解答

反変米田埋め込み `y:C→[Cᵒᵖ,Type]` について
`Nat(yA,yB)≅yB(A)=Hom_C(A,B)` が米田の補題から得られます。この全単射は射fを前合成による自然変換y fへ送る
写像の逆なので、yのhom写像は全単射です。従ってyは完全かつ忠実です。対象を前層として展開しても、元の圏の
射とその自然変換の間で情報を失いません。

圏Cを具体的な関手圏へ埋め込み、対象をそのすべての一般化された要素によって研究できます。

### 問題3：自然同型から対象同型を回収する

#### ヒント

`yA≅yB` の順方向・逆方向を完全忠実性で射 `A⟶B` と `B⟶A` へ戻します。

#### 解答

自然同型の順成分に対応するfと逆成分に対応するgを米田の全単射で取ります。自然変換の合成が恒等であるため、忠実性に
より `f≫g=𝟙 A` と `g≫f=𝟙 B` が従います。従ってA≅Bです。これは表現対象の一意性を一つの計算で与え、
「すべての対象から見た射の振る舞いが自然に同じなら対象は同型」という米田的観点を表します。

積や極限を表すhom関手の自然同型から、普遍対象間の標準同型を直ちに得られます。

## 第52章：随伴——homの自然同型・単位・余単位

### 問題1：hom全単射から単位と余単位を取り出す

#### ヒント

`Hom_D(FX,Y)≅Hom_C(X,GY)` でY=FXまたはX=GYとし、恒等射を転置します。

#### 解答

単位は `η_X=Φ_{X,FX}(𝟙_{FX}):X⟶GFX` です。余単位は逆全単射で
`ε_Y=Φ^{-1}_{GY,Y}(𝟙_{GY}):FGY⟶Y`。全単射の自然性からこれらは自然変換になります。逆法則を恒等射へ適用すると
`Fη≫εF=𝟙F` と `ηG≫Gε=𝟙G` の三角恒等式が得られます。単位・余単位は追加の任意データではなく、恒等射の
転置です。

自由・忘却随伴では単位が生成元の挿入、余単位が生成された式の評価になります。

### 問題2：単位・余単位から転置を復元する

#### ヒント

`f:FX⟶Y` を `η_X≫Gf`、`g:X⟶GY` を `Fg≫ε_Y` へ送ります。

#### 解答

`transpose(f)=η_X≫G.map f`、`untranspose(g)=F.map g≫ε_Y` と定めます。前者を戻すと
`Fη_X≫FGf≫ε_Y`。余単位の自然性で中央を移し、三角恒等式でfになります。逆合成も単位の自然性ともう一方の
三角恒等式でgになります。関手法則により両写像はX,Yについて自然なのでhom自然同型を回収できます。

APIでは随伴のどの提示から始めても、転置・単位・余単位を相互変換して都合のよい形式で証明できます。

### 問題3：自由・忘却随伴を具体的に読む

#### ヒント

集合Xから自由モノイドList Xを作り、関数 `X→U M` をモノイド準同型へ延長します。

#### 解答

自由関手FはXを語のモノイドList Xへ、忘却Uはモノイドを台集合へ送ります。関数 `f:X→U M` は
`foldMap f:F X→M` へ一意に延長され、逆に準同型hは一文字語への制限 `x↦h[x]` を与えます。この対応が
`Hom_Mon(FX,M)≅Hom_Set(X,UM)` です。単位は `x↦[x]`、余単位はMの語を積で評価する写像です。

自由群・自由加群・構文木でも、生成元への割当てを構造準同型へ延長する同じ普遍性を使います。

## 第53章：モナド・余モナド・Kleisli圏・Eilenberg–Moore圏

### 問題1：Optionの自然性まで証明する

#### ヒント

単位 `some` と乗法 `join` が任意の関数fに対してmapと可換することを場合分けします。

#### 解答

Option関手は `map f none=none`、`map f (some x)=some(f x)`。単位自然性
`map f (some x)=some(f x)` は定義どおりです。乗法自然性 `map f(join z)=join(map(map f) z)` はzがnone、some none、
some(some x)の三場合で成立します。単位則はjoin∘someとjoin∘map some、結合則は三重Optionの四種の形を場合分け
すれば確認できます。値だけでなく自然変換としての一様性までがモナド構造です。

Listや例外モナドでも、関手法則・自然性・モナド法則を分けて検査します。

### 問題2：Kleisli合成の圏法則を導く

#### ヒント

`f:A→TB`、`g:B→TC` に対し `f>=>g = f≫Tg≫μ` と書きます。

#### 解答

Kleisli恒等射はηです。左単位 `η>=>f=f` はηの自然性とモナドの左単位、右単位 `f>=>η=f` は右単位から従います。
三射の二通りの合成は、関手法則とμの自然性で同じ形へ整え、モナド結合則
`Tμ≫μ=μ_T≫μ` で一致します。OptionではKleisli合成は、noneなら停止しsomeなら次の関数を実行する合成です。

do記法の再括弧付けが意味を変えない根拠を、Kleisli圏の結合律として説明できます。

### 問題3：二つの標準圏を比較する

#### ヒント

Kleisli圏は自由な計算、Eilenberg–Moore圏はT作用を解釈する代数を対象にします。

#### 解答

Kleisli圏の対象はCの対象、射A→BはCの射 `A→TB` で、モナド効果を生成して合成します。Eilenberg–Moore圏の対象は
`a:TA→A` が単位・結合法則を満たすT代数、射は作用と可換する写像です。Kleisli圏は自由代数だけからなる部分を
EM圏へ完全忠実に送れますが、一般の代数をすべて含むとは限りません。前者は計算記述、後者は計算の解釈を分類します。

随伴が誘導するモナドについて、比較関手がDをEM圏へ送り、モナド性がそれを同値にする流れへ接続します。

## 第54章：自己関手の代数と代数準同型

### 問題1：Option代数の準同型条件を特徴づける

#### ヒント

Option代数 `a:Option A→A` はnoneの像とsomeの像で決まり、単位則がsomeの場合を固定します。

#### 解答

OptionモナドのEM代数なら単位則から `a(some x)=x`。従ってaは `a(none)=d` という既定要素dだけを選びます。二つの
代数 `(A,d_A)`、`(B,d_B)` の準同型fは `f∘a=b∘Option.map f` を満たし、someの場合は自明、noneの場合は
`f(d_A)=d_B` です。つまりOption代数の圏は基点付き集合と基点保存写像の圏になります。

モナド代数を具体的な既知構造へ分類し、抽象法則がどの演算・定数を選ぶか読み取ります。

### 問題2：二項木の一層関手を構成する

#### ヒント

葉にA、節に二つの再帰位置を持つので `F X=A+X×X` とします。

#### 解答

対象写像を `F X=A+X×X`、射fのmapを葉では恒等、節では `(x,y)↦(f x,f y)` とします。恒等・合成保存は和の場合分けと
積の成分計算で従います。F代数 `α:A+X×X→X` は葉をXへ解釈する関数と、二つのXを一つへ結ぶ演算を持ちます。
二項木型はこのFの始代数の台として構成されます。

ラベル付き節や可変分岐木では一層多項式を変え、代数の演算シグネチャを機械的に得ます。

### 問題3：代数準同型の合成を検査する

#### ヒント

`h∘α=β∘Fh` と `k∘β=γ∘Fk` を代入し、関手の合成保存を使います。

#### 解答

合成について `(k∘h)∘α=k∘(h∘α)=k∘β∘Fh=γ∘Fk∘Fh=γ∘F(k∘h)`。従ってk∘hも代数準同型です。
恒等射は `id∘α=α=α∘F id` から準同型です。通常の関数合成の結合律・単位律を継承するので、F代数と準同型は
圏をなします。可換正方形は合成で貼り合わせられます。

余代数準同型では正方形の矢印を反転し、同じ貼り合わせを双対的に確認します。

## 第55章：始代数・fold・Lambekの補題

### 問題1：foldの一意性を可換正方形から再構成する

#### ヒント

始F代数 `(μF,in)` から任意の代数 `(A,α)` への代数射が一意であることを展開します。

#### 解答

fold αは方程式 `in≫fold α = F(fold α)≫α` を満たします。これはfoldが代数準同型である条件です。別の
`h:μF→A` が同じ方程式を満たせばhも同じ二代数間の準同型なので、始性から `h=fold α`。従って再帰方程式は
存在だけでなく一意な解を指定します。リストではnil・consの二方程式がこの一枚の正方形へまとまります。

融合則は合成が同じ代数準同型方程式を満たすことを示し、foldの一意性だけで証明します。

### 問題2：Lambekの補題を始性だけから証明する

#### ヒント

代数 `(FμF,F in)` への一意な代数射hを取り、inとの合成を始性で比較します。

#### 解答

始代数を `(A,α:FA→A)` とします。`(FA,Fα)` への一意な代数射 `h:A→FA` を取ります。α自体は
`(FA,Fα)→(A,α)` の代数射です。合成 `h≫α` は始代数Aから自身への代数射なので恒等射と等しい。一方、hの
準同型条件とこの等式をFで写すことから `α≫h=𝟙_{FA}` も導けます。従ってαは同型です。

終余代数の構造射も双対Lambek補題で同型になり、unfold/fold型の不動点方程式を与えます。

### 問題3：不動点と始代数を分ける反例を探す

#### ヒント

恒等関手Idでは任意の対象Aに恒等射 `A→A` があり、不動点になります。

#### 解答

F=Idなら `(A,id_A)` はすべてF代数で、構造射は同型です。しかし始代数は元の圏の始対象に対応し、任意のAが始とは
限りません。`Type` では空型が始ですがNatも `Id Nat≅Nat` を満たします。従って同型 `FA≅A` は不動点の存在しか
述べず、任意のF代数への一意な準同型という始性を含みません。

再帰方程式の解を得た後も、最小性・始性・選んだ意味論的順序を別途検証します。

## 第56章：自己関手の余代数と余代数準同型

### 問題1：停止し得る遷移の準同型を作る

#### ヒント

関手 `F X=1+A×X` の余代数は、停止か出力と次状態を返す機械です。

#### 解答

自然数状態nからnが0なら停止、正ならラベルnと状態n-1を返す余代数cを考えます。状態を偶奇など別表現へ写すhが
余代数準同型であるには `c≫Fh=h≫d`、つまり停止判定・現在出力・次状態写像がすべて保存される必要があります。
単に最初の出力が同じだけでは不十分です。カウントダウン状態を残り要素のリストへ送る写像なら、尾への遷移と可換します。

プロトコルの状態表現を変更するとき、観察と遷移を同時に保存する準同型を正当性条件にします。

### 問題2：余代数準同型の合成を証明する

#### ヒント

`c≫Fh=h≫d` と `d≫Fk=k≫e` を貼り合わせます。

#### 解答

`c≫F(k∘h)=c≫Fh≫Fk=h≫d≫Fk=h≫k≫e` です。関手の合成保存、hとkの準同型条件、結合律を使いました。
恒等射も関手の恒等保存から準同型です。従ってF余代数は圏をなし、内部状態表現の段階的変換を合成できます。

準同型が同型なら二つの状態機械は内部状態の改名を除いて同じ構造を持ちます。

### 問題3：代数の定義を反対圏で双対化する

#### ヒント

F代数射 `FA→A` を反対圏でopし、誘導された反対関手の余代数射として読みます。

#### 解答

自己関手F:C→Cは反対圏上に `Fᵒᵖ:Cᵒᵖ→Cᵒᵖ` を誘導します。代数構造 `α:FA→A` はopすると
`α.op:op A→Fᵒᵖ(op A)` となり余代数です。代数準同型の可換正方形も全射を反転すると余代数準同型の正方形になります。
この対応は代数圏の反対圏と反対関手の余代数圏の同型を与えます。

始代数の定理を反対圏へ適用し、終余代数の双対定理を体系的に生成します。

## 第57章：終余代数・anamorphism・振舞意味論

### 問題1：状態機械からストリームを生成する

#### ヒント

余代数 `c:S→A×S` の出力と次状態を反復し、`Stream A` への写像を定めます。

#### 解答

`ana c(s)` の先頭は `(c s).1`、尾は `ana c((c s).2)` と定めます。例えば `c(n)=(n,n+1)` ならnから始まる自然数列を
生成します。ストリームの構造射 `out:Stream A→A×Stream A` に対し
`ana c≫out=c≫(id×ana c)` が成り立ち、ana cは余代数準同型です。終余代数性がこの写像の一意性を保証します。

unfold、状態機械のトレース、遅延生成器を同じanamorphismとして設計できます。

### 問題2：anamorphismの一意性を証明する

#### ヒント

終余代数への余代数準同型は一意であるという定義を直接適用します。

#### 解答

`h:S→νF` が `c≫Fh=h≫out` を満たすならhは `(S,c)` から終余代数 `(νF,out)` への準同型です。ana cも同じ準同型なので、
終性により `h=ana c`。ストリームではhの先頭と尾が生成規則どおりなら、すべての有限観察が一致し、関数全体が一意です。
方程式を満たす候補を構成した後、一意性は別の余帰納的計算をせず普遍性で閉じられます。

状態最小化後の機械が同じ振舞意味論を持つことを、終余代数への射の一意性で証明します。

### 問題3：双模倣からストリーム等式を導く

#### ヒント

双模倣関係Rを状態とし、二つの射影を元の余代数への準同型にします。

#### 解答

Rが出力一致と後続対の閉性を満たすなら、R自体に余代数構造を入れられます。二射影 `π₁:R→S`、`π₂:R→S` は
準同型で、振舞写像 `beh:S→Stream A` との合成はどちらもRから終余代数への準同型です。終性から
`π₁≫beh=π₂≫beh`。従ってRで関係する状態の生成ストリームは等しいです。

双模倣を終余代数への振舞写像の核関係と比較し、完全抽象性の条件へ進めます。

-/

namespace FormalLab.Appendix.Solutions.Chapter054Exercise002

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor

universe u

/-- 葉を一種類だけ持つ二項木の、一層分の形 `1 + X × X`。 -/
def binaryTreeLayer : Type u ⥤ Type u where
  obj X := Unit ⊕ (X × X)
  map f := ↾(Sum.map id fun pair ↦ (f pair.1, f pair.2))
  map_id X := by
    apply ConcreteCategory.hom_ext
    intro layer
    cases layer <;> rfl
  map_comp f g := by
    apply ConcreteCategory.hom_ext
    intro layer
    cases layer <;> rfl

/-- 一層分の葉の個数を計算する構造写像。 -/
def leafCount : Unit ⊕ (Nat × Nat) → Nat
  | Sum.inl _ => 1
  | Sum.inr (left, right) => left + right

/-- 葉を1と数え、節では左右の個数を加える代数。 -/
def leafCountAlgebra : Algebra binaryTreeLayer where
  a := Nat
  str := ↾leafCount

example : leafCount (.inl Unit.unit) = 1 := rfl
example : leafCount (.inr (2, 3)) = 5 := rfl

end FormalLab.Appendix.Solutions.Chapter054Exercise002

namespace FormalLab.Appendix.Solutions.Chapter051Exercise001

structure NaturalSelector (A : Type) where
  app : (X : Type) → (A → X) → X
  natural : ∀ (X Y : Type) (f : A → X) (g : X → Y),
    app Y (g ∘ f) = g (app X f)

def selectorFromPoint {A : Type} (point : A) : NaturalSelector A where
  app _ function := function point
  natural _ _ _ _ := rfl

def pointFromSelector {A : Type} (selector : NaturalSelector A) : A :=
  selector.app A id

theorem selectorRecovered {A : Type} (selector : NaturalSelector A)
    (X : Type) (function : A → X) :
    (selectorFromPoint (pointFromSelector selector)).app X function = selector.app X function := by
  simpa [selectorFromPoint, pointFromSelector, Function.comp_def] using
    (selector.natural A X id function).symm

end FormalLab.Appendix.Solutions.Chapter051Exercise001