Experiment on contra-variant subtyping

[jiangsy]

No description provided.

[Ailrun]

https://github.com/Beluga-lang/McTT/tree/pr-some-contra This branch may also give you some idea

[HuStmpHrrr]

fix the cr by commenting entries in _CoqProject, and then it can be merged.

[jiangsy]

fix the cr by commenting entries in _CoqProject, and then it can be merged.

I think the Core part itself is good with failed files all commented out. The error is about extraction.

[jiangsy]

https://github.com/Beluga-lang/McTT/tree/pr-some-contra This branch may also give you some idea

Thanks for the reminder. I have already ported most development in that branch.

[Ailrun]

Could you explain why do we need that weak cong?

[Ailrun]

Also some relevant discussion: #129

[jiangsy]

Could you explain why do we need that weak cong?

it's still an experiment. basically for "realizaibility" of subtyping, I think we want ⇑ a n and ⇑ a' n' where a <: a' (instead of a ≈ a') to be "related" in some sense. but the readback of reflection with a sub/super value could (potentially) change the argument annotation. so we would like to prove a weaker lemma to show that except for these annotations, we get the same output.

[HuStmpHrrr]

Could you explain why do we need that weak cong?

a short answer is that with eta expansion, the theorem in your discussion simply won't hold with a strict equality, though I speculate that it might if we ignore types that are introduced via eta, e.g. input types of Pi, and second types of Sigma.

[Ailrun]

That sounds more like we need to remove the annotation on lambda after introducing type annotations on an intermediate representation