Take $R = \mathbb{Z}$ and the real projective plane $\mathbb{R}P^2$ as a $\Delta$-complexDefinitionDelta complex2026-10-04 · Lîm Tsú-thuàn: two vertices $v, w$, three edges $a, b, c$, and two triangles $U, L$.

Order the vertices of each triangle $[v_0, v_1, v_2]$ so that $v_0 v_1 = c$ in both, $v_1 v_2 = a, v_0 v_2 = b$ in $U$, and $v_1 v_2 = b, v_0 v_2 = a$ in $L$. Then

In the bases $U, L$ and $a, b, c$, the Smith normal form of $\partial_2$ is

so the invariant factors are $a_1 = 1, a_2 = 2$ and $n = 2$. For $b$, we have $\partial_1 a = \partial_1 b = w - v$ and $\partial_1 c = 0$, so $\partial_1$ has rank $1$

Hence, $b = 2 - 2 = 0$. Now applied the theorem

The boundary of $\Delta^n$ is

The interior of $\Delta^n$ is $\Delta^n \setminus \partial \Delta^n$.

A $\Delta$-complex is a topological space $X$ with a family of maps

for each $n \ge 0$ such that ($\Delta^n$ is the standard $n$-simplex)

1. Each interior restriction of map $\sigma^n_\alpha$ is injective
2. Each point $x \in X$ lies in the image of interior restriction of $\sigma^n_\alpha$ for exactly one $\sigma^n_\alpha$
3. Each $i$-boundary restriction of $\sigma^n_\alpha$ is equal to some $\sigma^{n-1}_\beta$ where we identify the $i$-boundary with a $\Delta^{n-1}$ by the unique linear homeomorphism that preserves the order of the vertices
4. A subspace $A \subseteq X$ is open if and only if $(\sigma^n_\alpha)^{-1}(A) \subseteq \Delta^n$ is open for all $\sigma^n_\alpha$

A $\Delta$-complex $X$ comes with a filtration by skeleta $X^0 \subseteq \cdots \subseteq X^k \subseteq \cdots \subseteq X$ where the $k$-skeleton $X^k$ is the union of all images of simplices of dimension at most $k$.

A $\Delta$-complex $X$ is called $k$-dimensional if $X^k = X$ and $X^{k-1} \ne X$; and it is called infinite dimensional if there is no such $k$.

We say that $X$ is of finite type if for each $k \ge 0$, it has only finitely many $k$-simplices. We say $X$ is finite if it has only finitely many simplices altogether.

Let $X$ be a $\Delta$-complexDefinitionDelta complex2026-10-04 · Lîm Tsú-thuàn. The $n$-th simplicial chain module $C^\Delta_n(X)$ is the free $\mathbb{Z}$-module with basis

Accordingly, each element of the $n$-th simplicial chain module is a formal $\mathbb{Z}$-linear combination

with finitely many nonzero coefficients. We call them simplicial $n$-chains in $X$.

The boundary homomorphism $\partial_n : C^\Delta_n(X) \to C^\Delta_{n-1}(X)$Definition$n$-th simplicial chain module and $n$-chains2026-10-04 · Lîm Tsú-thuàn for $n \ge 1$ is defined on the basis by

i.e. Alternatively add each restriction $\sigma^n_\alpha\vert_{[v_0, \dots, \widehat{v}_i, \dots, v_n]}$. Recall the third condition of $\Delta$-complexDefinitionDelta complex2026-10-04 · Lîm Tsú-thuàn.

The composition $C^\Delta_n(X) \xrightarrow{\partial_n} C^\Delta_{n-1}(X) \xrightarrow{\partial_{n-1}} C^\Delta_{n-2}(X)$DefinitionBoundary homomorphism (also known as differential)2026-10-04 · Lîm Tsú-thuàn is the zero map.

The $n$-th homology group of a chain complexDefinitionChain complex2026-10-04 · Lîm Tsú-thuàn $(C_\bullet, \partial_\bullet)$ is the $R$-module

The $n$-th simplicial homology group of a $\Delta$-complex $X$ is the $\mathbb{Z}$-module

Suppose we are given a Turing machine $e$ terminates with result $0$ or $1$ on all inputs, such that $e(n) = 0$ when $n \in A$ and $e(n) = 1$ when $n \in B$. Consider the algorithm $F$ that returns a Turing machine for a given natural number:$halt(k)$ is the machine that terminates with result $k$ on every input.

Because $e$ terminates on all inputs, so does $F$. By construction $e(F(n)) \ne e(n)$ for each input $n$: Consider the case that $e(n) = 0$, then $F(n) = halt(1)$. $halt(1) \in B$ because

