基本上概念大致上就是在universal domain $\mathcal{P}(\mathbb{N})$ 中，我們可以用PERs定義出一系列classes，而這些classes的表現就如同我們想要的types，而且可以表示dependent types跟System F那種polymorphic types

$X : T$ 表示 $X$ 的類型是 $T$ ，定義成 $X [ T ] X$ （因為型別是PER）

這裡只聊到型別部分，關於graph model本身的運作、拓樸，可以參考Scott的論文Data Types as Lattices

PER: 正確處理 exponentiation [ag-KA1U]

2026-06-25

From Denotational Semantics, looking backward - looking forward

Partial Equivalences as Types: First attempts的編碼有個缺點：exponentiation A => B 是定在函數 𝓟 ℕ → 𝓟 ℕ 上的關係，而不是一個 𝓟 ℕ 的關係，所以無法表示 A => B => A。這就是缺點的根源：A => B 不再是一個 Rel，因此 A => B => A 不合乎其型別的定義。

關鍵是 pairing : ℕ × ℕ ≃ ℕ，有了配對，一個 F : 𝓟 ℕ 就能被看成 ℕ 上的關係，用 $P(\omega)$ application 把函數放回 𝓟 ℕ。這樣 _=>_ 就封閉成 Rel → Rel → Rel，缺點消失，A => B => A 也跟著是 PER

