{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.Welcome.Rosetta where數學的羅塞塔石碑#
下表放在這裡方便查閱（或許也可以當成一則神祕的預告）。等我們討論如何把 Agda 當成證明語言使用時， 它會變得更有意義。
隨著 homotopy type theory 的出現，這張表又被發現多出一欄。我們會在 Cubical Agda 的脈絡下討論這個擴充。
| 黑板上的數學 | Agda |
|---|---|
| 一個命題（claim） | 一個型別（見證的型別） |
| 證明一個命題 | 給出對應型別的一個元素 |
| 一個不健全的證明嘗試 | 一個無法通過型別檢查的 term |
| 把證明嘗試的一部分留到之後再補 | 留下一個 hole ? |
| 發現缺了某個假設 | 多加一個引數 |
| 斷言 x = y | 型別 x ≡ y（某個標準的相等型別） |
| 看一眼就知道相等 | 見證 refl |
| 用歸納法論證 | 定義一個遞迴函數 |
| 歸納假設 | 遞迴的函數呼叫 |
| 分情況論證 | 用 pattern matching 定義函數 |
| 在一節的其餘部分固定一個元素 x ∈ A | 匿名模組 module _ (x : A) where |
| 函數作用 f(x) | 函數應用 f x |
| 結果 foo 作用在 x 上 | 函數應用 foo x |
| 結果 P ⇒ Q | 型別為 P → Q 的函數，把型別 P 的見證轉換為型別 Q 的見證 |
| 結果 P ∧ Q | P × Q 的元素（也就是一對見證） |
| 結果 P ∨ Q | P ⊎ Q 的元素（也就是其中任一邊的見證） |
| 結果 ∀(x ∈ A). P(x) | 型別為 (x : A) → P x 的函數，讀入任意的 x 作為輸入，輸出 P x 的見證 |
| 結果 ∃(x ∈ A). P(x) | Σ[ x ∈ A ] P x 的元素（也就是一個序對 (x , p)，由元素 x 與型別 P x 的見證組成） |
| 結果 ¬ P | 型別為 P → ⊥ 的函數 |
| 矛盾／荒謬 | 空型別 ⊥ |
| 集合 A 的（小）子集 | 一個函數 A → Set |
| 所有集合所成的類 | 所有小型別的型別 Set（也寫作 Set₀） |
| （小）集合 | 小型別，也就是 Set 的元素 |
| 真類（proper class） | 不是 Set 的元素的型別（而是某個非零 universe level i 的 Setᵢ 的元素） |
| 一個環 | 一個把載體、運算與定律打包在一起的 record |
| 一個交換環 | 一個多了交換律欄位的 record |