import FormalLab.Logic.Equality

/-!
# 第42章：始対象と終対象——零項の普遍性

空型に要素はなく、単位型には一つだけ要素があります。しかし圏論は要素数を直接数えず、
他の対象との射だけで同じ特徴を表します。空型からは任意の型へただ一つ関数があり、任意の
型から単位型へもただ一つ関数があります。この「任意の相手に対する存在と一意性」が、
始対象と終対象の最初の普遍性です。

本章ではまだ一般の圏をLeanで定義せず、型を対象、関数を射とする `Type` の圏で普遍性の
論理的な骨格を取り出します。内部表現から、射による特徴づけへ視点を移します。そこで現れる
「データ、方程式、一意な媒介射」は、後の普遍構成でも反復されます。具体的には積・余積、
一般の圏、表現可能関手で再び現れます。

## 全ての対象との一意な射で特徴づける

圏 `𝒞` の対象 `I` が始対象、`T` が終対象であることを

$$
I\;\text{が始対象}
\quad\Longleftrightarrow\quad
\forall A\in\mathrm{Ob}(\mathcal C).\,\exists!f:I\to A,
$$

$$
T\;\text{が終対象}
\quad\Longleftrightarrow\quad
\forall A\in\mathrm{Ob}(\mathcal C).\,\exists!g:A\to T.
$$

と書きます。型を対象、関数を射とみなす圏では、型 `I` が対象 `A` に対して**始的**であるとは、
`I → A` が一意に存在することです。型 `T` が `A` に対して**終的**であるとは、
`A → T` が一意に存在することです。

この見方では、型の内部を直接調べる代わりに、他の型との関数空間によって特徴づけます。
圏論でいう**対象**は点、**射**は向き付きの関係ではなく合成できる写像です。この章では
恒等関数と関数合成を持つ「型と関数」の世界だけを扱い、一般の圏の構造体はまだ導入しません。

ここでは宇宙サイズの問題を隠さないため、「全ての型を集めた圏」をまだ定義せず、対象
`A` ごとの性質 `IsInitialAt I A` と `IsTerminalAt T A` を定義します。全対象について
この性質を持つことが、圏論での始対象・終対象です。


-/

namespace FormalLab.CategoryTheory.InitialAndTerminal

universe u v

open FormalLab.Logic.Equality

/-!
## 固定した相手に対する一意な関数を定義する

`ExistsExactlyOne` を展開すると、始性の証明には次の三成分が必要です。

1. 標準射 `chosen : I → A`。
2. その射が要求された条件を満たす証明。この章では条件が `True` なので自明。
3. 任意の別の射 `f : I → A` が `chosen` と等しいという一意性。

「射が一つ以下」だけでも「少なくとも一つ」だけでも足りません。普遍性では存在と一意性を
分けて確認します。
-/

/-- `I` から `A` への関数がただ一つ存在する、という相対的な始性です。 -/
def IsInitialAt (I : Type u) (A : Type v) : Prop :=
  ExistsExactlyOne (fun _ : I → A => True)

/-- `A` から `T` への関数がただ一つ存在する、という相対的な終性です。 -/
def IsTerminalAt (T : Type u) (A : Type v) : Prop :=
  ExistsExactlyOne (fun _ : A → T => True)

/-- 指定した対象宇宙の全型に対する始性です。 -/
def IsInitial (I : Type u) : Prop :=
  ∀ A : Type v, IsInitialAt I A

/-- 指定した対象宇宙の全型に対する終性です。 -/
def IsTerminal (T : Type u) : Prop :=
  ∀ A : Type v, IsTerminalAt T A

/-!
## 空型は始的である

`Empty → A` の関数定義で入力を受け取っても、入力の構成子は一つもありません。そのため
どの `A` に対しても分岐なしで関数を定義できます。一意性も同じ理由から、二つの関数を
各入力で比較する場面そのものがありません。
-/

/-- 空型から任意の型への関数。処理すべき入力構成子はありません。 -/
def fromInitial (A : Type v) : Empty → A :=
  fun impossible => nomatch impossible

/-- 空型から `A` への任意の関数は標準関数と等しい。 -/
theorem fromInitialUnique (A : Type v) (f : Empty → A) : f = fromInitial A := by
  funext impossible
  exact nomatch impossible

/-- `Empty` から固定した任意の対象 `A` への射は一意に存在します。 -/
theorem emptyIsInitialAt (A : Type v) : IsInitialAt Empty A :=
  ⟨fromInitial A, True.intro, fun f _ => fromInitialUnique A f⟩

