-- With the following three lines of code, a new datatype is created.
-- Its name is "Bool" and its values are "false" and "true".
data Bool : Set₀ where
  false : Bool
  true  : Bool

-- https://agdapad.quasicoherent.io/#Padova2025/viewonly

data ℕ : Set where   -- \bN
  zero : ℕ
  succ : ℕ → ℕ    -- "successor"
-- The inhabitants of ℕ are:
-- zero, succ zero, succ (succ zero), succ (succ (succ zero)), ...

-- For instance, "double two" should be "four".
double : ℕ → ℕ
double zero     = zero
double (succ x) = succ (succ (double x))
-- informally, in blackboard mathematics:
-- double(succ(x)) = 2*(1+x) = 2+2x = 1+(1+2x) = succ(succ(2x)) = succ(succ(double(x)))

add : ℕ → ℕ → ℕ
add zero     y = y
add (succ x) y = succ (add x y)
-- informally, in blackboard mathematics:
-- succ(x)+y = (1+x)+y = 1+(x+y) = succ(x+y)

_+_ : ℕ → ℕ → ℕ
zero   + y = y
succ x + y = succ (x + y)

-- in blackboard mathematics, 3! = 3 * 2 * 1

_! : ℕ → ℕ
x ! = {!!}

data Weird : Set where
  foo : Weird → Weird
-- What are values of type Weird?
-- There are no values of type Weird.
-- This type is empty.

-- If we write "f x y", then Agda interprets this as the blackboard-mathematics "f(x,y)",
-- so as calling "f" with two arguments.

one : ℕ
one = succ zero

two : ℕ
two = succ (succ zero)

-- In C, bool isTheSunShining;
is-the-sun-shining : Bool
is-the-sun-shining = true

-- The identity function.
--
-- def id(x):
--   return x
--
-- bool id(bool x) {
--   return x;
-- }
id : Bool → Bool   -- \to \alpha α
id x = x

-- The negation function.
--
-- def neg(x):
--   if x:
--     return False
--   else:
--     return True
--
-- bool neg(bool x) {
--   if(x) {
--     return false;
--   } else {
--     return true;
--   }
-- }

neg : Bool → Bool
neg false = true
neg true  = false
-- This is a definition "by pattern matching".

-- We make a hole appear by writing a "?" and then pressing C-c C-l.

-- C-c C-l: load file
-- C-c C-v: evaluate term
-- C-c C-c: case split  (if the cursor is in a hole)
-- C-c C-space: check hole
-- C-c C-a: automatic mode

-- In blackboard mathematics: f(x), sin(π)
-- In Agda:                   f x,  sin π, id x

-- Set is the type of small types. In MLTT, "Set" is called "U₀".
-- Set itself is not a small type, but a large type.
-- The type of all large types is Set₁.
-- Set₁ itself it not a large type, but a very large type.
-- The type of all very large types is Set₂.
--
-- "Set" and "Set₀" are synonymous.
--
-- false : Bool : Set : Set₁ : Set₂ : Set₃ : Set₄ : ... : Setω : Setω+1 : ... : Setω2
--
-- The naive idea of a "set of all sets" or a "type of all types"
-- is inconsistent. In set theory, this is known as Russell's paradox,
-- and in type theory, this is known as Girard's paradox.

-- In Agda, by default, we do not have the "powerset axiom".
-- This axiom states that every set has a powerset.

fun : ℕ → (ℕ → ℕ)
fun zero        = id'
  where
  id' : ℕ → ℕ
  id' x = x
fun (succ zero) = double
fun _           = succ



{-
  * dependent types
  * lists, vectors
  * implicit parameters
-}

-- Most programming languages only support non-dependent types:
-- int, float, double, string, int[], ...

-- In contrast, Agda also supports dependent types -- these
-- are types which depend on values:
-- Vector ℕ a, the type of length-a-lists of natural numbers

Foo : ℕ → Set
Foo zero               = Bool
Foo (succ zero)        = ℕ
Foo (succ (succ zero)) = Bool → Bool
Foo _                  = ℕ


Bar : ℕ → Set₁
Bar zero = Bool'
  where
  data Bool' : Set₁ where
    false : Bool'
    true  : Bool'
  favorite-number : ℕ
  favorite-number = succ (succ (succ zero))
Bar _    = Set


-- Let's define the type of lists of natural numbers.
-- So this type should contain, for instance, the list (two ∷ (four ∷ (zero ∷ (one ∷ [])))).
data NatList : Set where
  []  : NatList
  _∷_ : ℕ → NatList → NatList
  -- The constructor "_∷_" takes two arguments,
  -- namely a natural number and
  -- an already-constructed list.

-- The following three lines of code introduce, for each X : Set, a type List X.
data List (X : Set) : Set where
  []  : List X
  _∷_ : X → List X → List X
  -- "X" is a "parameter" of this definition

newExampleList : List Bool
newExampleList = true ∷ (true ∷ (false ∷ (true ∷ [])))

-- double' : (a : ℕ) → ℕ........here we could use a.......
-- double' zero = zero
-- double' (succ x) = succ (succ (double' x))

-- "newLength" is a function which inputs two arguments, namely
-- - a type X
-- - a list xs : List X
-- and outputs the length of the list xs.
newLength : (X : Set) → List X → ℕ
newLength X []       = zero
newLength X (x ∷ xs) = succ (newLength X xs)

-- With the curly braces {...}, we mark the argument as implicit, so
-- that we do not need to explicitly supply it when calling the newLength' function.
newLength' : {X : Set} → List X → ℕ
newLength' []       = zero
newLength' (x ∷ xs) = succ (newLength' xs)

example-usage : ℕ
example-usage = newLength' {Bool} newExampleList

idBool : Bool → Bool
idBool x = x

idNat : ℕ → ℕ
idNat x = x

idListBool : List Bool → List Bool
idListBool x = x

-- In type theory, we would write:
--   generalIdentityFunction : Π_(X : Set) Π_(u : X) X
-- This function is a function which inputs two arguments, namely
-- - a type X (implicit) and
-- - a value u of type X.
generalIdentityFunction : {X : Set} → X → X
generalIdentityFunction u = u

-- By the type signature, the function "choice" would need to do the following:
-- Read a type X as input; produce a value of type X as output.
choice : (X : Set) → X
choice X = {!!}
-- this hole can never be filled, because of the case that X is empty

postulate
  crazy-number : ℕ
  foo-function : Bool → ℕ
  -- axiom-of-choice : (X : InhabitedSet) → X

data ListOfBooleans : Set where
  []  : ListOfBooleans
  _∷_ : Bool → ListOfBooleans → ListOfBooleans

exampleList : NatList
exampleList = two ∷ (one ∷ [])

length : NatList → ℕ
length []       = zero
length (x ∷ xs) = succ (length xs)
-- For instance, length exampleList should be two.


ex : Foo zero
ex = false
-- in Agdapad:         C-c C-,
-- in Let's play Agda: C-c ,

ex₂ : Foo one
ex₂ = two

-- The type "Foo n" depends on the value n.