implement pi type correctly

[dannypsnl]

implement pi type correctly

[dannypsnl]

I think it's a type in Type0 exists in Type1

A : Type0 shows A : Type1

[CYBAI]

As @dannypsnl discussed with me, we should do following steps to implement Pi type properly

1. Make universal level types
2. Confirm we can create universal types properly (e.g. a type in Type 0 exists in Type 1 but a type in Type 1 doesn't exist in Type 0)
3. After we have universal types, we can try to reuse them in Pi types

Refs:
[1]: https://sozeau.gitlabpages.inria.fr/www/research/publications/drafts/univpoly.pdf
[2]: https://ncatlab.org/homotopytypetheory/show/universe

[dannypsnl]

We do hard coding for universe for now

[dannypsnl]

When we have

data K
  c : K -> K

c should have type Pi (_ : K) K

[dannypsnl]

This is done and get usage now, let's treat universe level as a new issue