Working on subtyping #122
Working on subtyping #122
Conversation
|
I think #121 needs to be split into multiple PRs otherwise this one will be too big. I am not sure what is a better way than accepting broken CI before this work is done. |
|
How about changing some proofs that require both model&syntax (such as the |
| {{ Γ ⊢ A' : Type@i }} -> | ||
| {{ Γ , A' ⊢ B' : Type@i }} -> | ||
| {{ Γ ⊢ A' ⊆ A }} -> | ||
| {{ Γ , A' ⊢ B ⊆ B' }} -> |
There was a problem hiding this comment.
This (genuine) asymmetry bothers me a bit... By that, I mean, if we do not have argument subtyping {{ Γ , A' ⊢ B ⊆ B' }} and {{ Γ , A ⊢ B ⊆ B' }} would be equivalent, but now {{ Γ , A ⊢ B ⊆ B' }} doesn't even make sense (as B' may require the A', not A, in its context).
I cannot come up with a real problem and this should be fine, but it feels a bit...
More concretely, something like this bothers me: after presupposition, we can get exist i, {{ Γ, A' ⊢ B' : Type@i }} out of {{ Γ, A' ⊢ B ⊆ B' }}, but then, this is not enough to remove {{ Γ , A ⊢ B : Type@i }} because this one has a stronger information. (that B is still well-typed in a less informative context)
|
ok, syntactic part is ready |
C.f. #121
This PR is likely to be huge. Stay tuned.