import FormalLab.TypeTheory.IdentityTypes
import FormalLab.TypeTheory.WTypes

/-!
# 第38章：高次同一性・一価性・ホモトピー型理論

同一性の証拠を経路と読むと、二つの経路の間にも同一性があり、その同一性の間にもさらに同一性が
あります。点、経路、経路間のホモトピーという階層を切り捨てずに型の内部で扱うことが、ホモトピー
型理論（homotopy type theory; HoTT）の出発点です。

本章では経路・ホモトピー・可縮性・ファイバー・同値・一価性を順に定式化します。ただしLean 4の
`Eq` は `Prop` に属し、証明無関連性を持ちます。そのためHoTTの定義の形をLeanで照合することと、
Lean自身を一価的な型理論として使うことを区別します。この差を言葉だけで済ませず、真偽反転という
型同値がLeanの型の等式からは得られないことまで証明します。

## 経路の間の経路とホモトピー

型 `A` の二点 `x,y:A` の同一性型を `x =_A y` と書き、その要素を `x` から `y` への経路と読みます。
二つの関数 `f,g : A → B` のホモトピーは、各点 `x:A` に経路 `f(x)=g(x)` を割り当てる族です。

$$
f\sim g\;:\!\equiv\;\prod_{x:A}f(x)=_B g(x).
$$

これは点ごとの等式そのものです。関数外延性を仮定すれば `f ~ g` から関数の同一性 `f=g` を得ますが、
両者を定義だけで同一視はしません。
-/

namespace FormalLab.TypeTheory.HomotopyTypeTheory

universe u v w

def Homotopy {A : Type u} {B : Type v} (f g : A → B) : Prop :=
  ∀ x, f x = g x

theorem homotopy_refl {A : Type u} {B : Type v} (f : A → B) :
    Homotopy f f :=
  fun _ => rfl

theorem homotopy_symm {A : Type u} {B : Type v} {f g : A → B}
    (homotopy : Homotopy f g) : Homotopy g f :=
  fun x => (homotopy x).symm

theorem homotopy_trans {A : Type u} {B : Type v} {f g h : A → B}
    (first : Homotopy f g) (second : Homotopy g h) : Homotopy f h :=
  fun x => (first x).trans (second x)

theorem functionEqualityOfHomotopy {A : Type u} {B : Type v} {f g : A → B}
    (homotopy : Homotopy f g) : f = g :=
  funext homotopy

/-!
`Homotopy` は一般のHoTT記法と同じ依存関数の形を持ちます。`functionEqualityOfHomotopy` はLeanで
利用できる関数外延性を使います。HoTTでは関数外延性を一価性から導く展開もありますが、本章のLean証明は
その導出ではありません。

## 可縮な型は中心から全点へ経路を持つ

型 `A` が**可縮**（contractible）であるとは、中心 `c:A` と各点 `x:A` への経路 `c=x` があることです。

$$
\mathsf{isContr}(A)\;:\!\equiv\;
\sum_{c:A}\prod_{x:A}c=x.
$$

単に要素が存在するだけでは足りません。中心と任意の点が同一であるため、可縮な型はホモトピー的に
一点だけの情報を持ちます。
-/

def IsContractible (A : Sort u) :=
  PSigma fun center : A => ∀ point : A, center = point

def unitContractible : IsContractible Unit :=
  ⟨(), by
    intro point
    cases point
    rfl⟩

