AC!

XOO 寫信來討論，我才赫然發現證明 weak bisimilarity 的 transitivity 時為了方便而寫的

λΣ₁₁-dist : {A : Set} {P : A → Set1} {Q : (z : A) → P z → Set1} →
             (∀ z → Σ₁₁ (P z) (Q z)) → Σ₁₁ (∀ z → P z) (λ p → ∀ z → Q z (p z))
λΣ₁₁-dist f = (λ x → proj₁₁₁ (f x)) , (λ x → proj₁₁₂ (f x))

竟然就是 ITT 的 Axiom of Choice！突然從實用情境當中跳出來，嚇死我了 XD。

--
所以我們現在轉向研究 type theory 了嗎？