{-# OPTIONS --cubical-compatible #-}
module AFF2024.AgdaTutorial.Session-ALA where

data ℕ : Set where  -- \bN
  zero : ℕ
  succ : ℕ → ℕ   -- \to
-- With this definition, the
-- inhabitants of ℕ are:
-- zero, succ zero, succ (succ zero), ...

-- in blackboard maths: f(x,y)
-- in Agda:             f x y

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

one : ℕ
one = succ zero

-- For instance, double 4 should be 8.
double : ℕ → ℕ
double zero     = zero
double (succ x) = succ (succ (double x))
-- double (succ x) = 2*(1+x) = 2 + 2x = 1 + (1 + 2x)
-- = succ (succ (double x))

-- on a blackboard: add : ℕ × ℕ → ℕ
_+_ : ℕ → ℕ → ℕ
zero   + y = y
succ a + y = succ (a + y)
-- add (succ a) y = (succ a) + y = (1+a) + y = 1+(a+y) = 1 + (add a y)
-- = succ (add a y)

data _≡_ : ℕ → ℕ → Set where
  refl : {x : ℕ} → x ≡ x

-- For every number x : ℕ, for every number y : ℕ,
-- there is a new type/set called "x ≡ y".
-- This type contains all the witnesses that x equals y.
-- For instance, the type "zero ≡ one" is empty.
-- On the other hand, the type "zero ≡ zero" is inhabited:
thm : (zero ≡ zero)  -- \==
thm = refl

two : ℕ
two = succ (succ zero)

thm' : (one + one) ≡ two
thm' = refl

-- logical reading: ∀y:ℕ. zero + y = y.
-- computational reading: "thm''" is a function which inputs
-- a natural number (henceforth called "y")
-- and outputs a witness that zero + y equals y.
thm'' : (y : ℕ) → (zero + y) ≡ y
thm'' y = refl

-- Logical reading: ∀f : ℕ → ℕ. ∀x : ℕ. ∀y : ℕ. (x = y ⇒ f(x) = f(y))
-- Computational reading: "cong" is a function which inputs
-- (1) a function f : ℕ → ℕ
-- (2) a number x : ℕ
-- (3) a number y : ℕ
-- (4) a witness that x equals y
-- and outputs a witness that f x equals f y.
-- cong : (f : ℕ → ℕ) → (x : ℕ) → (y : ℕ) → x ≡ y → f x ≡ f y
cong : (f : ℕ → ℕ) {x y : ℕ} → x ≡ y → f x ≡ f y
cong f refl = refl

thm''' : (x : ℕ) → (x + zero) ≡ x
thm''' zero     = refl
thm''' (succ a) = cong succ (thm''' a)

-- {-# BUILTIN NATURAL ℕ #-}
-- eighthundred : ℕ
-- eighthundred = 800

{-
thm'''' : (axiom-of-choice : ...) → (x : ℕ) → (x + zero) ≡ x
thm'''' = ?
-}

-- Agda is based on "Martin-Löf type theory" (with a couple of additions),
-- which is a constructive system, but we can always postulate axioms
-- missing from this foundation:
postulate
  -- axiom-of-choice : {!!}
  crazy-identity  : zero ≡ one