Add subtyping for cumulativity

[Ailrun]

C.f. #120

Let's implement subtyping

• syntactic extension
  • Working on subtyping #122
  • remove contra-variant subtyping #127
• PER model
  • [WIP] define subtyping for the PER model #125
  • subtyping in the PER model #128
• PER model lemma
  • subtyping in the PER model #128
• completeness
  • working on completeness rules for subtyping #130
  • finish completeness proof #133
• soundness
  • working on realizability #140
  • Prove subtyping case for soundness #153
• subtyping checker
  • working on algorithmic subtyping #124
  • working on subtyping impl #152

[Ailrun]

@HuStmpHrrr It seems like Meven knows some :)
https://coq.discourse.group/t/coqs-cumulativity/2334

[Ailrun]

Oh lol that's actually an answer on your email haha

[HuStmpHrrr]

I think contra-variant subtyping will have to be abandoned (#125 ), as per our offline discussions. Too many things just can't work out. I will prepare a PR to do only co-variant subtyping.

see

[Ailrun]

I will leave this issue open for the contravariant subtyping.

[Ailrun]

Actually there is #129, so let's close this.