Recursion in Hippogriff at large types

theory EvenAndOdd/typeof := sig
  even : Type
  odd : Type
end

def EvenAndOdd : EvenAndOdd/typeof := struct
  even := sum
    'zero
    'succ (EvenAndOdd.odd)
  end
  odd := sum
    'succ (EvenAndOdd.even)
  end
end

def three : EvenAndOdd.odd := 'succ ('succ ('succ 'zero))
# rejected!
# def two : EvenAndOdd.odd := 'succ ('succ 'zero)

# rejected!
# def Bad : Type := Bad

\[\begin{align*} &\ms{let}_p \colon \{A\,B \colon \ms{Ty}_k\} \to (f \colon \triangleright (\ms{El}_k\,A) \to \ms{El}_p\,A) \to ((a \colon \ms{El}_k\,A) \to a \rightsquigarrow f\,(\ms{now}\,a) \to \ms{El}_k\,B) \to \ms{El}_k\,B \end{align*}\]

(sum uses \(\triangleright \ms{Ty}_k\))