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

  {-# 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)

  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 []       = 
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  _⊙_

於是現在改用 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₂

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

把 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)