but then $e(F(n)) = e(halt(1)) = 1 \ne 0 = e(n)$. The same argument applies to $e(n) = 1$.

By the second recursion theoremhttps://www.math.ucla.edu/~ynm/lectures/2009csl.pdf, there exists a Turing machine $f$ realizing $F$ applied to its own Gödel number, that is, $\phi_{\ulcorner f \urcorner} \simeq \phi_{\ulcorner F(f) \urcorner}$. Because $F(f)$ is $halt(0)$ or $halt(1)$, both constant, $\phi_{\ulcorner f \urcorner}$ is constant as well, say with value $k$. Hence

so either both $f$ and $F(f)$ lie in $A$, or both lie in $B$. In either case $e(f) = e(F(f))$. However, $e(n) \ne e(F(n))$ for all $n$.

A profunctor $P$ is a functor of the form

節點的角色應該是以下三種之一

• Follower
• Candidate
• Leader

我們希望leader至多只有一個，只有有leader的集群才會對外提供服務

任期可以叫term或是generation clock，用來這是第幾輪的決策，每個節點都要有這個資訊

日誌的每個entry應該包含

• 索引（index），每次新增entry都應該嚴格遞增的數字
• 任期（term），entry寫入時的任期
• 指令（command），要進行什麼操作

節點啟動時可以不知道leader是誰，我們可以設定為

• term為1
• 角色為follower
• 設定定時任務檢查leader發送的heartbeat訊號

如果定時任務歸零時沒有收到leader發送的heartbeat訊號，就發起選舉；反之，重設定時任務

leader如果直接看到比自己大的term（無論是heartbeat還是投票訊息），都應該放棄leader身份轉換為follower

現在我們來看逾時後投票的效果

Rama叢集由三個常駐行程組成：

• Zookeeper：存叢集metadata。Rama透過一層叫Metastore的抽象使用它，記錄哪個節點該跑哪些module worker、以及replication的leader election
• Conductor：CLI的接口，同時提供web版的Cluster UI，負責管理模組部署
• Supervisor：每台工作機跑一個，負責處理實際執行運算的worker process的調度

各自要獨立執行：

# 內建的單機 ZK，官方標注不適合正式環境
nohup ./rama devZookeeper >/dev/null 2>&1 &
nohup ./rama conductor >/dev/null 2>&1 &
nohup ./rama supervisor >/dev/null 2>&1 &

listening ports

2000   zookeeper
1973   conductor        <- CLI client 只需要這個
8888   cluster UI
3000   supervisor HTTP  ┐
3001   worker           ├ supervisor.port.range 的前幾個 port
3002   worker           ┘

Conductor的UI開在8888，裡面有相當豐富的runtime telemetry。要讓那些數字有東西可看，要先部署內建的monitoring模組，也順手設定一下遙測的保留期避免把磁碟吃光：

./rama deploy --action launch --systemModule monitoring --tasks 4 --threads 2 --workers 1
./rama monitoringConfig --setRetention 60,90000

Supervisor會拿 supervisor.port.range 的第一個 port 開自己的HTTP server，worker則往後依序取用。如果預設的 [3000, 4000] 跟機器上其他東西撞到，就需要更改這個設定

我改成 [3100, 4000]，結果每一個CLI指令都開始噴 Invalid config，連唯讀的 confValue 都不能用了，表示config驗證發生在所有指令的共同路徑上

文件說明只有說「port allocation range，預設 3000, 4000」，沒講到限制。試出來的結果是這樣：

[3000, 4000]   OK
[3100, 4100]   OK
[4000, 5000]   OK
[3100, 3200]   INVALID
[3001, 4000]   INVALID

所以range的寬度可能是必須恰好等於 1000，起點沒有限制。所以正確的閃避方式是平移整段ports

supervisor.port.range: [3100, 4100]

文件寫的支援範圍是Java 8/11/17/21，我機器上是 26。實測下來所有功能都正常，唯一的問題是RocksDB的JNI會噴warning

WARNING: java.lang.System::loadLibrary has been called by org.rocksdb.RocksDB
WARNING: Restricted methods will be blocked in a future release

現在只是警告，但未來的 JDK 會直接封鎖

是的，對真正的cluster來說沒有免ZK的模式

1. 只是要開發、測試 module：用 InProcessCluster，把 Rama 當成 Maven 依賴拉進專案，InProcessCluster.create() 會在 process 內模擬一整個叢集，API 跟真叢集完全相同。不需要 ZK、不需要 CLI、不需要任何 daemon。官方建議的開發流程就是用 IPC 開發測試，再用 CLI 部署到真叢集
2. 自用的小叢集：ZK 要有，但不需要是額外的機器。內建的 devZookeeper 就是一個單機 ZK，跟 Conductor 擠同一台就好。它沒有 HA，ZK 掛了叢集就失去協調能力，自用場景通常還可以接受；不然就是要自己開一個獨立的 Apache ZooKeeper

