Let's play Agda
  
A journey through programming, proofs and play:
running abstract mathematical proofs as programs

0. 👤 About me
1. 🚨 The biggest risk of this course
2. 😇 What Agda ostensibly is
3. 💥 What Agda really is
4. 🔭 What we could explore in this course (after covering the basics)
	  a. 🌳 Sets as trees
	  b. ♾️ Numbers larger than infinity
	  c. 🗝️ The sarcastic interpretation of classical logic
	  d. 🌌 Creating mathematical universes
	  e. ❌ A counterexample to the axiom of choice
	  f. 😱 The final digit of Graham's fantastical number
	  g. ✨ Your topic here
5. 👣 Our first steps with Agda


# 👤 About me

## 👨‍🏫 Mathematician from Augsburg, Germany

* ✅ your assistant
* ❌ not your boss
* 💬 +49 176 95110311 (Signal, Telegram, SMS)


## ⭐️ **Favorite mathematical objects**

* 🌌 Eff, a bizarre/comforting alternate mathematical universe in which...
  * 🧮 every function ℕ → ℕ is computable
  * 📈 every function ℝ → ℝ is continuous

* 🤯 The generic surjection ℕ ↠ ℝ, defeating the uncountability of ℝ


## 💡 **Favorite mathematical theorems**

* ♾️ Beyond every number, there is a prime number.
* 💣 ¬¬(A ∨ ¬A), the time travel theorem.


# 🚨 The biggest risk of this course

Too much talking/listening, too few Agda interactions.


# 😇 What Agda ostensibly is

Agda is a programming language ...

> square : ℕ → ℕ
> length : List Bool → ℕ   -- compute the length of a list of booleans
> pi     : ℝ               -- arbitrary-precision constant

... and simultaneously a proof language ...

> grande-teorema   : 2 + 2 ≡ 4
> binomial-theorem : (x : ℕ) (y : ℕ) → (x + y) ² ≡ x ² + 2 * x * y + y ²

made possible by *types of witnesses*, for instance:

- There is the type of witnesses that 2 + 2 equals 4. This type is written "2 + 2 ≡ 4".
  This type is inhabited.
- There is the type of witnesses that 2 + 2 equals 5. This type is written "2 + 2 ≡ 5".
  This type is empty.
- There is the type of witnesses that there are prime numbers larger than 42. This type is written
  "∃[ p ] (p > 42 × Prime p)". This type contains pairs consisting of a number and a witness
  that this number is indeed larger than 42 and is indeed prime. For instance (43 , ...).
- There is the type of witnesses that the binomial theorem holds. Such a witness is a function
  which reads as input two numbers x and y, and which outputs a
  witness that (x + y)² equals x² + 2xy + y².
- There is the type of witnesses that a given sorting function, for instance quicksort,
  indeed behaves correctly.
- There is the type of witnesses that the continuum hypothesis holds.

... helping us with ...

- verifying correctness of proofs
- implementing algorithms
- structuring mathematical thoughts
- appreciating mathematics from a computational angle
- collaboratively engineering mathematical libraries


# 💥 What Agda (and other systems like it) really is

- An extremely fun and addictive multiplayer game. :-)
- The ultimate canvas for your mathematical thoughts,
  giving you almost unlimited freedom while simultaneously offering an extremely strong safety net.
- Technology for lowering the barrier to do mathematics (kinda)
- A device for rendering ChatGPT, Claude & Co. **reliable**


# 🔭 What we could explore in this course (after covering the basics)

## 🌳 Sets as trees

## ♾️ Numbers larger than infinity

    0, 1, 2, 3, ..., ω (the first infinite number), ω + 1, ω + 2, ..., ω + ω = 2ω, 2ω + 1, 2ω + 2, ...,
    3ω, ..., 4ω, ..., ω², ..., ω³ = ω^3, ..., ω⁴ = ω^4, ..., ω^ω, ..., ω^ω^ω^ω^ω^... = ε₀, ε₀ + 1, ...,
    ε₀^ε₀^ε₀^ε₀^... = ε₁, ..., ε₁^ε₁^ε₁^ε₁^... = ε₂ = ε_2, ..., ε₃ = ε_3, ..., ε_ω, ...,
    ε_{ω⁵+17}, ..., ε_{ε₀}, ..., ε_{ε_{ε₀}}, ..., ..., ε_{ε_{ε_...}} = ζ₀, ...

## 🗝️ The sarcastic interpretation of classical logic

Theorem (Dickson's Lemma). For every function f : ℕ → ℕ, there is a number n : ℕ such that f(n) ≤ f(n+1).

Proof. This function attains a global minimum, say f(n). For this n, we have f(n) ≤ f(n+1).

Problem. This proof, while absolutely valid within classical mathematics, does not give any clue
how to find this number n.

Amazing fact. Mind-blowingly, after just a little bit of massaging, we can run this proof in Agda.
Agda will then compute a suitable number n such that f(n) ≤ f(n+1).

## 🌌 Creating mathematical universes

## ❌ A counterexample to the axiom of choice (in a different mathematical universe)

## 😱 The final digit of Graham's fantastical number

## ✨ Your topic here


# 👣 Our first steps with Agda

```
-- "Let there be natural numbers."
data ℕ : Set where   -- β \beta, → \to, ℕ \bN
  zero : ℕ
  succ : ℕ → ℕ   -- successor
-- These three lines tell Agda that there should be a new set, called "ℕ",
-- and that there should be two ways of constructing inhabitants of ℕ:
-- 1. zero is an element of ℕ.
-- 2. Given an inhabitant n : ℕ, succ(n) will be a new freshly-minted inhabitant of ℕ.
--
-- Summarizing, ℕ contains the following inhabitants:
-- zero, succ zero, succ (succ zero), ...

-- In blackboard mathematics, we write "f(x)".
-- In Agda,                   we write "f x".

data Bool : Set where
  false : Bool
  true  : Bool

-- `not true`  should be `false`.
-- `not false` should be `true`.
not : Bool → Bool
not false = true
not true  = false

-- `and` is a function which inputs two Booleans and outputs a Boolean.
and : Bool → Bool → Bool
and false y = false
and true  y = y

test : Bool
test = not (and false (not true))

one : ℕ
one = succ zero

two : ℕ
two = succ (succ zero)

-- zero is of type ℕ, because ℕ is the type of all natural numbers. (ℕ is a small type.)
-- ℕ is of type Set,  because Set is the type of all (small) types. In MLTT, Set is written "U₀".
-- Set is of type Set₁, because Set₁ is the type of all large types. In MLTT, Set₁ is written "U₁".
-- Set₁ is of type Set₂, because Set₂ is the type of all very large types.

-- zero : ℕ : Set : Set₁ : Set₂ : ... : Setω : ...
```