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

Polymorphic types [ag-8LAS]

Details [local-0]

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

Elimination就是instantiation [local-2]