Details [local-0]

  {-# OPTIONS --safe --without-K #-}
  open import MLTT.Spartan
  open import MLTT.List using (List; []; _∷_; member; in-head; in-tail)
  open import UF.Base using (ap₂)
  open import UF.Equiv
  open import UF.FunExt
  open import UF.Powerset
  open import UF.Subsingletons
  open import UF.SubtypeClassifier
  open import UF.PropTrunc
  open import Naturals.Binary using (pairing)
  open import Naturals.Properties using (succ-lc; positive-not-zero)

  module ag-KA1U
    (pt : propositional-truncations-exist)
    (fe : Fun-Ext)
    (pe : propext 𝓤₀)
    where

  open PropositionalTruncation pt
  open import ag-U75Z using (_[_]_; is-PER)

Definition Relation [local-1]

Rel 是 𝓟 ℕ 之間的關係

  Rel : 𝓤₀ ⁺⁺ ̇
  Rel = 𝓟 ℕ → 𝓟 ℕ → 𝓤₁ ̇

我們需要讓「函數」也住在 𝓟 ℕ 裡，這樣 _=>_ 才會是封閉的 Rel → Rel → Rel

關鍵是 pairing : ℕ × ℕ ≃ ℕ，取它的正向映射 ⌜ pairing ⌝ 把一對碼壓成一個碼。因為它是equivalence，所以是injective

encode : ℕ × ℕ → ℕ
encode = ⌜ pairing ⌝

encode-lc : {a b : ℕ × ℕ} → encode a ＝ encode b → a ＝ b
encode-lc = equivs-are-lc encode (⌜⌝-is-equiv pairing)

graph model的application不是輸入單一個編碼餵，而是餵一個**有限的編碼集合**。我們用 List ℕ 表示有限集合，用 encode 把它壓成一個 ℕ

codeList : List ℕ → ℕ
codeList []       = 0
codeList (x ∷ xs) = succ (encode (x , codeList xs))

codeList-lc : (l l′ : List ℕ) → codeList l ＝ codeList l′ → l ＝ l′
codeList-lc []       []        e = refl
codeList-lc []       (y ∷ ys)  e = 𝟘-elim (positive-not-zero _ (e ⁻¹))
codeList-lc (x ∷ xs) []        e = 𝟘-elim (positive-not-zero _ e)
codeList-lc (x ∷ xs) (y ∷ ys)  e = ap₂ _∷_ (ap pr₁ q) (codeList-lc xs ys (ap pr₂ q))
  where
  q : (x , codeList xs) ＝ (y , codeList ys)
  q = encode-lc (succ-lc e)

「有限集合 l 被 X 包含」：l 裡每個編碼都在 X 裡

_⊆ₗ_ : List ℕ → 𝓟 ℕ → 𝓤₀ ̇
l ⊆ₗ X = (k : ℕ) → member k l → k ∈ X

定義graph model的application：F ⊙ X 收集所有 m，使得存在一個有限近似 l ⊆ X，而 F 把 l（壓成的碼）送到 m

_⊙_ : 𝓟 ℕ → 𝓟 ℕ → 𝓟 ℕ
(F ⊙ X) m = (∃ l ꞉ List ℕ , (encode (codeList l , m) ∈ F) × (l ⊆ₗ X)) , ∃-is-prop
infixl 60 _⊙_

於是現在改用 F : 𝓟 ℕ → 𝓟 ℕ 的編碼版本 𝓟 ℕ，再靠 _⊙_ 取回作用。沿用記號與定義，並根據新的 Rel 定義我們需要的helpers

PER-symm : {A : Rel} → (is-PER A) → symmetric A
PER-symm per-A = per-A .pr₁
PER-trans : {A : Rel} → (is-PER A) → transitive A
PER-trans per-A = per-A .pr₂

Definition Exponentiation [local-2]

現在重新定義exponentiation

  _=>_ : Rel → Rel → Rel
  (A => B) F G = (X Y : 𝓟 ℕ) → X [ A ] Y → (F ⊙ X) [ B ] (G ⊙ Y)
  infixr 50 _=>_

把 F X 換成 F ⊙ X 後PER的證明基本上一樣

A=>B-is-PER-if-A-B-are-PERs : {A B : Rel}
     → is-PER A
     → is-PER B
     → is-PER (A => B)
A=>B-is-PER-if-A-B-are-PERs {A}{B} per-A per-B = I , II
  where
  I : symmetric (A => B)
  I F G F[A=>B]G X Y X[A]Y = goal
    where
    Y[A]X : Y [ A ] X
    Y[A]X = PER-symm per-A X Y X[A]Y

    apply : (F ⊙ Y) [ B ] (G ⊙ X)
    apply = F[A=>B]G Y X Y[A]X

    goal : (G ⊙ X) [ B ] (F ⊙ Y)
    goal = PER-symm per-B (F ⊙ Y) (G ⊙ X) apply
  II : transitive (A => B)
  II F G H F[A=>B]G G[A=>B]H X Y X[A]Y = goal
    where
    apply₁ : (F ⊙ X) [ B ] (G ⊙ Y)
    apply₁ = F[A=>B]G X Y X[A]Y

    Y[A]X : Y [ A ] X
    Y[A]X = PER-symm per-A X Y X[A]Y

    Y[A]Y : Y [ A ] Y
    Y[A]Y = PER-trans per-A Y X Y Y[A]X X[A]Y

    apply₂ : (G ⊙ Y) [ B ] (H ⊙ Y)
    apply₂ = G[A=>B]H Y Y Y[A]Y

    goal : F ⊙ X [ B ] H ⊙ Y
    goal = PER-trans per-B (F ⊙ X) (G ⊙ Y) (H ⊙ Y) apply₁ apply₂

因為封閉，套疊兩次得到 A => B => A 也是PER

A=>B=>A-is-PER : {A B : Rel}
     → is-PER A
     → is-PER B
     → is-PER (A => B => A)
A=>B=>A-is-PER per-A per-B =
  A=>B-is-PER-if-A-B-are-PERs per-A (A=>B-is-PER-if-A-B-are-PERs per-B per-A)

_=>_ 的型別現在是 Rel → Rel → Rel，缺點消失。但還有一個問題：A => B => A 既然關聯的是 𝓟 ℕ，那 fst : 𝓟 ℕ → 𝓟 ℕ → 𝓟 ℕ 活在host裡面是無法使用的，也必須被編碼成一個 𝓟 ℕ，這裡我們稱之為 K

box : ℕ → ℕ
box p = encode (codeList [] , p)

K : 𝓟 ℕ
K k = (∃ p ꞉ ℕ , k ＝ encode (codeList (p ∷ []) , box p)) , ∃-is-prop

核心引理：K ⊙ X 再作用任何 U 的結果是 X

K-const : (X U : 𝓟 ℕ) → ((K ⊙ X) ⊙ U) ＝ X
K-const X U = subset-extensionality pe fe to-X from-X
  where
  to-X : ((K ⊙ X) ⊙ U) ⊆ X
  to-X r = ∥∥-rec (∈-is-prop X r) I
    where
    I : (Σ l ꞉ List ℕ , (encode (codeList l , r) ∈ (K ⊙ X)) × (l ⊆ₗ U)) → r ∈ X
    I (l , kx , _) = ∥∥-rec (∈-is-prop X r) II kx
      where
      II : (Σ l₂ ꞉ List ℕ , (encode (codeList l₂ , encode (codeList l , r)) ∈ K) × (l₂ ⊆ₗ X)) → r ∈ X
      II (l₂ , ∈K , l₂⊆X) = ∥∥-rec (∈-is-prop X r) III ∈K
        where
        III : (Σ p ꞉ ℕ , encode (codeList l₂ , encode (codeList l , r)) ＝ encode (codeList (p ∷ []) , box p)) → r ∈ X
        III (p , eq) = transport (_∈ X) (ap pr₂ inner ⁻¹) p∈X
          where
          outer : (codeList l₂ , encode (codeList l , r)) ＝ (codeList (p ∷ []) , box p)
          outer = encode-lc eq

          inner : (codeList l , r) ＝ (codeList [] , p)
          inner = encode-lc (ap pr₂ outer)

          l₂=p∷[] : l₂ ＝ (p ∷ [])
          l₂=p∷[] = codeList-lc l₂ (p ∷ []) (ap pr₁ outer)

          p∈X : p ∈ X
          p∈X = l₂⊆X p (transport (member p) (l₂=p∷[] ⁻¹) in-head)

  from-X : X ⊆ ((K ⊙ X) ⊙ U)
  from-X r r∈X = ∣ [] , kx-mem , (λ k ()) ∣
    where
    kx-mem : encode (codeList [] , r) ∈ (K ⊙ X)
    kx-mem = ∣ (r ∷ []) , ∣ r , refl ∣ , sing-sub ∣
      where
      sing-sub : (r ∷ []) ⊆ₗ X
      sing-sub k in-head      = r∈X
      sing-sub k (in-tail ())

於是最後一個問題可以寫成

main : {A B : Rel} → K [ A => B => A ] K
main {A}{B} X Y X[A]Y U V U[B]V =
  transport (λ b → ((K ⊙ X) ⊙ U) [ A ] b) (K-const Y V ⁻¹)
    (transport (λ a → a [ A ] Y) (K-const X U ⁻¹) X[A]Y)

PER as types: product [ag-NN5N]

2026-06-26

Details [local-0]

  {-# OPTIONS --safe --without-K #-}
  open import MLTT.Spartan
  open import UF.Powerset
  open import UF.PropTrunc
  open import UF.FunExt
  open import UF.Subsingletons

  module ag-NN5N
    (pt : propositional-truncations-exist)
    (fe : Fun-Ext)
    (pe : propext 𝓤₀)
    where

  open import ag-U75Z using (_[_]_; is-PER)
  open import ag-KA1U pt fe pe using (Rel; encode; PER-symm; PER-trans)

首先我們需要針對程式的projection 1跟projection 2

Fst Snd : 𝓟 ℕ → 𝓟 ℕ
Fst X n = X (encode (0 , n))
Snd X n = X (encode (1 , n))

Definition Product [local-1]

我們把product定義成

程式的第一部分有類型 $A$ : Fst X [ A ] Fst Y
且程式的第二部分有類型 $B$ : Snd X [ B ] Snd Y

時，X [ A ×ᵣ B ] Y

  _×ᵣ_ : Rel → Rel → Rel
  (A ×ᵣ B) X Y = (Fst X [ A ] Fst Y) × (Snd X [ B ] Snd Y)
  infixr 55 _×ᵣ_

Product of PER依然是PER [local-2]

證明 A ×ᵣ B 依然是一個PER，不難看出證明就是per component而已

  A×B-is-PER : {A B : Rel}
       → is-PER A
       → is-PER B
       → is-PER (A ×ᵣ B)
  A×B-is-PER {A}{B} per-A per-B = I , II
    where
    I : symmetric (A ×ᵣ B)
    I X Y (XA , XB) =
      PER-symm per-A (Fst X) (Fst Y) XA ,
      PER-symm per-B (Snd X) (Snd Y) XB
    II : transitive (A ×ᵣ B)
    II X Y Z (XA , XB) (YA , YB) =
      PER-trans per-A (Fst X) (Fst Y) (Fst Z) XA YA ,
      PER-trans per-B (Snd X) (Snd Y) (Snd Z) XB YB

PER as types: sum [ag-MM24]

2026-06-26

Details [local-0]

  {-# OPTIONS --safe --without-K #-}
  open import MLTT.Spartan
  open import UF.Powerset
  open import UF.PropTrunc
  open import UF.FunExt
  open import UF.Subsingletons
  open import UF.DiscreteAndSeparated using (ℕ-is-set)
  open import Naturals.Properties using (positive-not-zero)

  module ag-MM24
    (pt : propositional-truncations-exist)
    (fe : Fun-Ext)
    (pe : propext 𝓤₀)
    where

  open import ag-U75Z using (_[_]_; is-PER)
  open import ag-KA1U pt fe pe using (Rel; PER-symm; PER-trans)
  open import ag-NN5N pt fe pe using (Fst; Snd)

tag 取成 singleton：｛ m ｝ 就是只含 m 的集合

｛_｝ : ℕ → 𝓟 ℕ
｛ m ｝ n = (m ＝ n) , ℕ-is-set

X = (｛0｝ , X0) 可以表示成 Fst X ＝｛ 0 ｝ 且 Snd X = X0，inr同理

is-inl is-inr : 𝓟 ℕ → 𝓤₁ ̇
is-inl X = Fst X ＝ ｛ 0 ｝
is-inr X = Fst X ＝ ｛ 1 ｝

輔助引理證明不可能既是inl又是inr

inl-and-inr-is-impossible : (X : 𝓟 ℕ) → is-inl X → is-inr X → 𝟘
inl-and-inr-is-impossible X p q =
  positive-not-zero 0 (transport (0 ∈_) (p ⁻¹ ∙ q) refl)

Definition Sum [local-1]

我們把sum定義成

要嘛兩邊都是inl、且 Snd X [ A ] Snd Y
不然就是兩邊都是inr、且 Snd X [ B ] Snd Y

  _+ᵣ_ : Rel → Rel → Rel
  (A +ᵣ B) X Y = (is-inl X × is-inl Y × (Snd X [ A ] Snd Y))
               + (is-inr X × is-inr Y × (Snd X [ B ] Snd Y))
  infixr 54 _+ᵣ_

Sum of PER依然是PER [local-2]

A +ᵣ B 依然是PER。symmetric跟transitivity的同向情況都是per component；混合情況用 inl-and-inr-is-impossible 推出矛盾排除

  A+B-is-PER : {A B : Rel}
       → is-PER A
       → is-PER B
       → is-PER (A +ᵣ B)
  A+B-is-PER {A}{B} per-A per-B = I , II
    where
    I : symmetric (A +ᵣ B)
    I X Y (inl (lX , lY , XA)) =
      inl (lY , lX , PER-symm per-A (Snd X) (Snd Y) XA)
    I X Y (inr (rX , rY , XB)) =
      inr (rY , rX , PER-symm per-B (Snd X) (Snd Y) XB)
    II : transitive (A +ᵣ B)
    II X Y Z (inl (lX , _ , XA)) (inl (_ , lZ , YA)) =
      inl (lX , lZ , PER-trans per-A (Snd X) (Snd Y) (Snd Z) XA YA)
    II X Y Z (inr (rX , _ , XB)) (inr (_ , rZ , YB)) =
      inr (rX , rZ , PER-trans per-B (Snd X) (Snd Y) (Snd Z) XB YB)
    II X Y Z (inl (_ , lY , _)) (inr (rY , _ , _)) =
      𝟘-elim (inl-and-inr-is-impossible Y lY rY)
    II X Y Z (inr (_ , rY , _)) (inl (lY , _ , _)) =
      𝟘-elim (inl-and-inr-is-impossible Y lY rY)

PER as types: dependent product & sum [ag-BQXB]

2026-06-26

Details [local-0]

  {-# OPTIONS --safe --without-K #-}
  open import MLTT.Spartan
  open import UF.Powerset
  open import UF.PropTrunc
  open import UF.FunExt
  open import UF.Subsingletons

  module ag-BQXB
    (pt : propositional-truncations-exist)
    (fe : Fun-Ext)
    (pe : propext 𝓤₀)
    where

  open import ag-U75Z using (_[_]_; is-PER)
  open import ag-KA1U pt fe pe using (Rel; PER-symm; PER-trans; _⊙_; _=>_)
  open import ag-NN5N pt fe pe using (Fst; Snd; _×ᵣ_)

依賴型別由一族 B : 𝓟 ℕ → Rel 給出。要讓它在 A 的商空間上良好定義，需要 B 在 A：U [ A ] V 時滿足 B U ＝ B V

dependent sum：Fst X 由 A 分類，Snd X 由 B (Fst X) 分類

Σᵣ : (A : Rel) → (𝓟 ℕ → Rel) → Rel
Σᵣ A B X Y = (Fst X [ A ] Fst Y) × (Snd X [ B (Fst X) ] Snd Y)
infixr 55 Σᵣ

dependent product：把 F 作用在被 A 分類的 X 上，結果由 B X 分類

Πᵣ : (A : Rel) → (𝓟 ℕ → Rel) → Rel
Πᵣ A B F G = (X Y : 𝓟 ℕ) → X [ A ] Y → (F ⊙ X) [ B X ] (G ⊙ Y)
infixr 50 Πᵣ

Dependent sum of PER依然是PER [local-1]

Per component提出證明，依賴的部分要靠 B U ＝ B V 把證明在 B (Fst X) 與 B (Fst Y) 之間搬移

  Σ-is-PER : {A : Rel} {B : 𝓟 ℕ → Rel}
       → is-PER A
       → ((U : 𝓟 ℕ) → is-PER (B U))
       → ({U V : 𝓟 ℕ} → U [ A ] V → B U ＝ B V)
       → is-PER (Σᵣ A B)
  Σ-is-PER {A}{B} per-A per-B resp = I , II
    where
    I : symmetric (Σᵣ A B)
    I X Y (p , q) =
      PER-symm per-A (Fst X) (Fst Y) p ,
      PER-symm (per-B (Fst Y)) (Snd X) (Snd Y)
        (transport (λ R → Snd X [ R ] Snd Y) (resp p) q)
    II : transitive (Σᵣ A B)
    II X Y Z (p₁ , q₁) (p₂ , q₂) =
      PER-trans per-A (Fst X) (Fst Y) (Fst Z) p₁ p₂ ,
      PER-trans (per-B (Fst X)) (Snd X) (Snd Y) (Snd Z) q₁
        (transport (λ R → Snd Y [ R ] Snd Z) (resp p₁ ⁻¹) q₂)

Dependent product of PER依然是PER [local-2]

結構與 _=>_ 相同，只是每次套用後都要把型別 B Y 搬回 B X

  Π-is-PER : {A : Rel} {B : 𝓟 ℕ → Rel}
       → is-PER A
       → ((U : 𝓟 ℕ) → is-PER (B U))
       → ({U V : 𝓟 ℕ} → U [ A ] V → B U ＝ B V)
       → is-PER (Πᵣ A B)
  Π-is-PER {A}{B} per-A per-B resp = I , II
    where
    I : symmetric (Πᵣ A B)
    I F G F[Π]G X Y X[A]Y = goal
      where
      Y[A]X : Y [ A ] X
      Y[A]X = PER-symm per-A X Y X[A]Y

      apply : (F ⊙ Y) [ B Y ] (G ⊙ X)
      apply = F[Π]G Y X Y[A]X

      apply' : (F ⊙ Y) [ B X ] (G ⊙ X)
      apply' = transport (λ R → (F ⊙ Y) [ R ] (G ⊙ X)) (resp Y[A]X) apply

      goal : (G ⊙ X) [ B X ] (F ⊙ Y)
      goal = PER-symm (per-B X) (F ⊙ Y) (G ⊙ X) apply'
    II : transitive (Πᵣ A B)
    II F G H F[Π]G G[Π]H X Y X[A]Y = goal
      where
      apply₁ : (F ⊙ X) [ B X ] (G ⊙ Y)
      apply₁ = F[Π]G X Y X[A]Y

      Y[A]X : Y [ A ] X
      Y[A]X = PER-symm per-A X Y X[A]Y

      Y[A]Y : Y [ A ] Y
      Y[A]Y = PER-trans per-A Y X Y Y[A]X X[A]Y

      apply₂ : (G ⊙ Y) [ B Y ] (H ⊙ Y)
      apply₂ = G[Π]H Y Y Y[A]Y

      apply₂' : (G ⊙ Y) [ B X ] (H ⊙ Y)
      apply₂' = transport (λ R → (G ⊙ Y) [ R ] (H ⊙ Y)) (resp Y[A]X) apply₂

      goal : (F ⊙ X) [ B X ] (H ⊙ Y)
      goal = PER-trans (per-B X) (F ⊙ X) (G ⊙ Y) (H ⊙ Y) apply₁ apply₂'

退化成非依賴時 [local-3]

當 B 是常數族時，Σᵣ 就是 product，Πᵣ 就是 exponentiation

  Σ-generalizes-× : {A B : Rel} (X Y : 𝓟 ℕ)
    → Σᵣ A (λ _ → B) X Y ＝ (A ×ᵣ B) X Y
  Σ-generalizes-× X Y = refl

  Π-generalizes-=> : {A B : Rel} (F G : 𝓟 ℕ)
    → Πᵣ A (λ _ → B) F G ＝ (A => B) F G
  Π-generalizes-=> F G = refl

Polymorphic types [ag-8LAS]

2026-06-26

Details [local-0]

  {-# OPTIONS --safe --without-K #-}
  open import MLTT.Spartan
  open import UF.Powerset
  open import UF.PropTrunc
  open import UF.FunExt
  open import UF.Subsingletons

  module ag-8LAS
    (pt : propositional-truncations-exist)
    (fe : Fun-Ext)
    (pe : propext 𝓤₀)
    where

  open import ag-U75Z using (_[_]_; is-PER)
  open import ag-KA1U pt fe pe using (Rel; PER-symm; PER-trans)

Polymorphic type量化的不是元素，而是型別（PER）本身。一支program住在 ∀X. T(X) 裡的意思是不管 X 是哪個型別，它都住在 T(X) 裡。在這裡型別就是 PER，所以這恰好是把所有instance F A 取交集

(M , N) 屬於 ∀ᵣ F iff對每個PER A 都有 M [ F A ] N

交集量化了所有 Rel，落在比 Rel 高一階的universe，但Agda的universe是predicative的，所以要提供一個新名字 Rel⁺

Rel⁺ : 𝓤₂ ⁺ ̇
Rel⁺ = 𝓟 ℕ → 𝓟 ℕ → 𝓤₂ ̇

∀ᵣ : (Rel → Rel) → Rel⁺
∀ᵣ F M N = (A : Rel) → is-PER A → M [ F A ] N

PER的交集依然是PER [local-1]

逐點證明：symmetric與transitive 都在固定的 A 上呼叫 F A 自己的PER結構，再把 A 量化回去

  ∀-is-PER : (F : Rel → Rel)
       → ((A : Rel) → is-PER A → is-PER (F A))
       → is-PER (∀ᵣ F)
  ∀-is-PER F per-F = I , II
    where
    I : symmetric (∀ᵣ F)
    I M N M[∀F]N A per-A =
      PER-symm (per-F A per-A) M N (M[∀F]N A per-A)
    II : transitive (∀ᵣ F)
    II M N L M[∀F]N N[∀F]L A per-A =
      PER-trans (per-F A per-A) M N L (M[∀F]N A per-A) (N[∀F]L A per-A)

Elimination就是instantiation [local-2]

交集對單一instance的投影，對應到polymorphic term在型別 A 上的type application

  ∀-elim : {F : Rel → Rel} (A : Rel) → is-PER A
       → {M N : 𝓟 ℕ} → ∀ᵣ F M N → M [ F A ] N
  ∀-elim A per-A M[∀F]N = M[∀F]N A per-A

Types on Scott's graph model [A3Q8]

PER: 正確處理 exponentiation [ag-KA1U]

Details [local-0]

Definition Relation [local-1]

Definition Exponentiation [local-2]

PER as types: product [ag-NN5N]

Details [local-0]

Definition Product [local-1]

Product of PER依然是PER [local-2]

PER as types: sum [ag-MM24]

Details [local-0]

Definition Sum [local-1]

Sum of PER依然是PER [local-2]

PER as types: dependent product & sum [ag-BQXB]

Details [local-0]

Dependent sum of PER依然是PER [local-1]

Dependent product of PER依然是PER [local-2]

退化成非依賴時 [local-3]

Polymorphic types [ag-8LAS]

Details [local-0]

PER的交集依然是PER [local-1]

Elimination就是instantiation [local-2]