{-# OPTIONS --allow-unsolved-meta #-}

open import Agda.Primitive

-- data Nat = Zero | Succ Nat
data  : Set where  -- \bN ℕ
  zero : 
  succ :   

double :   
double zero     = zero
double (succ n) = succ (succ (double n))

-- Set is the type of all (small) types.
-- Set itself is a type, but not a small type.
-- Set₁ is the type of all large types.
-- Set₂ is the type of all very large types.
-- zero : ℕ : Set : Set₁ : Set₂ : ... : Setω : Setω+1
id : {A : Set}  (A  A)
id x = x

ex : 
ex = id {} zero

data Vector (A : Set) :   Set where
  []  : Vector A zero
  _∷_ : {n : }  A  Vector A n  Vector A (succ n)

two : 
two = succ (succ zero)

ex₂ : Vector  two
ex₂ = two  (zero  [])

_+_ :     
zero   + b = b
succ a + b = succ (a + b)

data Bool : Set where
  false true : Bool

-- "The boolean way"
is-even? :   Bool
is-even? zero            = true
is-even? (succ zero)     = false
is-even? (succ (succ n)) = is-even? n

is-eq? :     Bool
is-eq? zero zero = true
is-eq? zero (succ b) = false
is-eq? (succ a) zero = false
is-eq? (succ a) (succ b) = is-eq? a b

is-eq?? : (  )  (  )  Bool
is-eq?? f g = {!!}

-- Haskell just has types depending on types,
-- like [Int] or IO Int; Agda also has types
-- depending on values; and in fact, types also
-- are just values (namely values of type Set
-- (or Set₁ (or Set₂ (...)))).
replicate : {X : Set}  (n : )  X  Vector X n
replicate zero     x = []
replicate (succ n) x = x  replicate n x

-- "The witness way"
-- "Even n" is the type of witnesses that n is even.
-- For instance, Even (succ zero) should be an empty type.
-- But Even zero and Even (succ (succ zero)) should contain
-- something.
data Even :   Set where
  base : Even zero
  step : {n : }  Even n  Even (succ (succ n))

postulate
  whatever : Even (succ zero)

-- de Bruijn factor

four-is-even : Even (succ (succ (succ (succ zero))))
four-is-even = step (step base)

even-numbers-are-even : {n : }  Even n  Even n
even-numbers-are-even p = p

double-x-is-even : (n : )  Even (double n)
double-x-is-even zero     = base
double-x-is-even (succ n) = step (double-x-is-even n)
-- double (succ n) is succ (succ (double n))

thm : Even (succ (succ zero))
thm = double-x-is-even (succ zero)

-- For every type X, and for every values a and b of X,
-- there should be a type "a ≡ b" of witnesses that a equals b.
-- For instance, if a and b are NOT equal, then this type should
-- be empty.
data _≡_ { : Level} {X : Set } : X  X  Set where
  refl : {x : X}  x  x
  -- bailout : {x y : X} → x ≡ y

lemma₀ : (zero + zero)  zero
lemma₀ = refl

lemma₁ : (b : )  (zero + b)  b
lemma₁ b = refl

cong
  : { : Level} {X Y : Set } {a b : X}
   (f : X  Y)  a  b  f a  f b
cong f refl = refl

lemma₂ : (a : )  (a + zero)  a
lemma₂ zero     = refl
lemma₂ (succ a) = cong succ (lemma₂ a)

foo :   (b : )    is-even? b  true  Vector  b
foo a b c p = {!!}

foo' :   (b : )    Even b  Vector  b
foo' a b c p = {!!}

data List (X : Set) : Set where
  []  : List X
  _∷_ : X  List X  List X

length : {X : Set}  List X  
length []       = zero
length (x  xs) = succ (length xs)

fib :   
fib zero            = zero
fib (succ zero)     = succ zero
fib (succ (succ n)) = fib n + fib (succ n)
-- This implemention requires O(fib(n)) time for computing fib n.

data IsFibonacci :   Set where
  bar : (a : )  IsFibonacci (fib a)

foo'' : {X : Set}  (xs : List X)  IsFibonacci (length xs)  {!!}
foo'' = {!!}

open import Data.Product

foo''' : {X : Set}  (xs : List X)  Σ[ a   ] (length xs  fib a)  {!!}
foo''' = {!!}