{-# OPTIONS --cubical-compatible #-}
module Padova2025.Welcome.Rosetta whereA mathematical Rosetta Stone#
The following table is included here for ease of reference (and perhaps as a kind of cryptic teaser). It will make more sense when we discuss how Agda can be used as a proof language.
With the advent of homotopy type theory, a further column to this table was discovered. We will discuss this expansion in the context of Cubical Agda.
| Blackboard mathematics | Agda |
|---|---|
| A claim | A type (of witnesses) |
| Proving a claim | Exhibiting an element of the corresponding type |
| An unsound proof attempt | A term which does not type-check |
| Leaving a part of a proof attempt to be filled in later | Leaving a hole ? |
| Realizing a missing assumption | Adding an extra argument |
| Assertion that x = y | Type x ≡ y (a certain standard equality type) |
| Trivially equal by inspection | Witness refl |
| Arguing by induction | Defining a recursive function |
| Induction hypothesis | Recursive function call |
| Arguing by cases | Defining a function by pattern matching |
| Fixing an element x ∈ A for the remainder of a section | Anonymous module module _ (x : A) where |
| Function application f(x) | Function application f x |
| Result foo applied to x | Function application foo x |
| Result P ⇒ Q | Function of type P → Q which transforms witnesses of type P into witnesses of type Q |
| Result P ∧ Q | Element of P × Q (i.e. a pair of witnesses) |
| Result P ∨ Q | Element of P ⊎ Q (i.e. a witness of either) |
| Result ∀(x ∈ A). P(x) | Function of type (x : A) → P x which reads an arbitrary x as input and produces a witness of P x as output |
| Result ∃(x ∈ A). P(x) | Element of Σ[ x ∈ A ] P x (i.e. a pair (x , p) consisting of an element x and a witness of type P x) |
| Result ¬ P | Function of type P → ⊥ |
| Contradiction/absurdity | Empty type ⊥ |
| A (small) subset of a set A | A function A → Set |
| Class of all sets | Type Set of all small types (also spelled Set₀) |
| (Small) set | Small type, i.e. element of Set |
| Proper class | Type which is not an element of Set (but of Setᵢ for some nonzero universe level i) |
| A ring | A record bundling carrier, operations and laws |
| A commutative ring | A record with an extra commutativity field |