Cubical subtyping demo: get rid of inS/outS

[plt-amy]

Implemented to test out https://github.com/agda/agda/issues/6041. This isn't gonna compile because it's using unreleased features, of course. Anyway, something along the way between 2.6.2.2→master made it so that CupProductTensor has megabytes upon megabytes of unsolved metas... at least that one isn't self-evidently my fault :sweat_smile:

[mortberg]

Can we turn this into a draft PR somehow? Seems like something that is not ready to be reviewed or merged yet

[plt-amy]

Oh yeah, forgot to mark it as a draft.. sorry :slightly_smiling_face:. To be clear (and for onlookers) this isn't a draft in the sense of "this is something I'm working on that will eventually be put up for review", this is a draft in the sense of "I needed to test my inS/outS change upstream, and I need other people to weigh in."

[mortberg]

Oh yeah, forgot to mark it as a draft.. sorry slightly_smiling_face. To be clear (and for onlookers) this isn't a draft in the sense of "this is something I'm working on that will eventually be put up for review", this is a draft in the sense of "I needed to test my inS/outS change upstream, and I need other people to weigh in."

Thanks for marking it as a draft! This way it's easier for us to see which PRs we need to review and which we can just weigh in on when there is something to discuss :-)

[felixwellen]

Is this still a thing? If so, let me link #948, since there, axel filled in some metas to make CupTensorProduct check with 2.6.3.