5.3.2.12 Natural isomorphism

ステートメント

• α::F⇒G:C→D is-natural-iso ⇔ ∀(A in C).( α_A is-iso in D )

主要な概念・命題

1. α::F⇒G:C→D is-iso within Cat(C, D) in Cat
2. ∃(β::G⇒F:C→D within Cat(C, D)).
   α;β = ID_F ∧ β;α = ID_G within Cat(C, D) in Cat
3. α;β = ID_F in Cat(C, D) ⇔ ∀(A in C).( A.(α;β) = A.ID_F in D)
4. A.(α;β) = A.ID_F in D ⇔
   A.α ; A.β = A.F in D ⇔
   β_Aα_A = F(A) in D
5. β;α = ID_G in Cat(C, D) ⇔ ∀(A in C).( A.(β;α) = A.ID_G in D)
6. A.(β;α) = A.ID_G in D ⇔
   A.β ; A.α = A.G in D ⇔
   α_Aβ_A = G(A) in D
7. ∀(A in C).( β_Aα_A ∧α_Aβ_A = G(A) in D )
8. ∀(A in C).( β_A and α_A are-inversion-pair in D )
9. ∀(A in C).( α_A is-invertible in D )

補足説明： Within と In

• X in A -- Xというナニカを、Aという世界のなかで考える。Aのさらに外の世界は（当面は）考えない。
• X within A in B -- Xというナニカを、Bという世界のなかで考える。Xは、世界Bの一部分であるAのなかに閉じ込められている。
• X in A in B -- XというナニカはAという世界のなかに居る。世界Aは、さらに外の世界Bのなかに居る。
• 世界Bの一部分であるAを取り出して（独立させて）世界Aと考えることもある。

世界（環境）に対して、そこに居るモノをインハビタント〈inhabitant | 住人 | habitant (仏) | アビ{ト | タ}ン〉、インハビタントからみての世界（環境）をアビタ〈生息地 | habitat (仏)〉と呼ぶ。居住〈inhabitation | 生息〉は、型理論で使われる用語。

実体が同じモノであっても、アビタが違えば、アビタにおける位置付けや役割が変わるので、あたかも違ったモノのように扱うことがある。

• 「僕のおとうさん」と「お友達のおとうさん」 (C A4)

同値な概念

すべて同値：

1. f:A→B is-iso in C
2. f:A→B is-iso-1 in C
3. f:A→B is-invertible in C
4. f:A→B is-invertible-1 in C
5. For f:A→B in C, ∃(g:B→A in C).( f:A→B , g:B→A are-inversion-pair in C )
6. For f:A→B in C, ∃(g:B→A in C).( f:A→B , g:B→A are-inversion-pair-2 in C )
7. For f:A→B in C, ∃(g:B→A in C).( f;g = id_A ∧ g;f = id_B in C )

すべて同値：

1. α::F⇒G is-iso in C
2. α::F⇒G is-iso-2 in C
3. α::F⇒G is-invertible in C
4. α::F⇒G is-invertible-2 in C
5. For α::F⇒G in C, ∃(β::G⇒F in C).( α::F⇒G, β::G⇒F are-inversion-pair in C )
6. For α::F⇒G in C, ∃(β::G⇒F in C).( α::F⇒G, β::G⇒F are-inversion-pair-2 in C )
7. For α::F⇒G in C, ∃(β::G⇒F in C).( α;β = ID_F ∧ β;α = ID_G in C )

特に、C = Cat のときは、次が同値：

1. α::F⇒G:C→D is-invertible-2 in Cat
2. For α::F⇒G:C→D in Cat, ∀(A in C).( α_A is-invertble-1 in D )