{-# OPTIONS --allow-unsolved-metas #-}

data _≡_ {X : Set} : X  X  Set where
  refl : {x : X}  x  x

data  : Set where
  zero : 
  succ :   

half :   
half zero            = zero
half (succ zero)     = zero
half (succ (succ n)) = succ (half n)
{-                                ^
                                  this argument to "half" is structurally
                                  smaller than the input argument
                                  "succ (succ n)"                      -}

_ : half (succ (succ (succ zero)))  succ zero
_ = refl

data _<_ :     Set where
  base  : {n : }      n < succ n
  step  : {a b : }    a < b  a < succ b

_ : zero < succ (succ (succ zero))
_ = step (step base)

lemma-succ-mon : {a b : }  a < b  succ a < succ b
lemma-succ-mon base     = base
lemma-succ-mon (step p) = step (lemma-succ-mon p)

lemma-succ-step : (a : )  a < succ a
lemma-succ-step a = {!!}

<-trans : {a b c : }  a < b  b < c  a < c
<-trans p q = {!!}

-- "digits n" should be the number of binary digits of
-- the number "n", with the convention that the number zero
-- consists of no binary digits at all.
-- For instance, "digits 5" should be "3", as 5 is 101 in binary.

half< : (n : )  half (succ n) < succ n
half< zero            = base
half< (succ zero)     = base
half< (succ (succ n)) = lemma-succ-mon (<-trans (half< n) (lemma-succ-step (succ n)))

-- The type "Acc n" is the type of witnesses that the number "n"
-- is accessible.
data Acc :   Set where
  -- Logical reading: For every number x,
  -- if every number y smaller than x is accessible,
  -- then x is accessible.
  acc : {x : }  ({y : }  y < x  Acc y)  Acc x
-- "Acc x" is the type of trees consisting of a root
-- and as many children as there are numbers smaller than "x".
-- To be more precise: one child for each number y together with a
-- witness that y < x.

data BinaryTree : Set where
  leaf : BinaryTree
  fork : BinaryTree  BinaryTree  BinaryTree
-- When we write "fork s t", then "s" and "t" are each
-- structurally smaller than "fork s t": "s" and "t"
-- are constitutent parts of the new whole, namely of "fork s t".

{-
{-# OPTIONS --no-positivity-check #-}

data V : Set where
  fork : (V → V) → V

absurd : ⊥
absurd = ?
-}

data CountablyBranchingTree : Set where
  leaf : CountablyBranchingTree
  fork : (  CountablyBranchingTree)  CountablyBranchingTree
-- When we write "fork f", then all the outputs of "f"
-- are each structurally smaller than "fork f": The outputs of "f"
-- are constitutent parts of the new whole, namely of "fork f".

data ExtremelyBranchingTree : Set₁ where
  leaf : ExtremelyBranchingTree
  fork : (Set  ExtremelyBranchingTree)  ExtremelyBranchingTree

open import Agda.Primitive

ex : Setω
ex = (n : Level)  Set n

ex' : Setω₁
ex' = Setω
{-
       *
     /  \
   leaf  *
        / \
     leaf  leaf
-}
exampleTree : BinaryTree
exampleTree = fork leaf (fork leaf leaf)

-- size : BinaryTree → ℕ

lemma-zero-is-accessible : Acc zero
lemma-zero-is-accessible = acc  ())

lemma-one-is-accessible : Acc (succ zero)
lemma-one-is-accessible = acc  { base  lemma-zero-is-accessible })

-- Logical reading: Every number n is accessible.
ℕ-is-wellfounded : (n : )  Acc n
ℕ-is-wellfounded n = {!!}

go : (n : )  Acc n  
go zero     g       = zero
go (succ n) (acc f) = succ (go (half (succ n)) (f (half< n)))
{-                                              ^^^^^^^^^^^
                                                this argument to "go"
                                                is structurally smaller
                                                than the input argument
                                                "acc f"                  -}

digits :   
digits n = go n (ℕ-is-wellfounded n)