def Fiber {A : Sort u} {B : Sort v} (f : A → B) (y : B) :=
  {x : A // f x = y}

def IsEquiv {A : Sort u} {B : Sort v} (f : A → B) :=
  ∀ y, IsContractible (Fiber f y)

/-!
Leanの `Fiber` は原像と等式証拠を `Subtype` に束ねます。これは `Eq` が `Prop` に属するためであり、
通常のHoTTで用いる `Σ(x:A).f(x)=y` の高次情報を保存する定義ではありません。原像の点と等式の
端点条件は照合できますが、等式証拠どうしの相違は証明無関連性によって消えます。

関数 `f:A→B` の点 `y:B` 上のファイバーは、原像 `x:A` と経路 `f(x)=y` の対です。全ファイバーが
可縮なら、各 `y` には逆像が一意に存在するだけでなく、その一意性を経路として持ちます。この条件を
`f` が同値であることの一つの定義とします。

## 逆写像のデータから可縮なファイバーを作る

写像 `f:A→B`、逆向きの写像 `g:B→A`、左右の逆法則があれば、`y` 上のファイバーの中心は
`(g(y), f(g(y))=y)` です。別の点 `(x,p)` は、`p` を使って `g(y)` を `g(f(x))` へ移し、左逆法則で
`x` へ結びます。
-/

def isEquivOfInverse {A : Sort u} {B : Sort v} (f : A → B) (g : B → A)
    (leftInverse : ∀ x, g (f x) = x)
  (rightInverse : ∀ y, f (g y) = y) : IsEquiv f := by
  intro y
  refine ⟨⟨g y, rightInverse y⟩, ?_⟩
  intro point
  apply Subtype.ext
  exact (congrArg g point.2.symm).trans (leftInverse point.1)

structure Equiv (A : Type u) (B : Type v) where
  toFun : A → B
  equivalence : IsEquiv toFun

infix:25 " ≃ " => Equiv

def identityEquiv (A : Type u) : A ≃ A where
  toFun := fun x => x
  equivalence := isEquivOfInverse (fun x => x) (fun x => x)
    (fun _ => rfl) (fun _ => rfl)

def boolNegationEquiv : Bool ≃ Bool where
  toFun := Bool.not
  equivalence := isEquivOfInverse Bool.not Bool.not
    (by intro value; cases value <;> rfl)
    (by intro value; cases value <;> rfl)

/-!
`A ≃ B` は同値の写像と、その全ファイバーが可縮だという証拠を束ねます。同型を逆関数と二つの逆法則で
定義する方法から `isEquivOfInverse` によりこの表現へ移れます。圏同値や論理同値は量化する対象と
保存する構造が異なるため、同じ記号の見た目だけで同一視しません。

## 型の同一性は恒等同値を運ぶ

型の経路 `p:A=B` があれば、`p` に沿って輸送することで同値 `A≃B` を得ます。この標準写像を
`idtoequiv` と呼びます。反射経路では恒等同値へ計算されます。
-/

def idToEquiv {A B : Type u} (path : A = B) : A ≃ B := by
  cases path
  exact identityEquiv A

theorem idToEquiv_refl (A : Type u) :
    idToEquiv (show A = A from rfl) = identityEquiv A := rfl

/-!
一価性公理は、宇宙内の型の同一性 `A=B` と型同値 `A≃B` の間で `idtoequiv` 自身が同値であると
述べます。

$$
\mathsf{isUnivalent}(\mathcal U)\;:\!\equiv\;
\prod_{A,B:\mathcal U}
\mathsf{isEquiv}\bigl(\mathsf{idtoequiv}:(A=B)\to(A\simeq B)\bigr).
$$

「同型な構造は同一視してよい」という標語より強く、標準写像とその高次の同一性情報まで指定する
主張です。単なる全単射の存在や、同値関係による商とは区別します。
-/

def LeanTypeZeroUnivalence :=
  ∀ A B : Type, IsEquiv (@idToEquiv A B)

theorem isEquiv_surjective {A : Sort u} {B : Sort v} {f : A → B}
    (equivalence : IsEquiv f) : Function.Surjective f := by
  intro y
  let center := (equivalence y).1
  exact ⟨center.1, center.2⟩

theorem identityAndNegationDiffer : identityEquiv Bool ≠ boolNegationEquiv := by
  intro equal
  have functionsEqual := congrArg Equiv.toFun equal
  have atFalse := congrFun functionsEqual false
  contradiction

theorem boolNegationNotFromEquality :
    ¬∃ path : Bool = Bool, idToEquiv path = boolNegationEquiv := by
  rintro ⟨path, image⟩
  cases path
  exact identityAndNegationDiffer image

theorem leanTypeZeroIsNotUnivalent : LeanTypeZeroUnivalence → False := by
  intro univalent
  have surjective := isEquiv_surjective (univalent Bool Bool)
  obtain ⟨path, image⟩ := surjective boolNegationEquiv
  exact boolNegationNotFromEquality ⟨path, image⟩

/-!
真偽反転は `Bool≃Bool` ですが、Leanの `Bool=Bool` の証明を `idToEquiv` で送っても得られません。
`leanTypeZeroIsNotUnivalent` は、Lean 4の現在の `Eq` と本章の同値定義に対する定理です。一価性一般への
反例ではありません。むしろ、HoTTの一価的宇宙をLean自身の宇宙と等号で直接実装したと称しては
ならないことを形式的に示します。

## 証明無関連性は高次経路を潰す

Leanでは任意の命題の二証明が等しいため、同じ端点を持つ二つの等式証拠も等しくなります。
-/

theorem equalityProofsCollapse {A : Type u} {x y : A} (first second : x = y) :
    first = second :=
  Subsingleton.elim first second

def IsProposition (A : Sort u) : Prop :=
  ∀ first second : A, first = second

def IsSet (A : Type u) : Prop :=
  ∀ x y : A, IsProposition (x = y)

theorem everyLeanTypeLooksLikeASet (A : Type u) : IsSet A := by
  intro x y first second
  exact equalityProofsCollapse first second

/-!
HoTTで「集合」と呼ばれる0-truncatedな型は、各同一性型が命題である型です。上の素朴な翻訳ではLeanの
全ての型が集合に見えます。これはHoTTが全型を集合とみなすという定理ではなく、Leanの `Eq : Prop` が
高次情報を保持しない結果です。HoTTを忠実に計算するには、cubical type theoryなど別の基礎や、対象理論を
構文・意味論としてLean内に符号化する方法が必要です。

## 高次帰納型は点だけでなく経路も生成する

W型の構成子は新しい点を作ります。高次帰納型（higher inductive type; HIT）はさらに、既に作った点の
間の経路や高次経路を構成子として指定します。円周 `S¹` の代表的な指定は一点
`base:S¹` と一経路 `loop:base=base` です。

通常のLean帰納宣言で `base` と `loop` を二つの点構成子として書けば、二要素型になり、円周には
なりません。また、点と自己等式を持つ構造体を作っても、自由な除去原理と経路に対する計算規則は
得られません。HITの定義には点構成子、経路構成子、両者に対応する除去・計算規則が必要です。

## 要点

* 関数間のホモトピーは各入力に対する出力間の経路族である。
* 関数が同値であることは、各点上のファイバーが可縮であることとして定義できる。
* `idtoequiv` は型の同一性を型同値へ送り、一価性はこの写像自体が同値だと述べる。
* Leanの `Eq : Prop` は証明無関連であり、HoTTの高次経路をそのまま保持しない。
* 高次帰納型は点構成子に加えて経路構成子と対応する計算規則を持つ。

## 研究史と文献案内

Hofmann–Streicher [HS98] の群oid解釈は、同一性証明の一意性が内包的Martin-Löf型理論から
導けないことを意味論的に示します。Awodey–Warren [AW09] はmodel categoryによる同一性型のモデルを与え、
型理論とホモトピー論の接続を展開しました。これらの仕事を、後に定式化された一価性そのものの証明と
読み替えません。

Voevodskyの一価性公理と高次帰納型を含む体系的な展開は、2012–2013年のIAS特別年を経て共同執筆された
[HOTT13] が標準的な入口です。本章は用語とLeanとの差を厳密に確認する章であり、同書の一価的基礎を
Lean 4上で実装したものではありません。

## 問題

### 逆写像からファイバーの収縮を再構成する

`isEquivOfInverse` の中心と収縮経路を、`Σ(x:A).f(x)=y` の記法で書き直してください。収縮の証明を
`congrArg`、右辺の経路、左逆法則の三段に分け、どの等式が各段で向きを反転するかを示します。
自然数への後者関数では同じ構成が失敗するファイバーを挙げ、全射性だけでは可縮性に足りない理由を
説明すれば完了です。

### 一価性の主張を三つの弱い主張と比較する

`A=B → A≃B`、`A≃B → A=B` の単なる関数の存在、`idToEquiv` の全射性、`idToEquiv` が同値であることを
順に並べてください。各主張が前の主張へ何を加えるかをファイバーで述べます。`Bool` の恒等同値と
真偽反転を使い、Leanの `Eq` ではどの段階が破れるかを定理から再構成すれば完了です。

### 円周の除去原理に必要なデータを特定する

円周から型族 `P:S¹→Type` への依存関数を定義するため、`base` 上の点と `loop` に沿う輸送について
何を指定すべきかを書いてください。通常の帰納型の点構成子だけを二つ置く誤った符号化と比較します。
点の個数、経路の生成、計算規則の三項目で差を説明し、W型だけでは経路構成子を表さない理由を
示せば完了です。
-/

end FormalLab.TypeTheory.HomotopyTypeTheory