所以ZK是必要的元件，但不一定需要額外的機器

這是我最想確認的使用方式：把叢集跑在別的機器上，然後從筆電下部署指令

client 端的 rama.yaml 只需要一行。我把設定刪到只剩 conductor.host，conductorReady、moduleStatus、deploy --action update 都還是能用

再來我讓 zookeeper.servers 指向一個不存在的host，上面的指令包含deploy在內照樣成功。也就是說CLI client完全不需要管Zookeeper，它只跟Conductor對話，module的jar是上傳給Conductor、再由Conductor散佈出去的

兩個要注意的地方：rama.yaml 這個檔案本身必須存在而且非空，空檔案會得到錯誤訊息 Could not find rama.yaml on classpath；另外client端的release版本必須跟叢集完全一致

所以一組最小的遠端配置是這樣。叢集那台，Conductor、Supervisor、ZK 都在上面執行：

conductor.host:
  internal: "localhost"
  external: "10.0.0.1"     # cluster 對外的 IP
local.dir: "/var/rama"
zookeeper.servers: ["localhost"]
worker.child.opts: "-Xmx4096m"

Client的設定只需要

conductor.host: "10.0.0.1"

內建的免費license上限是2 台 Supervisor 節點，Conductor跟Zookeeper不計。用 rama licenseInfo 可以看到 num-nodes: 2，有效期到2117年

所以自用的天花板就是兩台工作機。再往上要跟 RPL 買 license，拿到以後用 rama upsertLicense --licensePath xxx.edn 裝上去

# 部署自己的 module
rama deploy \
  --action launch \
  --jar target/app.jar \
  --module com.foo.MyModule \
  --tasks 64 \
  --threads 16 \
  --workers 8 \
  --replicationFactor 2

# 程式改動之後重新部署
rama deploy --action update \
  --jar target/app.jar \
  --module com.foo.MyModule

rama scaleExecutors --module com.foo.MyModule --threads 90 --workers 30
rama moduleStatus com.foo.MyModule
rama destroy --module com.foo.MyModule

rama repl --module com.foo.MyModule
rama runClj my.ns /path/to.jar
rama backup / supportBundle
rama shutdownCluster

--tasks 必須是 2 的次方，而且要滿足 tasks >= threads >= workers。這個約束在 deploy 跟 scaleExecutors 都適用

Only prove right adjoints preserve limits here, left adjoints case is dual.

It basically invokes Hom-functors preserve limits twice

The key is this: By definition of sieve, for any element $f \in R$, the set $f^*(R)$ is a maximal sieve of $\text{dom}(f)$! Because let's see

because elements of $R$ are closed under composition, $f^*(R)$ is the maximal sieve of $\text{dom}(f)$:

Because all elements of $R$ also belongs to $S$, we have $f^*(R) \subseteq f^*(S)$; but $f^*(R)$ is the maximal sieve of $\text{dom}(f)$, hence $f^*(R) = f^*(S)$.

Recall that maximal sieve of $U$ belongs to $J(U)$, implies that for any $f \in R$, we have $f^*(S) \mathbin{⪧}_J \text{dom}(f)$. We apply property (iii), conclude that $S \mathbin{⪧}_J U$.

We can construct

In a category $\mathcal{C}$, a maximal sieve of an object $X \in \mathcal{C}$ is defined as

The maximal sieve $M_X \mathbin{⪧}_J X$.

If $S \mathbin{⪧}_J X$ and $f : Y \to X$, then

$f^*(S)$ defined by

We can represent it as

Let $S \mathbin{⪧} X$ be a sieve on $X$, and $T \mathbin{⪧}_J X$ be a sieve in $J(X)$. If for all $f \in T$ we have $f^*(S) \mathbin{⪧}_J \text{dom}(f)$, then $S \mathbin{⪧}_J X$.

Let $A$ be a lattice, then $A$ is a frame iff it is a complete Heyting algebra. See Topology via logic

Also check Theorem 3.5.2, that a frame is a complete lattice and hence has infinite meets.

A map $f : A \to B$ is a frame homomorphism iff

• preserving finite meets $f(a \wedge b) = f(a) \wedge f(b)$
• preserving arbitrary joins $f(\bigvee_{i\in I} a_i) = \bigvee_{i\in I} f(a_i)$

A map $f : A \to B$ is a cHa homomorphism iff