/-- `Empty` は指定した宇宙の全ての型に対して始的です。 -/
theorem emptyIsInitial : IsInitial Empty :=
  fun A => emptyIsInitialAt A

/-!
## 単位型は終的である

`A → Unit` では入力はいくつあっても、出力候補は `()` 一つだけです。存在は全入力を `()`
へ送る関数で示し、一意性は任意の関数の出力 `f x : Unit` を場合分けすると `()` しかない
ことから示します。始性では始域の空性、終性では終域の一点性が、一意な関数という同じ
外部的条件へ現れます。
-/

/-- 任意の型から単位型へ、全入力を唯一の構成子へ送ります。 -/
def toTerminal (A : Type v) : A → Unit :=
  fun _ => ()

/-- `A` から単位型への任意の関数は標準関数と等しい。 -/
theorem toTerminalUnique (A : Type v) (f : A → Unit) : f = toTerminal A := by
  funext x
  cases f x
  rfl

/-- 固定した任意の対象 `A` から `Unit` への射は一意に存在します。 -/
theorem unitIsTerminalAt (A : Type v) : IsTerminalAt Unit A :=
  ⟨toTerminal A, True.intro, fun f _ => toTerminalUnique A f⟩

/-- `Unit` は指定した宇宙の全ての型に対して終的です。 -/
theorem unitIsTerminal : IsTerminal Unit :=
  fun A => unitIsTerminalAt A

/-!
## `Type` における実例と一般の圏

空型から関数を作れることは、空型の値を作れたという意味ではありません。単位型への
関数が一意であることは、始域が一点だという意味でもありません。どちらも関数空間の
一意性です。また始対象・終対象は一般に文字通り同じ対象ではなく、矢印を反転することで
交換される**双対**な概念です。

一般の圏では始対象や終対象が文字どおり一つの内部表現に決まるとは限りません。しかし二つの
始対象があれば、その普遍性から両方向の一意な射が生じ、合成は一意性によって恒等射になる
ため一意な同型が得られます。「一意」は通常、等号による一意性ではなく**一意な同型を除く
一意性**です。

## 要点

* 普遍性は対象の内部表現より、他の対象との射の存在と一意性で対象を特徴づける。
* 始対象から任意の対象へは一意な射が出て、任意の対象から終対象へは一意な射が入る。
* `Empty` の始性は入力がないこと、`Unit` の終性は出力候補が一つであることに由来する。
* 始対象と終対象はすべての矢印を反転すると交換される双対概念である。
* 普遍対象の一意性は、一般には一意な同型を除く一意性である。

## 研究史と文献案内

Eilenberg–Mac Laneの1945年論文 [EM45] は、圏・関手・自然同値を体系的に導入しました。
ただし、現在の教科書的な普遍性の全体系を同論文へ帰属させることはできません。始・終対象と普遍構成を
現代の記法で学ぶには [LEI14]、標準的な研究語彙は [MAC98]、型理論・論理との接続は
[LS86] を参照してください。

## 問題

### 存在一意性を型のデータへ分解する

`IsInitialAt I A` を展開し、各対象 `A` への射、満たす条件、その射の一意性を区別せよ。
関数の圏における `Empty` について `fromInitial` を構成し、この関数が `Empty` の項を作っている
のではなく、存在しない入力を除去していることを説明する。

同様に `Unit` への射を構成し、`fromInitialUnique` と `toTerminalUnique` がそれぞれ空性と一点性を
どこで使うかを比較せよ。対象の要素数と、その対象を始域・終域とする射の一意性を混同しないこと。

### 普遍対象の一意性を導く

二つの始対象 `I` と `J` を仮定し、普遍性から `I ⟶ J` と `J ⟶ I` を得よ。二つの合成が各恒等射に
等しいことを、射の具体的定義ではなく一意性だけから示す。これにより始対象が一意な対象ではなく、
一意な同型を除いて一意であることを導け。

同じ議論を終対象へ双対化し、どの等式で合成順序が反転するかを明記する。証明を丸ごと暗記せず、
普遍性の一意性節から再構成できれば完了である。

### 射を反転して終性を復元する

始性の定義に現れる全ての射を反転し、終性の式を数式で書け。反対圏という語を使う前に、対象を
変えず射の向きと合成順序を変える操作として説明する。

`A → Unit` が一意であることから `A` が一点型だとは結論できない具体例を与えよ。普遍性は対象の
内部要素を直接数える条件ではなく、周囲の全対象との射の配置を特徴づける条件であることを示すこと。
-/

end FormalLab.CategoryTheory.InitialAndTerminal