Reimplement sort system

[ice1000]

Taken from #507

Update (2023/2/17): I now believe that irrelevance as a universe is very weird. I would like to remove this feature and add irrelevance modality later.

• [ ] tyck rules for top level defs
• ~~[x] Prop tyck rules~~
• [ ] more Set tyck rules
• [ ] disallow data to live in ISet
• ~~[ ] non-Prop metas~~
• ~~[x] irrelevance of propositions (that, if A : Prop and a b : A, then a = b definitionally)~~
• [x] pi domain checks
• ~~[x] pattern matching restrictions~~
• [ ] Paths should be restricted to Type

[ice1000]

Ref: https://github.com/aya-prover/aya-dev/issues/449

[ice1000]

We temporarily give up Prop due to its complication