• preserving arbitrary meets $f(\bigwedge_{i\in I} a_i) = \bigwedge_{i\in I} f(a_i)$
• preserving arbitrary joins $f(\bigvee_{i\in I} a_i) = \bigvee_{i\in I} f(a_i)$
• monotone (preserving Heyting implication) $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$

cHa homomorphism has a left adjoint and a right adjoint

  {-# OPTIONS --safe --without-K #-}
  module ag-93PB where

  open import MLTT.Spartan
  open import MLTT.List
  open import UF.Equiv
  open import UF.Univalence

polynomial解釋成型別時

  ⟦_⟧ : Poly → 𝓤₀ ̇ → 𝓤₀ ̇
  ⟦ 𝟘ᵖ    ⟧ X = 𝟘
  ⟦ 𝟙ᵖ    ⟧ X = 𝟙
  ⟦ var   ⟧ X = X
  ⟦ p ⊕ q ⟧ X = ⟦ p ⟧ X + ⟦ q ⟧ X
  ⟦ p ⊗ q ⟧ X = ⟦ p ⟧ X × ⟦ q ⟧ X

Figure 4 的前六行但排除 $\partial_x(y \setminus x)$

  ∂ : Poly → Poly
  ∂ 𝟘ᵖ      = 𝟘ᵖ
  ∂ 𝟙ᵖ      = 𝟘ᵖ
  ∂ var     = 𝟙ᵖ
  ∂ (p ⊕ q) = ∂ p ⊕ ∂ q
  ∂ (p ⊗ q) = (∂ p ⊗ q) ⊕ (p ⊗ ∂ q)

我們先看案例 $\text{btree}\ X = 1 + X^2$

  B : Poly
  B = 𝟙ᵖ ⊕ (var ⊗ var)

  _ : ∂ B ＝ 𝟘ᵖ ⊕ ((𝟙ᵖ ⊗ var) ⊕ (var ⊗ 𝟙ᵖ))
  _ = refl

  ∂B-≃ : {X : 𝓤₀ ̇ } → ⟦ ∂ B ⟧ X ≃ (X + X)
  ∂B-≃ = qinveq to (from , from-to , to-from)
    where
    to : {X : 𝓤₀ ̇ } → ⟦ ∂ B ⟧ X → X + X
    to (inl ())
    to (inr (inl (⋆ , x))) = inl x
    to (inr (inr (x , ⋆))) = inr x

    from : {X : 𝓤₀ ̇ } → X + X → ⟦ ∂ B ⟧ X
    from (inl x) = inr (inl (⋆ , x))
    from (inr x) = inr (inr (x , ⋆))

    from-to : {X : 𝓤₀ ̇ } → (c : ⟦ ∂ B ⟧ X) → from (to c) ＝ c
    from-to (inl ())
    from-to (inr (inl (⋆ , x))) = refl
    from-to (inr (inr (x , ⋆))) = refl

    to-from : {X : 𝓤₀ ̇ } → (v : X + X) → to (from v) ＝ v
    to-from (inl x) = refl
    to-from (inr x) = refl

  ∂B-＝ : is-univalent 𝓤₀ → (X : 𝓤₀ ̇ ) → ⟦ ∂ B ⟧ X ＝ (X + X)
  ∂B-＝ ua X = eqtoid ua _ _ ∂B-≃

給一個 one-hole context Γ : ⟦ ∂ p ⟧ X 跟一個元素 x : X，把 x 塞進洞裡重建出完整的 ⟦ p ⟧ X。

  _⋖_ : (p : Poly) {X : 𝓤₀ ̇ } → ⟦ ∂ p ⟧ X → X → ⟦ p ⟧ X
  _⋖_ 𝟘ᵖ ()
  _⋖_ 𝟙ᵖ ()
  (var ⋖ ⋆)                x = x
  ((p ⊕ q) ⋖ inl Γ)        x = inl ((p ⋖ Γ) x)
  ((p ⊕ q) ⋖ inr Γ)        x = inr ((q ⋖ Γ) x)
  ((p ⊗ q) ⋖ inl (Γ , qv)) x = (p ⋖ Γ) x , qv
  ((p ⊗ q) ⋖ inr (pv , Γ)) x = pv , (q ⋖ Γ) x
  infixl  _⋖_

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)

  {-# 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 ( , n))
Snd X n = X (encode ( , n))

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

  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

  {-# 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 ＝ ｛  ｝
is-inr X = Fst X ＝ ｛  ｝

輔助引理證明不可能既是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  (transport ( ∈_) (p ⁻¹ ∙ q) refl)

  _+ᵣ_ : 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  _+ᵣ_